Изменения

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

'''Конъюнктивная нормальная форма '''(КНФангл. ''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=Существует алгоритм, который за полиномиальное время проверяет, что функциюформулу, заданную в форме Крома , можно удовлетворить (т.е КНФ в форме Крома не является тождественно равной <tex>0</tex>).}}{{main|proof=Данный алгоритм подробно описан в статье о выполнимости булевых формул, заданных в форме Крома: [[2SAT]].}} 

|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>

== КНФ в форме Хорна ==

'''Конъюнктивная нормальная форма '''(КНФангл. ''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= Далее будет приведено доказательство, предлагающее алгоритм решения.

{{Утверждение|about= В данном утверждении будет приведено доказательство, предлагающее алгоритм|statement=*'''Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворитьШаг 1. Одиночное вхождение переменных.'''|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>, то решения не существует.*Шаг 2# Отсутствуют одиночно стоящие переменные. Идем по скобкам *#:Всем переменным надо присвоить значение <tex> 0 </tex> и рассматриваем все переменныебулева формула разрешится. Это следует из того, встречающиеся более одного раза. Если что в каждом дизъюнкте есть хотя бы одна переменная входит и без отрицания и с отрицанием, то присваиваем ей подставив в нее значение <tex>0</tex> мы получим <tex>1</tex>в результате дизъюнкции. Если переменная входит всегда без отрицаний, то присваиваем ей значение В итоге мы получим выражение вида: <tex>1\wedge 1 \wedge \ldots \wedge 1</tex> и , что в результате даст нам <tex>01</tex>, если всегда входит с отрицаниями. В таком случае дальнейшие шаги выполнять не нужно.  *'''Шаг 32. Присваиваем всем оставшимся переменным ''' *:Опустим одиночно стоящие переменные и скобки, в которых значение стало равным <tex>1</tex>. Перейдём к <tex>1</tex>шагу алгоритма. По определению формы Хорна, если переменная входит в каждой из скобок, где мы опустили переменную, не больше <tex>1</tex> переменной без отрицания и . Либо какая-то из переменных внутри скобки будет иметь отрицание, т.е. при подстановке <tex>0</tex> иначе. Если после данного этапа какая-либо скобка станет равна <tex>01</tex>, то данная формула не разрешималибо мы рассмотрим переменную без отрицания как отдельно стоящую переменную.* Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение Значит <tex> 0 1</tex> и булева формула разрешитсяшаг алгоритма выполнится верно. Это следует из тогоБудем проделывать алгоритм, что в каждом дизъюнкте есть хотя бы одна переменная с отрицаниемначиная сначала, подставив в нее значение пока <tex>01</tex> мы получим шаг не найдёт ответ. Обозначим за <tex> 1N</tex> число вхождений переменных в результате дизъюнкцииформулу. Сделав так для каждой скобкиИтерация состоит из шагов, мы получим выражение вида: каждый из которых выполняется за <tex>O(N)</tex>1\wedge 1 \wedge ... \wedge 1Всего итераций будет не больше <tex>N</tex>, что в конечном итоге даст нам так как если первый шаг не завершил алгоритм, то уменьшил размер формулы на одно вхождение. Итого, асимптотика алгоритма составляет <tex> 1O(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>

*[https://en.wikipedia.org/wiki/Horn_clause| Conjunctive_normal_form Wikipedia {{---}} Horn clauseCNF]*[https://en.wikipedia.org/wiki/2-satisfiability| Wikipedia {{---}} 2-satisfiability]