NP-полнота задачи о выполнимости булевой формулы в форме КНФ — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Доказательство принадлежности классу NPH)
Строка 1: Строка 1:
 
==== Определения ====
 
==== Определения ====
* ''Литералом'' является переменная или отрицание переменной. Например, <tex>x</tex> или <tex>\neg y</tex>.
+
* ''Литералом'' является переменная или отрицание переменной. Например, <tex> x </tex> или <tex> \neg y </tex>.
* ''Дизъюнктом'' называется логическое '''ИЛИ''' одного или нескольких литералов. Например, <tex>x \vee \neg y \vee z</tex>
+
* ''Дизъюнктом'' называется логическое '''ИЛИ''' одного или нескольких литералов. Например, <tex> x \vee \neg y \vee z </tex>
 
* Говорят, что формула записана в ''конъюнктивной нормальной форме'' (КНФ), если представляет собой логическое '''И''' дизъюнктов.
 
* Говорят, что формула записана в ''конъюнктивной нормальной форме'' (КНФ), если представляет собой логическое '''И''' дизъюнктов.
 
==== Определение ====
 
==== Определение ====
<tex>CNFSAT = \{\phi \ |\ \phi </tex> ''в КНФ,'' <tex>\phi \in </tex> [[SAT]] <tex> \} </tex> &mdash; задача о выполнимости булевой формулы в форме КНФ.
+
<tex> CNFSAT = \{\phi \ |\ \phi </tex> ''в КНФ,'' <tex> \phi \in </tex> [[SAT]] <tex> \} </tex> &mdash; задача о выполнимости булевой формулы в форме КНФ.
  
 
== Теорема ==
 
== Теорема ==
Строка 13: Строка 13:
 
* <tex> CNFSAT \in NPH </tex>
 
* <tex> CNFSAT \in NPH </tex>
 
==== Доказательство принадлежности классу NP ====
 
==== Доказательство принадлежности классу NP ====
В качестве сертификата выберем множество <tex>\{y_1, ...,y_n\}</tex>, представляющее собой набор из нулей и единиц. Верификатору останется подставить эти значения в качестве аргументов в формулу <tex>\phi(x_1, ..., x_n)</tex> и проверить, выдает ли она единицу. Длина сертификата и время работы верификатора, очевидно, удовлетворяют условиям полиномиальности. Таким образом, <tex>CNFSAT \in \Sigma_1 = NP</tex>
+
В качестве сертификата выберем множество <tex> \{y_1, ...,y_n\} </tex>, представляющее собой набор из нулей и единиц. Верификатору останется подставить эти значения в качестве аргументов в формулу <tex> \phi(x_1, ..., x_n) </tex> и проверить, выдает ли она единицу. Длина сертификата и время работы верификатора, очевидно, удовлетворяют условиям полиномиальности. Таким образом, <tex> CNFSAT \in \Sigma_1 = NP </tex>
  
 
==== Доказательство принадлежности классу NPH ====
 
==== Доказательство принадлежности классу NPH ====
Выполним [[сведение по Карпу]] задачи <tex>SAT</tex> к задаче <tex>CNFSAT</tex>. Для этого необходимо построить функцию <tex>f</tex>, вычислимую за полиномиальное время от длины входа, которая выполняла бы преобразование <tex>\phi \to \omega</tex>, где <tex>\omega</tex> в КНФ. Заметим, что в общем случае время построения эквивалентной формулы в форме КНФ может оказаться больше полиномиального. В частности, длина формулы может вырасти экспоненциально, и тогда время порождения тоже экспоненциально вырастет. Однако нам достаточно предъявить формулу <tex>\omega</tex>, которая будет выполнима тогда и только тогда, когда выполнима исходная формула <tex>\phi</tex>. При этом формулы могут оказаться не эквивалентными, ввиду, например, добавления новых переменных.
+
Выполним [[сведение по Карпу]] задачи <tex> SAT </tex> к задаче <tex> CNFSAT </tex>. Для этого необходимо построить функцию <tex> f </tex>, вычислимую за полиномиальное время от длины входа, которая выполняла бы преобразование <tex> \phi \to \omega </tex>, где <tex> \omega </tex> в КНФ. Заметим, что в общем случае время построения эквивалентной формулы в форме КНФ может оказаться больше полиномиального. В частности, длина формулы может вырасти экспоненциально, и тогда время порождения тоже экспоненциально вырастет. Однако нам достаточно предъявить формулу <tex> \omega </tex>, которая будет выполнима тогда и только тогда, когда выполнима исходная формула <tex> \phi </tex>. При этом формулы могут оказаться не эквивалентными, ввиду, например, добавления новых переменных.
  
Итак, опишем действия функции <tex>f</tex>.
+
Итак, опишем действия функции <tex> f </tex>.
 
* На первом этапе все отрицания <tex> \neg </tex> спускаются вниз по дереву выражения, так что в формуле остаются только отрицания переменных. Булева формула превращается в логические '''И''' и '''ИЛИ''' литералов. Это преобразование дает формулу, эквивалентную исходной, и занимает время, как максимум, квадратичное относительно длины этой формулы. Для этого используются ''законы Де Моргана'' и ''закон двойного отрицания''.
 
* На первом этапе все отрицания <tex> \neg </tex> спускаются вниз по дереву выражения, так что в формуле остаются только отрицания переменных. Булева формула превращается в логические '''И''' и '''ИЛИ''' литералов. Это преобразование дает формулу, эквивалентную исходной, и занимает время, как максимум, квадратичное относительно длины этой формулы. Для этого используются ''законы Де Моргана'' и ''закон двойного отрицания''.
 
