Теорема Кука — различия между версиями
Npgs (обсуждение | вклад) |
Npgs (обсуждение | вклад) |
||
Строка 1: | Строка 1: | ||
=== Определение === | === Определение === | ||
− | Проблема < | + | Проблема <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> — проблема выполнимости булевых формул. |
− | Докажем, что эта проблема < | + | Докажем, что эта проблема <tex>NP\,\!</tex>-полна. |
== Формулировка == | == Формулировка == | ||
− | '''Теорема Кука''' гласит, что < | + | '''Теорема Кука''' гласит, что <tex>SAT \in NPC.</tex> |
== Доказательство == | == Доказательство == | ||
− | < | + | <tex>SAT \in NPC</tex>, если |
− | *< | + | *<tex>SAT \in NP</tex> |
− | *< | + | *<tex>SAT \in NPH</tex> |
− | Прежде всего докажем, что < | + | Прежде всего докажем, что <tex>SAT \in NP.</tex> |
− | Так как < | + | Так как <tex>NP = \Sigma_1\,\!</tex>, то достаточно показать, что <tex>SAT \in \Sigma_1</tex> |
− | В качестве сертификата берём набор нулей и единиц в количестве < | + | В качестве сертификата берём набор нулей и единиц в количестве <tex>n\,\!</tex> штук, соответствующих значениям аргументов функции <tex>\phi\,\!</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi\,\!</tex>. |
− | Верификатор просто подставит эти значения в формулу < | + | Верификатор просто подставит эти значения в формулу <tex>\phi\,\!</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу. |
− | Если же у нас существует такой сертификат < | + | Если же у нас существует такой сертификат <tex>y\,\!</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой. |
− | Теперь докажем, что < | + | Теперь докажем, что <tex>SAT \in NPH.</tex> Для этого сведём проблему <tex>BH_{1N}\,\!</tex>, которая, как нам известно, <tex>NP\,\!</tex>-полна, к проблеме <tex>SAT.\,\!</tex> Тогда получится, что любая проблема из <tex>NP\,\!</tex> может быть сведена по Карпу к проблеме <tex>BH_{1N}\,\!</tex>, и, по транзитивности сведения по Карпу, к <tex>SAT.\,\!</tex> |
− | По условию проблемы < | + | По условию проблемы <tex>BH_{1N}\,\!</tex>, у нас есть недетерминированная машина Тьюринга <tex>m\,\!</tex>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <tex>x\,\!</tex> и время <tex>t\,\!</tex>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <tex>\phi\,\!</tex>, что она выполнима тогда, и только тогда, когда <tex>m\,\!</tex>, получив на вход <tex>x\,\!</tex>, делает не более <tex>t\,\!</tex> шагов и допускает это слово. |
− | В любой момент времени мгновенное описание (МО) < | + | В любой момент времени мгновенное описание (МО) <tex>m\,\!</tex> есть строка <tex>z\#_qyb</tex>, где <tex>b\,\!</tex> — строка, состоящая из такого количества пробелов, чтобы длина всего МО была <tex>t + 1.\,\!</tex> Соответственно, начальное МО задаётся так : <tex>\#_sx\,\!</tex>. Если же <tex>|x| > t\,\!</tex>, то будем считать, что на ленту записаны лишь первые <tex>t\,\!</tex> символов, ведь <tex>m\,\!</tex> не может обработать большее количество символов за <tex>t\,\!</tex> шагов. |
− | Также нам удобно считать, что все вычисления проходят ровно за < | + | Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>. |
− | Тогда процесс работы машины < | + | Тогда процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : |
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0" | {| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0" | ||
− | |+ '''Процесс работы машины < | + | |+ '''Процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>''' |
|- | |- | ||
! width="50" style="border-right:3px solid gray; border-bottom:3px solid gray;" | MO !! width="50" style="border-bottom:3px solid gray;"| 0 !! width="50" style="border-bottom:3px solid gray;" | 1 !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | t | ! width="50" style="border-right:3px solid gray; border-bottom:3px solid gray;" | MO !! width="50" style="border-bottom:3px solid gray;"| 0 !! width="50" style="border-bottom:3px solid gray;" | 1 !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | t | ||
|- style="height:50px;" | |- style="height:50px;" | ||
− | ! style="border-right:3px solid gray;" | < | + | ! style="border-right:3px solid gray;" | <tex>q_0\,\!</tex> |
− | | < | + | | <tex>q_{0, 0}\,\!</tex> || <tex>q_{0, 1}\,\!</tex> || || || || || || || <tex>q_{0, t}\,\!</tex> |
|- style="height:50px" | |- style="height:50px" | ||
− | ! style="border-right:3px solid gray;" | < | + | ! style="border-right:3px solid gray;" | <tex>q_1\,\!</tex> |
− | | < | + | | <tex>q_{1, 0}\,\!</tex> || <tex>q_{1, 1}\,\!</tex> || || || || || || || <tex>q_{1, t}\,\!</tex> |
|- style="height:30px" | |- style="height:30px" | ||
! style="border-right:3px solid gray;" | ... || || || || || || || || || | ! style="border-right:3px solid gray;" | ... || || || || || || || || || | ||
|- style="height:50px" | |- style="height:50px" | ||
− | ! style="border-right:3px solid gray;" | < | + | ! style="border-right:3px solid gray;" | <tex>q_i\,\!</tex> |
− | | || || || < | + | | || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || <tex>q_{i, j + 2\,\!}</tex> || || |
|- style="height:50px" | |- style="height:50px" | ||
− | ! style="border-right:3px solid gray;" | < | + | ! style="border-right:3px solid gray;" | <tex>q_{i + 1}\,\!</tex> |
− | | || || || < | + | | || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || || || |
|- style="height:30px" | |- style="height:30px" | ||
! style="border-right:3px solid gray;" | ... || || || || || || || || || | ! style="border-right:3px solid gray;" | ... || || || || || || || || || | ||
|- style="height:50px" | |- style="height:50px" | ||
− | ! style="border-right:3px solid gray;" | < | + | ! style="border-right:3px solid gray;" | <tex>q_t\,\!</tex> |
− | | < | + | | <tex>q_{t, 0}\,\!</tex> || <tex>q_{t, 1}\,\!</tex> || || || || || || || <tex>q_{t, t}\,\!</tex> |
|} | |} | ||
− | Каждый элемент таблицы < | + | Каждый элемент таблицы <tex>q_{i, j}\in \Sigma \cup Q</tex>. И для каждого такого элемента заведём <tex>|\Sigma| + |Q|\,\!</tex> переменных <tex>Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q\,\!</tex> |
− | Общий вид формулы : < | + | Общий вид формулы : <tex>\phi = S \land T \land N \land C</tex> |
Версия 21:29, 13 марта 2010
Определение
Проблема
— проблема выполнимости булевых формул.Докажем, что эта проблема
-полна.Формулировка
Теорема Кука гласит, что
Доказательство
, если
Прежде всего докажем, что
Так как
, то достаточно показать, чтоВ качестве сертификата берём набор нулей и единиц в количестве
штук, соответствующих значениям аргументов функции . Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу .Верификатор просто подставит эти значения в формулу
и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.Если же у нас существует такой сертификат
, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.Теперь докажем, что
Для этого сведём проблему , которая, как нам известно, -полна, к проблеме Тогда получится, что любая проблема из может быть сведена по Карпу к проблеме , и, по транзитивности сведения по Карпу, кПо условию проблемы
, у нас есть недетерминированная машина Тьюринга , причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово и время , заданное в унарной системе счисления. Нам же надо построить такую булеву формулу , что она выполнима тогда, и только тогда, когда , получив на вход , делает не более шагов и допускает это слово.В любой момент времени мгновенное описание (МО)
есть строка , где — строка, состоящая из такого количества пробелов, чтобы длина всего МО была Соответственно, начальное МО задаётся так : . Если же , то будем считать, что на ленту записаны лишь первые символов, ведь не может обработать большее количество символов за шагов.Также нам удобно считать, что все вычисления проходят ровно за
шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход , если в МО есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО .Тогда процесс работы машины
на входе , то есть цепочка переходов может быть представлен следующей таблицей :MO | 0 | 1 | ... | ... | t | ||||
---|---|---|---|---|---|---|---|---|---|
... | |||||||||
... | |||||||||
Каждый элемент таблицы
. И для каждого такого элемента заведём переменныхОбщий вид формулы :