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

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

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

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

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

Пример :

[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] F(x_1, ..., x_n)=F(y_1, ..., y_n)=F(z_1, ..., z_n)= 1 \Rightarrow F(\lt x_1, y_1, z_1\gt , \lt x_2, y_2, z_2\gt , ..., \lt x_n, y_n, z_n \gt ) [/math]

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

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

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

Пример:

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