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

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

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

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

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

Пример :

[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]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]

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

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

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

Пример:

[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]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]

См.также

• СКНФ
• 2-SAT(КНФ в форме Крома)