Изменения
→КНФ в форме Хорна
*'''Шаг 2.'''
*:Опустим одиночно стоящие переменные и скобки, в которых значение стало равным <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 повторение алгоритма мы присваиваем как минимум одной переменной значение и начинаем проделывать алгоритм для оставшихся переменных, если первый шаг не завершил алгоритм. Число вызовов алгоритма с первого шага линейно зависит от того, сколько на 2 этапе алгоритма одиночных переменных, их может быть не больше N. Так как после каждой итерации алгоритма, мы уменьшаем число этих вхождений хотя бы на 1, то суммарно повторов итерации будет не больше <tex>N</tex>.
Каждый из шагов выполняется за время <tex>O(N)</tex>, а подстановок значений в переменные формулы может быть не больше <tex>N</tex> раз, т.к. всего переменных <tex>N</tex>. Получается сложность <tex>O(N^2)</tex>.
}}
