Изменения
→КНФ в форме Хорна
{{Утверждение
|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>, то решения не существует <tex>(O(n))</tex>, где <tex> n </tex> - длина формулы.
* Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. Сделав так для каждой скобки, мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в конечном итоге даст нам <tex> 1</tex> В таком случае дальнейшие шаги выполнять не нужно.
*'''Шаг 2.''' Идем по скобкам и выписываем все встречающиеся нам переменные, кроме тех, с которыми мы работали на предыдущем шаге. Если переменная всегда входит всегда без отрицаний, то присваиваем ей значение <tex>1</tex> и <tex>0</tex>, если переменная всегда входит с отрицаниями , присваиваем <tex>(O(n))0</tex>. На данном шаге никакая скобка не может обратиться в <tex>0</tex>. *'''Шаг 3.''' На данном шаге остались переменные, не являющиеся одиночно стоящими и входящие как с отрицаниями, так и без них. Рассмотрим скобки, в которых значение всех рассмотренных ранее переменных или их отрицаний уже равны <tex> 0 </tex> (это возможно только в случае, когда в скобке присутствуют одиночно стоящие переменные из первого шага, или их отрицания). Рассматриваемые на данном шаге переменные в такой скобке могут входить с отрицанием и без него. Если рассматриваемая переменная входит без отрицания, то присвоим ей значение <tex> 1</tex>, иначе, присвоим ей <tex> 0 </tex> <tex> (O(n)) </tex>. Если после этого какая-либо скобка обратилось в <tex> 0 </tex>, то решения нет, иначе формула разрешима. *Время работы алгоритма:Будем считать, что длина формулы - количество символов, входящих в данную формулу. Обозначим ее за <tex> n </tex>.*'''Шаг 1.''' На данном шаге мы делаем один проход по формуле, ища одиночно стоящие переменные. Следовательно, время работы первого шага <tex> (O(n)) </tex>.*'''Шаг 2.''' На данном шаге мы за линейное время мы проходим по формуле и помечаем все переменные, которые входят либо только без отрицаний либо только с отрицаниями и после этого присваиваем им нужные значения. Время работы данного шага <tex> (O(n)) </tex>.*'''Шаг 3.''' На данном шаге мы также делаем один проход по формуле и присваиваем нужные значения оставшимся переменным. Время работы данного шага также <tex> (O(n)) </tex>.*Итого, время работы данного алгоритма линейное.
}}
{{Утверждение
|statement=Функцию <tex>F</tex> можно задать в форме Хорна <tex> \iff </tex> выполнено следующее следствие:<tex> F(x_1, ..., x_n)=F(y_1, ..., y_n)=1 \Rightarrow F(x_1 \wedge y_1, x_2 \wedge y_2, ..., x_n \wedge y_n)</tex>
