45
правок
Изменения
→КНФ в форме Хорна
|statement= Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
|proof= Далее будет приведено доказательство, предлагающее алгоритм решения.
Функцию можно представить в любом виде. Например, можно использовать древовидную структуру. Для формулы <tex> x \wedge (x \vee \neg y \vee \neg z) </tex>, которую мы будем использовать далее, дерево может выглядеть так :[[Файл:Tree_structure.png]]
*'''Шаг 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>, то решения не существует. Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. В итоге мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в результате даст нам <tex> 1</tex>. В таком случае дальнейшие шаги выполнять не нужно.
*'''Шаг 3.''' Опустим одиночно стоящие переменные и скобки, в которых значение стало равным 1, так как они уже не влияют на существование ответа. Проделаем с полученным выражением алгоритм, начиная с <tex>1</tex> шага, пока <tex>1</tex> шаг не найдёт ответ.
