Изменения

*'''Шаг 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>0</tex> станет равна <tex>1</tex>, либо мы рассмотрим переменную без отрицания как они уже не влияют на существование ответаотдельно стоящую переменную. Значит <tex>1</tex> шаг алгоритма выполнится верно. Проделаем с полученным выражением алгоритм, начиная с <tex>1</tex> шага, пока <tex>1</tex> шаг не найдёт ответ.