36
правок
Изменения
Нет описания правки
== Доказательство ==
Для доказательства будем строить вероятностную программу <tex>''Verifier</tex>'', которая хочет проверить, верно ли, что заданная формула <tex>\varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов. Программа <tex>''Verifier</tex> '' может совершить не больше полинома от длины входа действий, а также может обращаться к программе <tex>''Prover</tex>'', которая пытается любым возможным способом убедить <tex>''Verifier</tex> '' в верности рассматриваемого утверждения.
Далее в программе <tex>''Verifier</tex> '' будем писать "проверим ...", что означает проверку соответствующего условия, и, при ложности, <tex>''Verifier</tex> '' будет сразу завершаться и возвращать <tex>''false</tex>'', т.к. <tex>''Prover</tex> '' её обманывает, а значит, нет правильного доказательства проверяемого утверждения.
Шаг 0.
Пусть формула <tex>\varphi</tex> каким-либо образом записана. Пусть формула <tex>\varphi</tex> имеет <tex>n</tex> переменных и степень <tex>d</tex>. Сделаем следующие замены и получим формулу <tex>A(x_1, x_2, ..., x_n)</tex>:
# <tex>x \land y \to x \cdot y</tex>
# <tex> \lnot x \to 1 - x</tex>
# <tex> x \lor y \to x + y - x \cdot y = 1 - (1 - x) \cdot (1 - y)</tex>
Заметим, что длина формулы возрастет не больше, чем в константу раз.
Пусть полином <tex>A(x_1, x_2, ..., x_n)</tex> имеет степень <tex>d</tex>.
Итак, надо проверить следующее арифметическое уравнение: <tex>\sum_{x_1 = 0}^{1}\sum_{x_2 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n) = k</tex>.
Попросим <tex>''Prover</tex>'' 'а прислать <tex>''Verifier</tex>'' 'у простое число <tex>p > max(2^n, k_p)</tex> и сертификат о его простоте.
Проверим простоту <tex>p</tex> по сертификату и условие <tex>p > max(2^n, k_p)</tex>. Константу <tex>k_p</tex> определим позднее.
Далее будем проводить весь счет вычислять и проверять уравнение равенства по модулю <tex>p</tex>.
Пусть <tex>A_0(x_1) = \sum_{x_2 = 0}^{1}\sum_{x_3 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n)</tex>.
Попросим <tex>''Prover</tex>'' 'а прислать <tex>''Verifier</tex>'' 'у формулу <tex>A_0(x_1)</tex>.
Проверим следующее утверждение: <tex>A_0(0) + A_0(1) = k</tex>.
Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длинны входа <tex>''Verifier</tex>'' 'а. Этот факт следует из того, что формула имеет степень меньшую либо равную <tex>d</tex>, и она от одной переменной. Поэтому её можно представить так: <tex>A_0(x) = \sum_{i = 0}^{d} C_i \cdot x ^ i</tex>, и попросить <tex>''Prover</tex>'' 'а прислать только сами коэффициенты <tex>C_i</tex> по модулю <tex>p</tex>.
Шаг 1.
Пусть <tex>r_1 = random(p)</tex>. Отправим <tex>r_1</tex> программе <tex>''Prover</tex>''.
Пусть <tex>A_1(x_2) = \sum_{x_3 = 0}^{1}\sum_{x_4 = 0}^{1}...\sum_{x_n = 0}^{1} A(r_1, x_2, ..., x_n)</tex>.
Попросим <tex>''Prover</tex>'' 'а прислать <tex>''Verifier</tex>'' 'у формулу <tex>A_1(x_2)</tex>.
Проверим следующее утверждение: <tex>A_1(0) + A_1(1) = A_0(r_1)</tex>.
Шаг <tex>n</tex>.
Пусть <tex>r_n = random(p)</tex>. Отправим <tex>r_n</tex> программе <tex>''Prover</tex>''.
Пусть <tex>A_n() = A(r_1, r_2, ..., r_n)</tex>.
Попросим программу <tex>''Prover</tex> '' прислать <tex>''Verifier</tex>'' 'у значение <tex>A_n()</tex>.
Проверим следующее утверждение: <tex>A_n() = A_{n-1}(r_n)</tex>.
А также сами подставим <tex>r_1, r_2, ..., r_n</tex> в <tex>A(x_1, x_2, ..., x_n)</tex> и проверим правильность присланного значения <tex>A_n()</tex>.
Возвращаем <tex>''true</tex>''.
Итак, остается доказать, что написанный <tex>''Verifier</tex> '' - корректный <tex>''Verifier</tex> '' для языка <tex>\#SAT</tex>. Таким образом, нужно доказать:# Построенный <tex>''Verifier</tex> '' - вероятностная машина Тьюринга, совершающая не более полинома от длинны входа действий.
# <tex><\varphi, k> \in \#SAT \Rightarrow \exists Prover : P(Verifier^{Prover}(x)) \ge 2/3</tex>.
# <tex><\varphi, k> \notin \#SAT \Rightarrow \forall Prover : P(Verifier^{Prover}(x)) \le 1/3</tex>.
Доказательство:
# Из программы <tex>''Verifier</tex> '' видно, что она работает за <tex>O(poly(|input|))</tex>.# Если <tex>\varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов, то существует такая программа <tex>''Prover</tex>'', что <tex>P(VP(x)) = 1</tex>. Такая программа:
## Присылает, например, первое простое число, большее <tex>max(2^n, k_p)</tex>, и сертификат.
## Считает сумму <tex>A_0(x_1)</tex> и присылает формулу.
## Считает сумму <tex>A_1(x_2)</tex> и присылает формулу.
## ...
# Пусть <tex>\varphi</tex> имеет не <tex>k</tex> удовлетворяющих наборов. Тогда для того, что бы <tex>''Verifier</tex> '' вернул <tex>''true</tex>'', необходимо <tex>''Prover</tex>'' 'у посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:
Шаг 0.
Так как <tex>\varphi</tex> имеет не <tex>k</tex> удовлетворяющих наборов, то <tex>''Prover</tex> '' не может послать правильное <tex>A_0</tex> – не выполнится условие <tex>A_0(0) + A_0(1) = k</tex>. Поэтому он посылает не <tex>A_0</tex>, а некое <tex>\tilde{A}_0</tex>.
Шаг 1.
Шаг <tex>n</tex>.
С вероятностью <tex>1 - d / p : A_{n-1}(r_n) \ne \tilde{A}_{n-1}(r_n)</tex>, и потому <tex>''Verifier</tex> '' получит не <tex>A_n</tex>, а <tex>\tilde{A}_n</tex>.
Из этого процесса заметим, что с вероятностью большей либо равной <tex>(1 - d / p) ^ n</tex> мы дойдем до последнего шага и будем имееть <tex>\tilde{A}_n</tex> вместо <tex>A_n</tex>. Так как на шаге <tex>n</tex> <tex>''Verifier</tex> '' вычисляет <tex>A_n</tex> и проверяет значение, то <tex>''Verifier</tex> '' вернет <tex>''false</tex>''.
Так как мы хотим сделать вероятность возврата <tex>''false</tex> '' большую либо равную <tex>2/3</tex>, то выберем <tex>k_p</tex> так, чтобы <tex>(1 - d / k_p) ^ n \ge 2/3</tex>.
Утверждение доказано.
