Изменения
→КНФ в форме Хорна
Любую формулу можно представить в виде КНФ в форме Хорна. Для этого формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме дизьюнкта Хорна.
{{Утверждение|about= В данном утверждении будет приведено доказательство, предлагающее алгоритм|statement='''Утверждения:Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.'''|proof=*Шаг 1. Попробуем найти в данной формуле одиночно стоящие переменные. Например, для формулы <tex> x \wedge (x \vee \neg y \vee \neg z) </tex> такой переменной является <tex>x</tex>. Если такие переменные существуют, то им надо присвоить значение <tex> 1 </tex>, если переменная входит без отрицания и <tex>0</tex>, если переменная входит с отрицанием, так как в конъюнкции они должны дать <tex>1</tex>. Заметим, что если какая-либо скобка после этого обратилась в <tex> 0 </tex>, то решения не существует.*Шаг 2. Идем по скобкам и рассматриваем все переменные, встречающиеся более одного раза. Если переменная входит и без отрицания и с отрицанием, то присваиваем ей значение <tex>0</tex>. Если переменная входит всегда без отрицаний, то присваиваем ей значение <tex>1</tex> и <tex>0</tex>, если всегда входит с отрицаниями. *Шаг 3. Присваиваем всем оставшимся переменным <tex>1</tex>, если переменная входит без отрицания и <tex>0</tex> иначе. Если после данного этапа какая-либо скобка равна <tex>0</tex>, то данная формула не разрешима.* Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. Сделав так для каждой скобки, мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в конечном итоге даст нам <tex> 1</tex>.}}
*Функцию <tex>F</tex> можно задать в форме Хорна <tex> \iff </tex> выполнено следующее следствие:
