Сравнение метода резолюций и ИВ

Мы привели конструктивные доказательства полноты исчисления высказываний и полноты метода резолюций. Оба они используют перебор по полному бинарному дереву. Но доказательство полноты для ИВ перебирает дерево в направлении от листьев к корню и всегда даёт экспоненциально длинный вывод, а в построении резолютивного вывода используется лишь допустимое дерево, которое может быть намного меньше.

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

Пример 1.47 (2-КНФ). Если каждый дизъюнкт содержит не более двух литералов, то такая КНФ называется 2-КНФ. Резольвента дизъюнктов, в каждый из которых входит не более двух литералов, также содержит не более двух литералов. Поэтому резолютивный вывод для 2-КНФ не может быть очень длинным — из п переменных можно образовать всего 0(п²) дизъюнктов, содержащих не более двух литералов.

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

Если для формулы существует короткое опровержение методом резолюций, то для отрицания этой формулы существует не слишком длинный вывод в ИВ.

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

Отметим, что неизвестен эффективный алгоритм поиска кратчайшего вывода в исчислении высказываний, причём скорее всего такого алгоритма и вовсе не существует.

Задачи.

• 1.27. Докажите выполнимость КНФ, которая состоит из 200 дизъюнктов, каждый из которых содержит 8 различных литералов.
• 1.28. Назовём КНФ С замкнутой по длине, если она нс содержит пустого дизъюнкта, а резольвента любых её двух дизъюнктов (1) либо тавтологична; (2) либо содержится в КНФ; (3) либо содержит больше литералов, чем любой дизъюнкт из С. Приведите пример замкнутой по длине невыполнимой КНФ с 2,71 — 1 переменными, все дизъюнкты которой содержат не более п литералов (п ^ 3).
• 1.29. Проверьте методом резолюций выполнимость КНФ