Специальные формы КНФ — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(КНФ в форме Крома)
м (rollbackEdits.php mass rollback)
 
(не показано 66 промежуточных версий 10 участников)
Строка 1: Строка 1:
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Эти две формы интересны тем, что для них существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение <tex>1</tex>, в то время, как для обычной функции, не представленной данной формой, эта задача является [[Примеры NP-полных языков. Теорема Кука|NP-полной]].  
+
__TOC__
 +
 
 +
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Для двух этих форм существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение <tex>1</tex>, в то время, как для обычной функции, не представленной данной формой, эта задача является [[Примеры NP-полных языков. Теорема Кука|<tex>\mathrm{NP}</tex>-полной]]. Этот факт интересен потому, что, имея большое количество функций, которые можно свести к форме Хорна или Крома, мы сможем гарантированно вычислять необходимое нам условие за полиномиальное время. Поэтому с помощью применения данных форм мы сможем решать очень быстро целый класс задач, например, задачи на графах, которые, как известно, имеют большое практическое применение.
  
 
== КНФ в форме Крома ==
 
== КНФ в форме Крома ==
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
'''Конъюнктивная нормальная форма (КНФ) в форме Крома (2-КНФ)''' (англ. ''2-CNF'') {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух.}}
+
'''Конъюнктивная нормальная форма '''(англ. ''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... </tex>
+
<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= Существует алгоритм, который за полиномиальное время проверяет, что формулу, заданную в форме Крома, можно удовлетворить.}}
 +
{{main|2SAT}}
  
*Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить (т.е КНФ в форме Крома не является тождественно равной <tex>0</tex>).
 
[[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>
 +
}}
  
*Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие:
+
== КНФ в форме Хорна ==
 
 
<tex> F(x_1, ..., x_n)=F(y_1, ..., y_n)=F(z_1, ..., z_n)=1 \Rightarrow</tex>  <tex>F(\langle x_1, y_1, z_1 \rangle, \langle x_2, y_2, z_2 \rangle, ..., \langle x_n, y_n, z_n \rangle)</tex>
 
 
 
= КНФ в форме Хорна =
 
  
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
'''Конъюнктивная нормальная форма (КНФ)в форме Хорна''' (англ. ''Horn clause'')  {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.}}
+
'''Конъюнктивная нормальная форма '''(англ. ''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 ... \vee \overline x_n ) \wedge (x_1  \vee \overline x_2  \vee ... \vee \overline x_n)\wedge ...</tex>
+
<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>.
+
Каждая скобка представляет собой Дизъюнкт Хорна<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> x \wedge (x \vee \neg y \vee \neg z) </tex>  
+
Обозначим за <tex>N</tex> число вхождений переменных в формулу.
такой переменной является <tex>x</tex>. Если такие переменные существуют, то им надо присвоить значение <tex> 1 </tex>, если переменная входит без отрицания и <tex>0</tex>, если переменная входит с отрицанием, так как в конъюнкции они должны дать <tex>1</tex>. Далее, если какая-либо скобка обратилась в <tex> 0 </tex>, то решения не существует, иначе, решение существует, так как всем остальным переменным мы можем присвоить нужные нам значения так, чтобы в каждом дизъюнкте значение было равно <tex> 1</tex>.
+
Итерация состоит из шагов, каждый из которых выполняется за <tex>O(N)</tex>. Всего итераций будет не больше <tex>N</tex>, так как если первый шаг не завершил алгоритм, то уменьшил размер формулы на одно вхождение. Итого, асимптотика алгоритма составляет <tex>O(N^2)</tex>.
Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. Сделав так для каждой скобки, мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в конечном итоге даст нам <tex> 1</tex>.
+
}}
*Функцию <tex>F</tex> можно задать в форме Хорна <tex>  \iff </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>
<tex> F(x_1, ..., x_n)=F(y_1, ..., y_n)=1  \Rightarrow  F(x_1 \wedge y_1, x_2  \wedge  y_2, ..., x_n \wedge y_n)</tex>
+
}}
  
 
== См.также ==
 
== См.также ==
 
* [[СКНФ]]
 
* [[СКНФ]]
 
* [[2SAT]]
 
* [[2SAT]]
 +
