Изменения

*Найдем в данной формуле одиночно стоящие переменные. Например, для формулы <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> . В таком случае дальнейшие шаги выполнять не нужно. 

Будем считать, что длиной формулы является количество символовпеременных, входящих в нее. Обозначим ее за <tex> n </tex>.*'''Шаг 1.''' На данном В каждом шаге мы делаем один проход проходимся по формуле, ища одиночно стоящие переменные. Следовательно, время работы первого шага <tex> (O(n)) </tex>.*'''Шаг 2.''' На данном шаге мы за линейное время мы проходим по формуле и помечаем все переменные, которые входят либо только без отрицаний либо только с отрицаниями всем переменным и после этого присваиваем им нужные значениянекоторым из них какое-то значение. Время работы данного шага <tex> (O(n)) </tex>.*'''Шаг 3.''' На данном шаге мы также делаем один проход по формуле и присваиваем нужные значения оставшимся переменным. Время работы данного шага также <tex> (O(n)) </tex>.*ИтогоОтсюда следует, что время работы данного алгоритма линейное, относительно количества входящих переменных.