45
правок
Изменения
→КНФ в форме Хорна
*:Опустим одиночно стоящие переменные и скобки, в которых значение стало равным <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>O(N)</tex>, так как найти одиночно стоящие переменные можно за линейный проход.
