Изменения

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

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

{{Утверждение|statement= Существует алгоритм, который за полиномиальное время проверяет, что формулу, заданную в форме Крома, можно удовлетворить.}}{{main|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>}} == КНФ в форме Крома Хорна == {{Определение|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)более одного литерала без отрицания.}} '''Пример:'''

Пример:<mathtex>(A \or overline x_1 \neg Bvee \overline x_2 \vee \ldots \vee \overline x_n ) \and wedge (x_1 \neg A vee \or C ) overline x_2 \vee \and (ldots \neg C vee \or B overline x_n) \cdots wedge \ldots</mathtex>

В такой форме можно представить задачу 2Каждая скобка представляет собой Дизъюнкт Хорна<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,задача распределения значений булевым переменным таким образом, чтобы они удовлетворяли всем наложенным ограничениям).Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами(к примеру,такие как нахождение такого расположения меток на диаграмме, при котором никакие две не пересекаются и т.д.)}} Дизъюнкт Хорна]</ref>.

== КНФ в форме Хорна ==*'''Конъюнктивной нормальной формой(КНФ) в форме ХорнаШаг 2.''' - это конъюнкция выражений *:Опустим одиночно стоящие переменные и скобки, в скобкахкоторых значение стало равным <tex>1</tex>. Перейдём к <tex>1</tex> шагу алгоритма. По определению формы Хорна,каждое в каждой из которых представляет собой дизъюнкцию литералов(literalскобок, где мы опустили переменную,переменная или ее не больше <tex>1</tex> переменной без отрицания. Либо какая-то из переменных внутри скобки будет иметь отрицание),в которой присутствует т.е. при подстановке <tex>0</tex> станет равна <tex>1</tex>, либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит <tex>1</tex> шаг алгоритма выполнится верно. Будем проделывать алгоритм, начиная сначала, пока <tex>1</tex> шаг не более одного неотрицательного литераланайдёт ответ.

Пример:Обозначим за <tex>N</tex> число вхождений переменных в формулу.Итерация состоит из шагов, каждый из которых выполняется за <mathtex> O(N)</tex>. Всего итераций будет не больше <tex>N</tex>, так как если первый шаг не завершил алгоритм, то уменьшил размер формулы на одно вхождение. Итого, асимптотика алгоритма составляет <tex>O(N^2)</tex>.}}{{Утверждение|statement=Функцию <tex>F</tex> можно задать в форме Хорна <tex> \neg A iff </tex> выполнено следующее следствие:<tex> F(x_1, \or \neg B ldots, x_n)=F(y_1, \vee \cdots \or \neg C ldots, y_n) =1 \and Rightarrow F(A x_1 \wedge y_1, x_2 \or \neg B wedge y_2, \vee \cdots ldots, x_n \or \neg Cwedge y_n)</mathtex>}}

Каждая скобка состоит из,так называемых дизъюнктов Хорна.Дизъюнкт с ровно одним положительным литералом называется ''определенным'' дизъюнктом.Дизъюнкт без положительных литералов иногда называется ''целью'' или ''запросом''(конкретно в логическом программировании)== См.также ==* [[СКНФ]]* [[2SAT]]* [[ДНФ]]

Любую формулу можно представить в виде КНФ в форме Хорна==Источники информации==*[https://en.Для этого любую формулу необходимо преобразовать в КНФ(конъюнкцию элементарных дизъюнкций) и далее каждую дизъюнкцию представить в форме Хорнаwikipedia.org/wiki/Conjunctive_normal_form Wikipedia {{---}} CNF]