Специальные формы КНФ — различия между версиями
Rybak (обсуждение | вклад) м |
Rybak (обсуждение | вклад) (→КНФ в форме Крома) |
||
| Строка 15: | Строка 15: | ||
| − | *Функцию <tex>F</tex> можно задать в форме Крома | + | *Функцию <tex>F</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 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> | ||
| − | |||
= КНФ в форме Хорна = | = КНФ в форме Хорна = | ||
Версия 01:35, 25 сентября 2011
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме, то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов:
КНФ в форме Крома
| Определение: |
| Конъюнктивная нормальная форма(КНФ) в форме Крома - это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух. |
Пример :
Утверждения:
- Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить(т.е КНФ в форме Крома не является тождественным ).
- Функцию можно задать в форме Крома, тогда и только когда выполнено следующее следствие :
КНФ в форме Хорна
| Определение: |
| Конъюнктивная нормальная форма(КНФ) в форме Хорна - это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания. |
Пример:
Каждая скобка представляет собой Дизъюнкт Хорна.
Любую формулу можно представить в виде КНФ в форме Хорна. Для этого формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме дизьюнкта Хорна.
Утверждения:
- Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
- Функцию можно задать в форме Хорна когда выполнено следующее следствие :
