Изменения

*Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#КНФ Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в форме Крома|КНФ скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Для двух этих форм существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение <tex>1</tex>, в форме Крома(2-КНФто время, как для обычной функции, не представленной данной формой,2эта задача является [[Примеры NP-Sat,2полных языков. Теорема Кука|<tex>\mathrm{NP}</tex>-CNF)полной]]. Этот факт интересен потому, что, имея большое количество функций, которые можно свести к форме Хорна или Крома, мы сможем гарантированно вычислять необходимое нам условие за полиномиальное время. Поэтому с помощью применения данных форм мы сможем решать очень быстро целый класс задач, например, задачи на графах, которые, как известно, имеют большое практическое применение.

*[[#== КНФ в форме ХорнаКрома =={{Определение|КНФ definition='''Конъюнктивная нормальная форма '''(англ. ''conjunctive normal form, CNF'') '''в форме ХорнаКрома, 2-КНФ<ref>[https://en.wikipedia.org/wiki/2-satisfiability Wikipedia {{---}} 2-satisfiability]</ref>''' (Horn clauseангл. ''2-CNF'')]]{{---}} конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию ровно двух литералов.}}

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

В такой {{Утверждение|statement=Функцию <tex>F</tex> можно задать в форме можно представить задачу 2-SAT Крома <tex> \iff </tex> выполнено следующее следствие : <tex> F(x_1, \ldots, x_n)=F(y_1, \ldots, y_n)=F(2-satisfiabilityz_1,задача распределения значений булевым переменным таким образом\ldots, чтобы они удовлетворяли всем наложенным ограничениямz_n).Алгоритм для решения 2-SAT может быть применим во всех задачах=1 \Rightarrow</tex> <tex>F(\langle x_1, где есть набор величинy_1, каждая из которых может принимать 2 возможных значенияz_1 \rangle, и есть связи между этими величинами.\langle x_2, y_2, z_2 \rangle, \ldots, \langle x_n, y_n, z_n \rangle)</tex>}}

'''Конъюнктивной нормальной формойКонъюнктивная нормальная форма '''(КНФангл. ''conjunctive normal form, CNF'') '''в форме Хорна<ref>[https://en.wikipedia.org/wiki/Horn_clause Wikipedia {{---}} Horn clause]</ref>''' (англ. ''Horn clause'' ) {{--- }} это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию литералов(literal,переменная или ее отрицание),в которой присутствует не более одного неотрицательного литералабез отрицания.}}

<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 Википедия {{---}} Дизъюнкт Хорна]</ref>. {{Утверждение|statement= Существует алгоритм, который за полиномиальное время проверяет, что функцию,так называемых дизъюнктов заданную в форме Хорна, можно удовлетворить.Дизъюнкт с ровно одним положительным литералом называется |proof= Далее будет приведено доказательство, предлагающее алгоритм решения. *'''Шаг 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> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <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> шаг алгоритма выполнится верно. Будем проделывать алгоритм, начиная сначала, пока <tex>1</tex> шаг не найдёт ответ. Обозначим за <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]]* [[ДНФ]]

'''Пример:''' Пусть нам дано выражение ( ¬ 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]

== См.также ==[[СКНФКатегория: Булевы функции ]]