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