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