Изменения
→КНФ в форме Хорна
__TOC__
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Для двух этих форм существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение <tex>1</tex>, в то время, как для обычной функции, не представленной данной формой, эта задача является [[Примеры NP-полных языков. Теорема Кука|<tex>\mathrm{NP}</tex>-полной]]. Этот факт интересен потому, что, имея большое количество функций, которые можно свести к форме Хорна или Крома, мы сможем гарантированно вычислять необходимое нам условие за полиномиальное время. Поэтому с помощью применения данных форм мы сможем решать очень быстро целый класс задач, например, задачи на графах, которые, как известно, имеют большое практическое применение.
{{Определение
|definition=
'''Конъюнктивная нормальная форма '''(англ. ''conjunctive normal form, CNF'') '''в форме Крома, 2-КНФ<ref>[https://en.wikipedia.org/wiki/2-satisfiability Wikipedia {{---}} 2-satisfiability]</ref>''' (англ. ''2-CNF'') {{---}} конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких ровно двух литералов, число которых не превышает двух.}}
'''Пример :'''
*'''Шаг 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> число вхождений переменных в формулу.
