Изменения

Перейти к: навигация, поиск

Специальные формы КНФ

778 байт добавлено, 18:54, 15 июня 2016
КНФ в форме Хорна
|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(O(n))</tex>, если переменная входит без отрицания и где <tex>0n </tex> иначе. Если после данного этапа какая-либо скобка равна <tex>0</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))</tex>. На данном шаге никакая скобка не может обратиться в <tex>0</tex>. *'''Шаг 3.''' На данном шаге остались переменные, входящие как с отрицаниями, так и без них. Рассмотрим скобки, в которых значение всех переменных или их отрицаний уже равны <tex> 0 </tex> (это возможно только в случае, когда в скобке присутствуют одиночно стоящие переменные из первого шага, или их отрицания). Если рассматриваемая переменная входит без отрицания, то присвоим ей значение <tex> 1</tex>, иначе, присвоим ей <tex> 0 </tex> <tex> (O(n)) </tex>. Если после этого какая-либо скобка обратилось в <tex> 0 </tex>, то решения нет, иначе формула разрешима.
}}
Анонимный участник

Навигация