Изменения

Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Эти две формы интересны тем, что для них существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение <tex>1</tex>, в то время, как для обычной функции, не представленной данной формой, эта задача является [[Примеры NP-полных языков. Теорема Кука|NP-полной]].

'''Конъюнктивная нормальная форма (КНФ) в форме Крома (2-КНФ)''' (англ. ''conjunctive normal form'') '''в форме Крома (2-КНФ)'SAT'' ) {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух.}}

'''Конъюнктивная нормальная форма (КНФ)в форме Хорна''' (англ. ''conjunctive normal formHorn clause'') '''в форме Хорна''' {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.}}

* [http://en.wikipedia.org/wiki/2-satisfiability 2-SAT(КНФ в форме Крома)[2SAT]]