Существует два способа представления формулы,заданной в конъюнктивной нормальной форме(КНФ,Conjunctive Normal Form,CNF),т.е имеющей вид конъюнкции выражений в скобках(clauses),каждое из которых представляет собой дизъюнкцию одного или нескольких литералов:__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-Sat,satisfiability]</ref>''' (англ. ''2-CNF'') {{---}} конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию ровно двух литералов.}} '''Пример :''' <tex>(x_1\vee\overline x_2) \wedge (\overline x_1 \vee x_3 ) \wedge (\overline x_3 \vee x_2 ) \wedge (\overline x_1 \vee \overline x_2) \wedge\ldots </tex> {{Утверждение|statement= Существует алгоритм, который за полиномиальное время проверяет, что формулу, заданную в форме Крома, можно удовлетворить.}}{{main|2SAT}}
*КНФ в форме Хорна(Horn clause)
{{Утверждение
|statement=Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие : <tex> F(x_1, \ldots, x_n)=F(y_1, \ldots, y_n)=F(z_1, \ldots, z_n)=1 \Rightarrow</tex> <tex>F(\langle x_1, y_1, z_1 \rangle, \langle x_2, y_2, z_2 \rangle, \ldots, \langle x_n, y_n, z_n \rangle)</tex>
}}
== КНФ в форме Хорна ==
== КНФ в форме Крома ==
{{Определение
|definition=
'''Конъюнктивной нормальной формойКонъюнктивная нормальная форма '''(КНФангл. ''conjunctive normal form, CNF'') '''в форме КромаХорна<ref>[https://en.wikipedia.org/wiki/Horn_clause Wikipedia {{---}} Horn clause]</ref>''' (англ. ''Horn clause'') {{- --}} это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию нескольких литералов,количество которых в которой присутствует не превышает 2х. Эта же такая форма называется 2-CNF (2-conjunctive normal form)более одного литерала без отрицания.}}
'''Пример:'''
<math>(A \or \neg B) \and (\neg A \or C ) \and (\neg C \or B ) \and (\neg A \or \neg C ) \cdots </math>
В такой форме можно представить задачу 2<tex> (\overline x_1 \vee \overline x_2 \vee \ldots \vee \overline x_n ) \wedge (x_1 \vee \overline x_2 \vee \ldots \vee \overline x_n)\wedge \ldots</tex> Каждая скобка представляет собой Дизъюнкт Хорна<ref>[https://ru.wikipedia.org/wiki/%D0%94%D0%B8%D0%B7%D1%8A%D1%8E%D0%BD%D0%BA%D1%82_%D0%A5%D0%BE%D1%80%D0%BD%D0%B0 Википедия {{--SAT (2-satisfiability}} Дизъюнкт Хорна]</ref>. {{Утверждение|statement= Существует алгоритм,задача распределения значений булевым переменным таким образомкоторый за полиномиальное время проверяет, чтобы они удовлетворяли всем наложенным ограничениям).Алгоритм для решения 2-SAT может быть применим во всех задачахчто функцию, где есть набор величинзаданную в форме Хорна, каждая из которых может принимать 2 возможных значенияможно удовлетворить.|proof= Далее будет приведено доказательство, и есть связи между этими величинамипредлагающее алгоритм решения.
== КНФ в форме Хорна =={{Определение|definition=*'''Шаг 1. Одиночное вхождение переменных.'''Конъюнктивной нормальной формойНайдем в данной формуле одиночно стоящие переменные. Например, для формулы <tex> x \wedge (КНФx \vee \neg y \vee \neg z) </tex> такой переменной является <tex>x</tex>. *# Присутствуют одиночно стоящие переменные.*#:Присвоим всем таким переменным значение <tex> 1 </tex>, если переменная входит без отрицания и <tex>0</tex> иначе, так как в форме Хорна''' конъюнкции они должны дать <tex>1</tex>. Заметим, что если какая- это конъюнкция выражений либо скобка после этого обратилась в скобках<tex> 0 </tex>,каждое то решения не существует. *# Отсутствуют одиночно стоящие переменные. *#:Всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из которых представляет собой дизъюнкцию литералов(literalтого,что в каждом дизъюнкте есть хотя бы одна переменная или ее отрицание)с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. В итоге мы получим выражение вида: <tex>1\wedge 1 \wedge \ldots \wedge 1</tex>,что в которой присутствует результате даст нам <tex> 1</tex>. В таком случае дальнейшие шаги выполнять не более одного неотрицательного литераланужно.}}
Пример*'''Шаг 2.''' *:Опустим одиночно стоящие переменные и скобки, в которых значение стало равным <tex>1</tex>. Перейдём к <tex>1</tex> шагу алгоритма. По определению формы Хорна, в каждой из скобок, где мы опустили переменную, не больше <tex>1</tex> переменной без отрицания. Либо какая-то из переменных внутри скобки будет иметь отрицание, т.е. при подстановке <tex>0</tex> станет равна <tex>1</tex>, либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит <tex>1</tex> шаг алгоритма выполнится верно. Будем проделывать алгоритм, начиная сначала, пока <mathtex> (\neg A \or \neg B \vee \cdots \or \neg C ) \and (A \or \neg B \vee \cdots \or \neg C)1</mathtex>шаг не найдёт ответ.
Каждая скобка Обозначим за <tex>N</tex> число вхождений переменных в формулу.Итерация состоит изшагов, каждый из которых выполняется за <tex>O(N)</tex>. Всего итераций будет не больше <tex>N</tex>,так называемых дизъюнктов Хорнакак если первый шаг не завершил алгоритм, то уменьшил размер формулы на одно вхождение.Дизъюнкт с ровно одним положительным литералом называется ''определенным'' дизъюнктомИтого, асимптотика алгоритма составляет <tex>O(N^2)</tex>.Дизъюнкт без положительных литералов иногда называется ''целью'' или ''запросом''}}{{Утверждение|statement=Функцию <tex>F</tex> можно задать в форме Хорна <tex> \iff </tex> выполнено следующее следствие:<tex> F(конкретно в логическом программированииx_1, \ldots, x_n)=F(y_1, \ldots, y_n)=1 \Rightarrow F(x_1 \wedge y_1, x_2 \wedge y_2, \ldots, x_n \wedge y_n).</tex>}}
Дизъюнкты Хорна могут быть пропозициональными формулами, либо формулами первого порядка, в зависимости от того, рассматриваются ли пропозициональные литералы(значением которых может быть логическое высказывание) или литералы первого порядка== См.также ==* [[СКНФ]]* [[2SAT]]* [[ДНФ]]
Пропозициональные дизъюнкты Хорна также представляют интерес для теории сложности вычислений, где задача поиска множества истинностных значений, выполняющих КНФ в форме Хорна, является P-полной.Задача выполнимости дизъюнктов Хорна первого порядка не разрешима.==Примечания==
Любую формулу можно представить в виде КНФ в форме Хорна.Для этого любую формулу необходимо преобразовать в КНФ(конъюнкцию элементарных дизъюнкций) и далее каждую дизъюнкцию представить в форме Хорна.<references />
Пример: Пусть нам дано выражение ( ¬ A v (B ^ D) ≡ B → C )==Источники информации==Тогда*[https: ¬ A v (B ^ D) ≡(¬A v B) ^ (¬A v D)//en.wikipedia.org/wiki/Conjunctive_normal_form Wikipedia {{---}} CNF]
B→C ≡¬B v C
(¬A v B) ^ (¬A v D) ≡ (¬B v C) - в форме Хорна.[[Категория: Дискретная математика и алгоритмы]]
== См.также ==[[СКНФКатегория: Булевы функции ]]
