Изменения

__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>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= Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна , можно удовлетворить.

Функцию можно представить *'''Шаг 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>. В таком случае дальнейшие шаги выполнять не нужно.

*'''Шаг 12. Одиночное вхождение переменных''' Найдем в данной формуле *:Опустим одиночно стоящие переменные. Напримери скобки, для формулы в которых значение стало равным <tex> x \wedge (x \vee \neg y \vee \neg z) </tex> такой переменной является <tex>x1</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 ... \wedge 1</tex>шаг алгоритма выполнится верно. Будем проделывать алгоритм, что в результате даст нам начиная сначала, пока <tex> 1</tex>. В таком случае дальнейшие шаги выполнять шаг не нужнонайдёт ответ.

*'''Шаг 2.''' Идем по скобкам и выписываем все встречающиеся нам переменные, кроме тех, с которыми мы работали на предыдущем шаге. Если переменная всегда входит без отрицаний, присваиваем ей значение Обозначим за <tex>1N</tex>число вхождений переменных в формулу.Итерация состоит из шагов, если переменная всегда входит с отрицаниями, присваиваем каждый из которых выполняется за <tex>0O(N)</tex>. На данном шаге никакая скобка Всего итераций будет не может обратиться в больше <tex>0N</tex>.  *'''Шаг 3.''' Опустим одиночно стоящие переменные и скобки, в которых значение стало равным 1, так как они уже если первый шаг не влияют на существование ответа. Проделаем с полученным выражением завершил алгоритм, начиная с <tex>1</tex> шага, пока <tex>1</tex> шаг не найдёт ответ. *Время работы алгоритма:Так как функция состоит из простых выражений, мы сможем её разбить то уменьшил размер формулы на дерево за линейное времяодно вхождение.Будем считатьИтого, что длиной формулы является количество переменных, входящих в нее. Обозначим ее за асимптотика алгоритма составляет <tex> n 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>

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