# <tex> \neg(x \wedge y) = \neg x \vee \neg y </tex>
 
# <tex> \neg(x \wedge y) = \neg x \vee \neg y </tex>
Строка 25: Строка 25:
  
 
* Второй этап - переписать формулу, которая представляет собой логическое '''И''' и '''ИЛИ''' литералов, в виде произведения дизъюнктов, т.е. привести ее к КНФ. Введение новых переменных позволяет провести это преобразование за время, полиномиально зависящее от размера исходной формулы.
 
* Второй этап - переписать формулу, которая представляет собой логическое '''И''' и '''ИЛИ''' литералов, в виде произведения дизъюнктов, т.е. привести ее к КНФ. Введение новых переменных позволяет провести это преобразование за время, полиномиально зависящее от размера исходной формулы.
 +
Рассмотрим дерево разбора произвольной формулы. Листья этого дерева будут соответствовать литералам, а узлы - логической операции '''И''' или '''ИЛИ''' над двумя его потомками.
 +
- Для узла с меткой '''И''' соответствующая КНФ получается как конъюнкция ('''И''') всех дизъюнктов двух подформул <tex> \alpha </tex> и <tex> \beta </tex>.
 +
- Для узла с меткой '''ИЛИ''' нужно ввести новую переменную. Добавляем ее во все дизъюнкты левого операнда <tex> \alpha </tex> и ее отрицание во все дизъюнкты правого операнда <tex> \beta </tex>. Можно заметить, что формула <tex> \alpha \vee \beta </tex> выполнима тогда и только тогда, когда выполнима <tex> (\alpha \vee y) \wedge (\beta \vee \neg y) </tex>.

Версия 14:45, 19 марта 2010

Определения

  • Литералом является переменная или отрицание переменной. Например, [math] x [/math] или [math] \neg y [/math].
  • Дизъюнктом называется логическое ИЛИ одного или нескольких литералов. Например, [math] x \vee \neg y \vee z [/math]
  • Говорят, что формула записана в конъюнктивной нормальной форме (КНФ), если представляет собой логическое И дизъюнктов.

Определение

[math] CNFSAT = \{\phi \ |\ \phi [/math] в КНФ, [math] \phi \in [/math] SAT [math] \} [/math] — задача о выполнимости булевой формулы в форме КНФ.

Теорема

[math] CNFSAT \in NPC. [/math]

Доказательство

Для доказательства теоремы необходимо установить два факта:

  • [math] CNFSAT \in NP [/math]
  • [math] CNFSAT \in NPH [/math]

Доказательство принадлежности классу NP

В качестве сертификата выберем множество [math] \{y_1, ...,y_n\} [/math], представляющее собой набор из нулей и единиц. Верификатору останется подставить эти значения в качестве аргументов в формулу [math] \phi(x_1, ..., x_n) [/math] и проверить, выдает ли она единицу. Длина сертификата и время работы верификатора, очевидно, удовлетворяют условиям полиномиальности. Таким образом, [math] CNFSAT \in \Sigma_1 = NP [/math]

Доказательство принадлежности классу NPH

Выполним сведение по Карпу задачи [math] SAT [/math] к задаче [math] CNFSAT [/math]. Для этого необходимо построить функцию [math] f [/math], вычислимую за полиномиальное время от длины входа, которая выполняла бы преобразование [math] \phi \to \omega [/math], где [math] \omega [/math] в КНФ. Заметим, что в общем случае время построения эквивалентной формулы в форме КНФ может оказаться больше полиномиального. В частности, длина формулы может вырасти экспоненциально, и тогда время порождения тоже экспоненциально вырастет. Однако нам достаточно предъявить формулу [math] \omega [/math], которая будет выполнима тогда и только тогда, когда выполнима исходная формула [math] \phi [/math]. При этом формулы могут оказаться не эквивалентными, ввиду, например, добавления новых переменных.

Итак, опишем действия функции [math] f [/math].

  • На первом этапе все отрицания [math] \neg [/math] спускаются вниз по дереву выражения, так что в формуле остаются только отрицания переменных. Булева формула превращается в логические И и ИЛИ литералов. Это преобразование дает формулу, эквивалентную исходной, и занимает время, как максимум, квадратичное относительно длины этой формулы. Для этого используются законы Де Моргана и закон двойного отрицания.
  1. [math] \neg(x \wedge y) = \neg x \vee \neg y [/math]
  2. [math] \neg(x \vee y) = \neg x \wedge \neg y [/math]
  3. [math] \neg(\neg x) = x [/math]
  • Второй этап - переписать формулу, которая представляет собой логическое И и ИЛИ литералов, в виде произведения дизъюнктов, т.е. привести ее к КНФ. Введение новых переменных позволяет провести это преобразование за время, полиномиально зависящее от размера исходной формулы.

Рассмотрим дерево разбора произвольной формулы. Листья этого дерева будут соответствовать литералам, а узлы - логической операции И или ИЛИ над двумя его потомками. - Для узла с меткой И соответствующая КНФ получается как конъюнкция (И) всех дизъюнктов двух подформул [math] \alpha [/math] и [math] \beta [/math]. - Для узла с меткой ИЛИ нужно ввести новую переменную. Добавляем ее во все дизъюнкты левого операнда [math] \alpha [/math] и ее отрицание во все дизъюнкты правого операнда [math] \beta [/math]. Можно заметить, что формула [math] \alpha \vee \beta [/math] выполнима тогда и только тогда, когда выполнима [math] (\alpha \vee y) \wedge (\beta \vee \neg y) [/math].