Специальные формы КНФ — различия между версиями
(→КНФ в форме Хорна) |
(→КНФ в форме Крома) |
||
| Строка 16: | Строка 16: | ||
*Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие: | *Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие: | ||
| − | <tex>F(x_1, ..., x_n)=F(y_1, ..., y_n)=F(z_1, ..., z_n)=1\Rightarrow 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) </tex> | + | <tex> F(x_1, ..., x_n)=F(y_1, ..., y_n)=F(z_1, ..., z_n)=1 \Rightarrow</tex> <tex>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)</tex> |
= КНФ в форме Хорна = | = КНФ в форме Хорна = | ||
Версия 11:06, 7 января 2015
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме, то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов.
КНФ в форме Крома
| Определение: |
| Конъюнктивная нормальная форма (КНФ) (англ. conjunctive normal form) в форме Крома (2-КНФ) — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух. |
Пример :
Утверждения:
- Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить(т.е КНФ в форме Крома не является тождественным ).
- Функцию можно задать в форме Крома выполнено следующее следствие:
КНФ в форме Хорна
| Определение: |
| Конъюнктивная нормальная форма (КНФ) (англ. conjunctive normal form) в форме Хорна — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания. |
Пример:
Каждая скобка представляет собой Дизъюнкт Хорна[1].
Любую формулу можно представить в виде КНФ в форме Хорна. Для этого формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме дизьюнкта Хорна.
Утверждения:
- Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
- Функцию можно задать в форме Хорна выполнено следующее следствие:
