Специальные формы КНФ

Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме, то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Эти две формы интересны тем, что для них существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение [math]1[/math], в то время, как для обычной функции, не представленной данной формой, эта задача является NP-полной.

КНФ в форме Крома

Определение:

Конъюнктивная нормальная форма (КНФ) в форме Крома (2-КНФ) (англ. 2-CNF) — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух.

Пример :

[math](x_1\vee\overline x_2) \wedge (\overline x_1 \vee x_3 ) \wedge (\overline x_3 \vee x_2 ) \wedge (\overline x_1 \vee \overline x_2) \wedge... [/math]

Утверждения:

• Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить (т.е КНФ в форме Крома не является тождественным [math]0[/math]).

Для начала приведем данное выражение к импликативной форме следующим образом: заметим, что выражение вида [math] a \vee b [/math] эквивалентно [math] \neg a \Rightarrow b \vee \neg b \Rightarrow a [/math]. Это можно воспринимать следующим образом: если есть выражение [math] a \vee b [/math], и нам необходимо добиться обращения его в [math] true [/math] то, если [math] a = true [/math], [math] b [/math] должно быть равно [math] false [/math] и наоборот. Построим граф импликаций, для каждой переменной в паре будет по две вершины (обозначим их [math] x [/math] и [math] \neg x [/math]). Рёбра в графе будут соответствовать импликативным связям. Например, для формулы вида: [math] (a \vee b) \wedge (a \vee \neg b) [/math] граф импликаций будет содержать следующие ориентированные ребра: [math] \neg a \rightarrow b, \neg b \rightarrow a, \neg b \rightarrow \neg c, c \rightarrow b [/math]. Заметим, что если для какой-то вершины [math] x [/math] выполняется, что из [math] x [/math] достижима [math] \neg x [/math], а из [math] \neg x [/math] достижима [math] x [/math], то задача не имеет решения.Это следует из того, что какое бы значение для переменной [math] x [/math] мы бы ни выбрали, мы всегда придём к противоречию, что должно быть выбрано и обратное ему значение. Условие не существования таких вершин является необходимым и достаточным для решения данной задачи. Переформулируем утверждение в терминах теории графов: для решения данной задачи необходимо и достаточно, чтобы [math] \forall x [/math] вершины [math] x [/math] и [math] \neg x [/math] находились в разных компонентах сильной связности графа импликаций.

• Функцию [math]F[/math] можно задать в форме Крома [math] \iff [/math] выполнено следующее следствие:

[math] F(x_1, ..., x_n)=F(y_1, ..., y_n)=F(z_1, ..., z_n)=1 \Rightarrow[/math] [math]F(\langle x_1, y_1, z_1 \rangle, \langle x_2, y_2, z_2 \rangle, ..., \langle x_n, y_n, z_n \rangle)[/math]

КНФ в форме Хорна

Определение:

Конъюнктивная нормальная форма (КНФ)в форме Хорна (англ. Horn clause) — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.

Пример:

[math] (\overline x_1 \vee \overline x_2 \vee ... \vee \overline x_n ) \wedge (x_1 \vee \overline x_2 \vee ... \vee \overline x_n)\wedge ...[/math]

Каждая скобка представляет собой Дизъюнкт Хорна.

Любую формулу можно представить в виде КНФ в форме Хорна. Для этого формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме дизьюнкта Хорна.

Утверждения:

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

Для начала попробуем найти в данной формуле одиночно стоящие переменные. Например, для формулы [math] x \wedge (x \vee \neg y \vee \neg z) [/math] такой переменной является [math]x[/math]. Если такие переменные существуют, то им надо присвоить значение [math] 1 [/math], если переменная входит без отрицания и [math]0[/math], если переменная входит с отрицанием, так как в конъюнкции они должны дать [math]1[/math]. Далее, если какая-либо скобка обратилась в [math] 0 [/math], то решения не существует, иначе, решение существует, так как всем остальным переменным мы можем присвоить нужные нам значения так, чтобы в каждом дизъюнкте значение было равно [math] 1[/math]. Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение [math] 0 [/math] и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение [math]0[/math] мы получим [math] 1[/math] в результате дизъюнкции. Сделав так для каждой скобки, мы получим выражение вида: [math]1\wedge 1 \wedge ... \wedge 1[/math], что в конечном итоге даст нам [math] 1[/math].

• Функцию [math]F[/math] можно задать в форме Хорна [math] \iff [/math] выполнено следующее следствие:

[math] F(x_1, ..., x_n)=F(y_1, ..., y_n)=1 \Rightarrow F(x_1 \wedge y_1, x_2 \wedge y_2, ..., x_n \wedge y_n)[/math]

См.также

• СКНФ
• 2SAT

Источники информации

• Wikipedia — Horn clause
• Wikipedia — 2-satisfiability