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