Изменения
→КНФ в форме Хорна
{{Утверждение
|aboutstatement= В данном утверждении будет приведено доказательство, предлагающее алгоритм|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>1</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>.
}}
