Резолютивный вывод. 
Дискретный анализ. 
Формальные системы и алгоритмы

Далее в этом разделе мы рассматриваем вопрос о выполнимости КНФ.

Поскольку а V а ~ а Л а ~ а, мы предполагаем в дальнейшем, что все дизъюнкты не содержат повторений литералов и попарно различны. Другими словами это означает, что мы представляем КНФ как совокупность различных дизъюнктов D1,…, D_n, каждый из которых в свою очередь является множеством различных литералов. Для удобства будем допускать и пустое множество литералов, которому соответствует тождественно ложный пустой дизъюнкт. Далее в этом разделе мы всюду говорим о дизъюнктах как о множествах литералов.

Определение 1.41. Резольвентой пары дизъюнктов вида {т} U А и {1т} U D относительно переменной х называется дизъюнкт A U В. Здесь {т^а} обозначает дизъюнкт, состоящий в точности из литерала х^а.

Заметим, что если А и В содержат пару противоположных литералов у и 1 у, то резольвента A U В является тавтологией.

Определение 1.42. Пусть V — множество дизъюнктов. Резолютивный вывод дизъюнкта D из V — это такая последовательность дизъюнктов R,…, R_n, что R_n = D и каждый член /?_?; этой последовательности либо принадлежит V, либо является резольвентой каких-то предыдущих дизъюнктов Rj, Rk, j, k < i.

Резолютивный вывод пустого дизъюнкта из V называется опровержением V. (Как будет показано ниже, опровержение является фактически доказательством невыполнимости V.)

Теорема 1.43 (корректность метода резолюций). Если существует резолютивный вывод пустого дизъюнкта из дизъюнктов КНФ С, то КНФ невыполнима.

Доказательство. Пусть КНФ V' получена из КНФ V добавлением резольвенты пары дизъюнктов {т}иА и {1т}UВ, которые входят в V.

Выполнимость V равносильна выполнимости V, так как формулы (xVA)A (IxVjB) и (х/Л)Л (1х/Б)Л (Л/Б) эквивалентны: чтобы первая формула была истинной, должна быть истинна одна из формул А или В. Это означает, что добавление к КНФ дизъюнктов любого резолютивного вывода из множества дизъюнктов этой КНФ не меняет выполнимости КНФ. Поэтому из резолютивного вывода пустого дизъюнкта следует невыполнимость КНФ. ?

Назовём множество дизъюнктов V полным непротиворечивым, если V не содержит пустого дизъюнкта и любая резольвента дизъюнктов из V либо тавтологична, либо содержится в V.

Лемма 1.44. КНФ с полным непротиворечивым множестволь дизъюнктов выполнима.

Доказательство. Конъюнкция ложна, если ложен хотя бы один её член. Поэтому знания значений части переменных КНФ бывает достаточно, чтобы сделать вывод о ложности КНФ на таком частично определённом наборе значений. Точнее говоря, если известно, что ложны литералы ?,…, ?k и в КНФ входит дизъюнкт D С {?,… ,?k}, то КНФ ложна.

Построим выполняющий набор для полного непротиворечивого множества дизъюнктов V. Будем присваивать значения переменным, но очереди. Для г = 1,…, п полагаем Xi = 1, если на частично определённом наборе значений х = ai, …, xi-1 = 1, xi = О КНФ ложна; в противном случае полагаем Х{ = 0. Заметим, что это правило применимо и к первой переменной.

Предположим, что КНФ ложна на построенном наборе значений а. Выберем наименьшее к, для которого КНФ ложна на (частичном) наборе Х{ = a*, i = 0,…, к (случай г = 0 отвечает пустому частичному набору, в котором ни одной переменной не присвоено значения). По построению это означает, что КНФ ложна на обоих наборах …, оц., О и Of 1, а*, 1. Поэтому найдутся такие дизъюнкты D2 из Р, что

В силу выбора к ни один дизъюнкт из V не содержится в множестве L = {x^ai,…, х^^к } (иначе КНФ была бы ложна на более коротком частичном наборе значений переменных). С другой стороны, D содержит rr^+i, Р2 содержит lxk+i, а их резольвента относительно Xk+i содержится в L. Эта резольвента нетавтологична в силу выбора D, D? и не принадлежит V. Получили противоречие с полнотой Р, которое и доказывает истинность КНФ на построенном наборе значений а. ?

Теорема 1.45 (полнота метода резолюций). Если КНФ С невыполнима, то существует резолютивный вывод пустого дизъюнкта из дизъюнктов КНФ С.

Доказательство. Рассуждаем следующим образом. Выводим из дизъюнктов С все возможные резольвенты, пока это возможно и не выведен пустой дизъюнкт. Если процесс завершится выводом пустого дизъюнкта, то мы получили искомый резолютивный вывод. В противном случае процесс остановится на полном непротиворечивом множестве дизъюнктов, которое выполнимо в силу предыдущей леммы. ?