Изменения

Перейти к: навигация, поиск

Sharp SAT

6120 байт добавлено, 19:20, 4 сентября 2022
м
rollbackEdits.php mass rollback
== Определение ==
<tex>\#SAT = \{ <\langle \varphi, k> \rangle | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>
== Утверждение ==
== Доказательство ==
Для доказательства будем строить вероятностную программу ''Verifier'', которая хочет проверить, верно ли, что заданная формула фи <tex>\varphi</tex> имеет ровно к <tex>k</tex> удовлетворяющих наборов. Программа ''Verifier '' может совершить не больше полинома от длины входа шаговдействий, а также может обращаться к программе ''Prover'', которая пытается любым возможным способом убедить нас (т.е. ''Verifier) '' в верности рассматриваемого утверждения.
Программа Далее в программе ''Verifier '' будем писать "проверим ...", что означает проверку соответствующего условия, и, при ложности, ''Verifier'' будет выполнять следующие шагисразу завершаться и возвращать ''false'', т.к. ''Prover'' её обманывает, а значит, нет правильного доказательства проверяемого утверждения.
''Verifier'' будет выполнять следующие шаги. Шаг 0. Пусть формула <tex>\varphi</tex> каким -либо образом записана. Пусть формула <tex>\varphi</tex> имеет <tex>n</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>\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>d</tex>.
Попросим программу Prover прислать нам простое число p Итак, надо проверить следующее уравнение: <tex> 2\sum_{x_1 = 0}^{1}\sum_{x_2 = 0}^{1}...\sum_{x_n = 0}^n{1} A(x_1, x_2, и сертификат о его простоте.Проверим простоту p по сертификату.., и условие p x_n) = k</tex> 2^n.
ЗаметимПопросим ''Prover'' 'а прислать ''Verifier'' 'у такое простое число <tex>p</tex>, что если какое-либо проверяемое условие не выполнено<tex>max(2^n+1, k_p) \le p \le 2 \cdot max(2^n+1, k_p)</tex>, то программа Verifier сразу завершается и возвращает false, тсертификат о его простоте.к. Prover нас обманываетПроверим простоту <tex>p</tex> по сертификату и условие <tex>max(2^n+1, а значитk_p) \le p \le 2 \cdot max(2^n+1, нет правильного доказательства проверяемого утверждения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>.
Попросим программу ''Prover '' 'а прислать нам ''Verifier'' 'у формулу <tex>A_0(x_1)???</tex>.Проверим следующее утверждение: A0<tex>A_0(0) + A0A_0(1) = k???</tex>. Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длины входа ''Verifier'' 'а. Этот факт следует из того, что формула имеет степень меньшую либо равную <tex>d</tex>, и она от одной переменной. Поэтому её можно представить так: <tex>A_0(x) = \sum_{i = 0}^{d} C_i \cdot x ^ i</tex>, и попросить ''Prover'' 'а прислать только сами коэффициенты <tex>C_i</tex> по модулю <tex>p</tex>. Шаг 1. Пусть <tex>r_1 = random(p)</tex>. Отправим <tex>r_1</tex> программе ''Prover''.
Пусть r_1 = random(p).
Пусть <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>.
Попросим программу ''Prover '' 'а прислать нам ''Verifier'' 'у формулу <tex>A_1(x_2)</tex>.Проверим следующее утверждение: <tex>A_1(0) + A_1(1) = A_0(r_1)</tex>. Шаг 2. ...
Продолжим так делатьШаг <tex>n</tex>. Пусть <tex>r_n = random(p)</tex>. Отправим <tex>r_n</tex> программе ''Prover''.
Пусть r_n = random(p).
Пусть <tex>A_n() = A(r_1, r_2, ..., r_n)</tex>.
Попросим программу ''Prover '' прислать нам формулу ''Verifier'' 'у значение <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>. Возвращаем ''true''.  Итак, остается доказать, что написанный ''Verifier'' - корректный ''Verifier'' для языка <tex>\#SAT</tex>. Таким образом, нужно доказать:# Построенный ''Verifier'' - вероятностная машина Тьюринга, совершающая не более полинома от длины входа действий.# <tex>\langle \varphi, k \rangle \in \#SAT \Rightarrow \exists Prover : P(Verifier^{Prover}(x)) \ge 2/3</tex>.# <tex>\langle \varphi, k \rangle \notin \#SAT \Rightarrow \forall Prover : P(Verifier^{Prover}(x)) \le 1/3</tex>. Доказательство: # Из программы ''Verifier'' видно, что она работает за <tex>O(poly(|input|))</tex>.# Если <tex>\varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов, то существует такая программа ''Prover'', что <tex>P(Verifier^{Prover}(x)) = 1</tex>. Такая программа:## Присылает, например, первое простое число, большее <tex>max(2^n+1, k_p)</tex>, и сертификат.## Считает сумму <tex>A_0(x_1)</tex> и присылает формулу.## Получает <tex>r_1</tex>.## Считает сумму <tex>A_1(x_2)</tex> и присылает формулу.## ...# Пусть <tex>\varphi</tex> имеет не <tex>k</tex> удовлетворяющих наборов. Тогда для того, что бы ''Verifier'' вернул ''true'', необходимо ''Prover'' 'у посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать: Шаг 0. Так как <tex>\varphi</tex> имеет не <tex>k</tex> удовлетворяющих наборов, то ''Prover'' не может послать правильное <tex>A_0</tex> – не выполнится условие <tex>A_0(0) + A_0(1) = k</tex>. Поэтому он посылает не <tex>A_0</tex>, а некое <tex>\tilde{A}_0</tex>. Шаг 1. Во первых, отметим, что ситуация <tex>A_0(r_1) = \tilde{A}_0(r_1)</tex> происходит с вероятностью меньшей либо равной <tex>d / p</tex> для некоторого случайно выбранного <tex>r_1</tex>, что следует из [[Лемма_Шварца-Зиппеля|леммы Шварца-Зиппеля]]. Таким образом, с вероятностью большей либо равной <tex>1 - d / p : A_0(r_1) \ne \tilde{A}_0(r_1)</tex> и, ввиду того, что должно выполняться условие <tex>A_1(0) + A_1(1) = A_0(r_1)</tex>, получаем, что <tex>A_1</tex> тоже будет неправильное, т.е. некоторое <tex>\tilde{A}_1</tex>. Шаг 2. ... Шаг <tex>n</tex>. С вероятностью <tex>1 - d / p : A_{n-1}(r_n) \ne \tilde{A}_{n-1}(r_n)</tex>, и потому ''Verifier'' получит не <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> ''Verifier'' вычисляет <tex>A_n</tex> и проверяет значение, то ''Verifier'' вернет ''false''.  Так как мы хотим сделать вероятность возврата ''false'' большую либо равную <tex>2/3</tex>, то выберем <tex>k_p</tex> так, чтобы <tex>(1-d/k_p)^n \ge 2/3</tex>. Возьмем <tex>k_p = 3 d \cdot n</tex>. Заметим, что длина <tex>k_p</tex> есть <tex>poly(|input|)</tex>. Из разложения функции по Тейлору получаем: <tex>(1-d/k_p)^n = (1 - 1/(3n))^n = 1 - 1/3 + \frac{n(n - 1)}{2 (3n)^2} - \frac{n(n-1)(n-2)}{6 (3n)^3} + ... </tex>. Так как <tex>n</tex> - целое неотрицательное число, то: <tex>(1-d/k_p)^n \ge 2/3 + \frac{n(n-1)}{n^2}(\frac{1}{2 \cdot 3^2} - \frac{1}{6 \cdot 3^3}) + ... \ge 2/3</tex>.
Вероятность ... Утверждение доказано.
1632
правки

Навигация