165
правок
Изменения
Изменение стиля
=== Определение ===
Проблема '''SAT''' = <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> — проблема выполнимости булевых формул.
Докажем, что эта проблема [[NP-полнота|<tex>'''NP</tex>'''-полна.]]
== Формулировка теоремы Кука =='''Теорема Кука'''
== Доказательство ==
=== Доказательство того, что ''SAT'' ∈ ''NP'' ===Прежде всего докажем, что <tex>'''SAT \in ''' ∈ '''NP'''.</tex>
В качестве сертификата берём набор нулей и единиц в количестве <tex>n</tex> штук, соответствующих значениям аргументов функции <tex>\phi</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi</tex>.
Если же у нас существует такой сертификат <tex>y</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.
=== Доказательство того, что ''SAT'' ∈ ''NPH'' ===Теперь докажем, что <tex>'''SAT \in ''' ∈ '''NPH'''.</tex> Для этого сведём проблему '''BH<texsub>BH_{1N}</texsub>'''<ref>[[NP-полнота_задачи_BH1N|'''NP'''-полнота задачи '''BH<mathsub>BH_{1N}</mathsub>''']]</ref>, которая, как нам известно, <tex>'''NP</tex>'''-полна, к проблеме <tex>'''SAT'''.</tex> Тогда получится, что любая проблема из <tex>'''NP</tex> ''' может быть [[Сведение_по_Карпу|сведена по Карпу]] к проблеме '''BH<texsub>BH_{1N}</texsub>''', и, по транзитивности сведения по Карпу, к <tex>'''SAT'''.</tex>
По условию проблемы '''BH<texsub>BH_{1N}</texsub>''', у нас есть недетерминированная машина Тьюринга <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>\#_sxb</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>f: \langle m, x, 1^t \rangle \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от длины входа — <tex>|\phi| = O(n^2)</tex>.
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex>\langle m, x, 1^t \rangle \in BH_{</tex> ∈ '''BH<sub>1N}</texsub>'''.
# Пусть <tex>\langle m, x, 1^t \rangle \in BH_{</tex> ∈ '''BH<sub>1N}</texsub>''', тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> примет значение ''истина''.# Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> на нем принимает значение ''истина''. Тогда по данному набору можем построить таблицу, по которой восстановим допускающую цепочку переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>. Совершив эти переходы машина <tex>m</tex> перейдет в допускающее состояние за время <tex>t</tex>, следовательно <tex>\langle m, x, 1^t\rangle \in BH_{</tex> ∈ '''BH<sub>1N}</texsub>'''.
Значит, <tex>'''SAT \in ''' ∈ '''NPH</tex> ''' и из доказанного ранее следует,что <tex>'''SAT \in ''' ∈ '''NPC</tex>. Теорема доказана''', что и требовалось доказать.
== Ссылки ==
