Изменения
→КНФ в форме Хорна
*:Опустим одиночно стоящие переменные и скобки, в которых значение стало равным <tex>1</tex>. Перейдём к <tex>1</tex> шагу алгоритма. По определению формы Хорна, в каждой из скобок, где мы опустили переменную не больше <tex>1</tex> переменной без отрицания. Либо какая-то из переменных внутри скобки будет иметь отрицание, т.е. при подстановке <tex>0</tex> станет равна <tex>1</tex>, либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит <tex>1</tex> шаг алгоритма выполнится верно. Будем проделывать алгоритм, начиная сначала, пока <tex>1</tex> шаг не найдёт ответ.
Обозначим за <tex>N</tex> число переменных, входящих в формулу.Количество повторений алгоритма с <tex>1</tex> шага зависит от того, назовём это число длиной формулысколько у нас в формуле есть различных переменных линейно, т.к. за 1 повторение алгоритма мы присваиваем как минимум одной переменной значение и начинаем проделывать алгоритм для оставшихся переменных.Каждый из шагов выполняется за время <tex>O(N)</tex>, а подстановок значений в переменные формулы может быть не больше <tex>N</tex> раз, т.к. мы присваиваем каждой переменной значение один развсего переменных <tex>N</tex>. Получается сложность <tex>O(N^2)</tex>.
}}
{{Утверждение
