Изменения
→КНФ в форме Хорна
*Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
Для начала попробуем найти в данной формуле одиночно стоящие переменные. Например, для формулы <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>, то решения не существует, иначе, решение существует, так как всем остальным переменным мы можем присвоить нужные нам значения так, чтобы в каждом дизъюнкте значение было равно <tex> 1</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> выполнено следующее следствие:
