Стратегии управления процессом поиска доказательства методом резолюций. Стратегии упрощения при вычислении резолюций

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

Виды стратегий:

o стратегия поиска в ширину,

o стратегия опорного множества,

o стратегия предпочтения одночленам,

o стратегия линейная по входу,

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

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

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

Стратегия линейная по входу требует обязательной принадлежности одного из родительских предложений базовому множеству. Пример предыдущего параграфа соответствует этой стратегии.

Ограничения, вводимые стратегиями, приводят к увеличению глубины диаграммы опровержения и отсутствию полноты стратегии. На рис.38.1 приведена диаграмма процесса поиска доказательства в ширину, которая показывает, что доказательство получено на третьем уровне резолюций, в отличии от линейной стратегии (рис.37.1), позволившей завершить поиск лишь на четвертом уровне.

Рис.37.1. Диаграмма процесса поиска доказательства в ширину

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

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

o Любое предложение, содержащее литерал и его отрицание, может быть отброшено. Например: .

o Если литерал, входящий в предложение, для любых допустимых интерпретаций имеет значение “ложь”, то его можно исключить. Например: эквивалентно .

o Предложение в неудовлетворимом множестве, которое подсуммируется с другим предложением, можно отбросить. Если является подмножеством , то подсуммирует . Например: подсуммирует .

o