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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Доказательство принадлежности классу NPH)
(Доказательство принадлежности классу NPH)
Строка 19: Строка 19:
  
 
Итак, опишем действия функции <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>
* <tex> \neg(x \vee y) = \neg x \wedge \neg y </tex>
+
# <tex> \neg(x \vee y) = \neg x \wedge \neg y </tex>
* <tex> \neg(\neg x) = x </tex>
+
# <tex> \neg(\neg x) = x </tex>

Версия 14:14, 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]