* [[ДНФ]]
  
 
==Примечания==
 
==Примечания==
Строка 54: Строка 63:
  
 
==Источники информации==
 
==Источники информации==
*[https://en.wikipedia.org/wiki/Horn_clause| Wikipedia {{---}} Horn clause]
+
*[https://en.wikipedia.org/wiki/Conjunctive_normal_form Wikipedia {{---}} CNF]
*[https://en.wikipedia.org/wiki/2-satisfiability| Wikipedia {{---}} 2-satisfiability]
+
 
  
 
[[Категория: Дискретная математика и алгоритмы]]
 
[[Категория: Дискретная математика и алгоритмы]]
  
 
[[Категория: Булевы функции ]]
 
[[Категория: Булевы функции ]]

Текущая версия на 19:39, 4 сентября 2022

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

КНФ в форме Крома

Определение:
Конъюнктивная нормальная форма (англ. conjunctive normal form, CNF) в форме Крома, 2-КНФ[1] (англ. 2-CNF) — конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию ровно двух литералов.


Пример :

[math](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 [/math]

Утверждение:
Существует алгоритм, который за полиномиальное время проверяет, что формулу, заданную в форме Крома, можно удовлетворить.
Основная статья: 2SAT


Утверждение:
Функцию [math]F[/math] можно задать в форме Крома [math] \iff [/math] выполнено следующее следствие : [math] F(x_1, \ldots, x_n)=F(y_1, \ldots, y_n)=F(z_1, \ldots, z_n)=1 \Rightarrow[/math] [math]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)[/math]

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

Определение:
Конъюнктивная нормальная форма (англ. conjunctive normal form, CNF) в форме Хорна[2] (англ. Horn clause) — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.


Пример:

[math] (\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[/math]

Каждая скобка представляет собой Дизъюнкт Хорна[3].

Утверждение:
Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна, можно удовлетворить.
[math]\triangleright[/math]

Далее будет приведено доказательство, предлагающее алгоритм решения.

  • Шаг 1. Одиночное вхождение переменных. Найдем в данной формуле одиночно стоящие переменные. Например, для формулы [math] x \wedge (x \vee \neg y \vee \neg z) [/math] такой переменной является [math]x[/math].
    1. Присутствуют одиночно стоящие переменные.
      Присвоим всем таким переменным значение [math] 1 [/math], если переменная входит без отрицания и [math]0[/math] иначе, так как в конъюнкции они должны дать [math]1[/math]. Заметим, что если какая-либо скобка после этого обратилась в [math] 0 [/math], то решения не существует.
    2. Отсутствуют одиночно стоящие переменные.
      Всем переменным надо присвоить значение [math] 0 [/math] и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение [math]0[/math] мы получим [math] 1[/math] в результате дизъюнкции. В итоге мы получим выражение вида: [math]1\wedge 1 \wedge \ldots \wedge 1[/math], что в результате даст нам [math] 1[/math]. В таком случае дальнейшие шаги выполнять не нужно.
  • Шаг 2.
    Опустим одиночно стоящие переменные и скобки, в которых значение стало равным [math]1[/math]. Перейдём к [math]1[/math] шагу алгоритма. По определению формы Хорна, в каждой из скобок, где мы опустили переменную, не больше [math]1[/math] переменной без отрицания. Либо какая-то из переменных внутри скобки будет иметь отрицание, т.е. при подстановке [math]0[/math] станет равна [math]1[/math], либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит [math]1[/math] шаг алгоритма выполнится верно. Будем проделывать алгоритм, начиная сначала, пока [math]1[/math] шаг не найдёт ответ.

Обозначим за [math]N[/math] число вхождений переменных в формулу.

Итерация состоит из шагов, каждый из которых выполняется за [math]O(N)[/math]. Всего итераций будет не больше [math]N[/math], так как если первый шаг не завершил алгоритм, то уменьшил размер формулы на одно вхождение. Итого, асимптотика алгоритма составляет [math]O(N^2)[/math].
[math]\triangleleft[/math]
Утверждение:
Функцию [math]F[/math] можно задать в форме Хорна [math] \iff [/math] выполнено следующее следствие:[math] 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)[/math]

См.также

Примечания

Источники информации