Изменения
→КНФ в форме Хорна
__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'') {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких ровно двух литералов, количество которых не превышает двух.}}
'''Пример :'''
<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= Существует алгоритм, который за полиномиальное время проверяет, что формулу, заданную в форме Крома , можно удовлетворить.}}|proof= {{main|2SAT}}}}
{{Утверждение
|statement=Функцию <tex>\mathbb{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'') {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.}}
'''Пример:'''
<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= Далее будет приведено доказательство, предлагающее алгоритм решения.
*'''Шаг 2.''' Идем по скобкам *:Опустим одиночно стоящие переменные и выписываем все встречающиеся нам переменныескобки, в которых значение стало равным <tex>1</tex>. Перейдём к <tex>1</tex> шагу алгоритма. По определению формы Хорна, кроме техв каждой из скобок, с которыми где мы работали на предыдущем шагеопустили переменную, не больше <tex>1</tex> переменной без отрицания. Если переменная всегда входит без отрицанийЛибо какая-то из переменных внутри скобки будет иметь отрицание, присваиваем ей значение т.е. при подстановке <tex>0</tex> станет равна <tex>1</tex>, если переменная всегда входит с отрицаниями, присваиваем либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит <tex>01</tex>шаг алгоритма выполнится верно. На данном шаге никакая скобка не может обратиться в Будем проделывать алгоритм, начиная сначала, пока <tex>01</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]]
* [[ДНФ]]
==Примечания==
==Источники информации==
*[https://en.wikipedia.org/wiki/Horn_clause| Conjunctive_normal_form Wikipedia {{---}} Horn clauseCNF]*[https://en.wikipedia.org/wiki/2-satisfiability| Wikipedia {{---}} 2-satisfiability]
[[Категория: Дискретная математика и алгоритмы]]
[[Категория: Булевы функции ]]