8.10. СТРАТЕГИИ УПОРЯДОЧЕНИЯ

На основе резольвенций, обеспечиваемых различными стратегиями очищения, иногда можно искать опровержение, упорядочив выполняемые резольвенции. В стратегиях упорядочения не запрещаются никакие типы резольвенций, а лишь даются указания на то, какие из них надо выполнять в первую очередь. Стратегии упорядочения соответствуют рассмотренным в гл. 3 и 5 эвристическим стратегиям перебора для поиска на графах. При хорошем упорядочении не обязательно вычислять все элементы множеств Если пустое предложение появляется впервые на уровне то хочется думать, что перебор можно прямо направить на этот уровень, не заполняя нижние уровни.

Две довольно эффективные стратегии упорядочения — это стратегия предпочтения одночленам и стратегия наименьшего числа компонент. В стратегии предпочтения одночленам делается попытка сначала построить резольвенты между одночленами, т. е. предложениями, содержащими единственный литерал. Если это удается, то сразу же получается опровержение. Если же не могут найти пару одночленов, у которых есть

резольвента, то пытаются найти резольвенту для пар одночлен— двучлен и т.д. (Как только какая-нибудь пара предложений разрешается, полученную резольвенту сразу сопоставляют с одночленами с тем, чтобы найти возможные резольвенты.) Во избежание совершения невыгодной цепочки одночленных резольвенций обычно устанавливается граничный уровень. Если предложение содержится в но не содержится в , то говорят, что данное предложение имеет уровень Если граничный уровень равен то предложения из не строятся. Когда граничный уровень препятствует поиску одночленных резольвенций, применяют другие схемы упорядочения (такие, как резольвенции двучленов и одночленов и т. д.) до тех пор, пока не будут построены новые одночлены.

Стратегия предпочтения одночленам оправдана гарантированным укорочением длины предложений, вызываемым одночленными резольвенциями. Так как цель построения резольвент состоит в образовании пустого предложения (нулевой длины), то стратегия предпочтения одночленам напрашивается сама собой. При введении граничных уровней для возможности использования и других резольвенций такая стратегия не препятствует нахождению опровержения (если оно существует в пределах заданной границы) и, как правило, сильно ускоряет процесс перебора.

Стратегия наименьшего числа компонент упорядочивает резольвенции согласно длине получаемых резольвент. Так, два предложения, дающие наиболее короткую резольвенту, разрешаются в первую очередь. Эта стратегия в некотором смысле дороже, поскольку до выполнения резольвенции надо подсчитать длины потенциальных резольвент и упорядочить их.