Sharp SAT — различия между версиями
SVKazakov (обсуждение | вклад) (Новая страница: «== Определение == <tex>\#SAT = \{ <\varphi, k> | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex> == У…») |
м (rollbackEdits.php mass rollback) |
||
(не показано 17 промежуточных версий 2 участников) | |||
Строка 1: | Строка 1: | ||
== Определение == | == Определение == | ||
− | <tex>\#SAT = \{ | + | <tex>\#SAT = \{ \langle \varphi, k \rangle | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex> |
== Утверждение == | == Утверждение == | ||
Строка 7: | Строка 7: | ||
== Доказательство == | == Доказательство == | ||
− | Пусть формула <tex>\varphi</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>x \land y \to x \cdot y</tex> | ||
# <tex> \lnot x \to 1 - x</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> 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>\sum_{x_1 = 0}^{1}\sum_{x_2 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n) = k</tex>. | ||
+ | |||
+ | Попросим ''Prover'' 'а прислать ''Verifier'' 'у такое простое число <tex>p</tex>, что <tex>max(2^n+1, k_p) \le p \le 2 \cdot max(2^n+1, k_p)</tex>, и сертификат о его простоте. | ||
+ | Проверим простоту <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>. | ||
+ | Проверим следующее утверждение: <tex>A_0(0) + A_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''. | ||
+ | |||
+ | Пусть <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''. | ||
+ | |||
+ | Пусть <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>. | ||
+ | |||
+ | Утверждение доказано. |
Текущая версия на 19:20, 4 сентября 2022
Определение
имеет удовлетворяющих наборов
Утверждение
Доказательство
Для доказательства будем строить вероятностную программу Verifier, которая хочет проверить, верно ли, что заданная формула
имеет ровно удовлетворяющих наборов. Программа Verifier может совершить не больше полинома от длины входа действий, а также может обращаться к программе Prover, которая пытается любым возможным способом убедить Verifier в верности рассматриваемого утверждения.Далее в программе Verifier будем писать "проверим ...", что означает проверку соответствующего условия, и, при ложности, Verifier будет сразу завершаться и возвращать false, т.к. Prover её обманывает, а значит, нет правильного доказательства проверяемого утверждения.
Verifier будет выполнять следующие шаги.
Шаг 0.
Пусть формула
каким-либо образом записана. Пусть формула имеет переменных. Сделаем следующие замены и получим формулу :Заметим, что длина формулы возрастет не больше, чем в константу раз.
Пусть полином
имеет степень .Итак, надо проверить следующее уравнение:
.Попросим Prover 'а прислать Verifier 'у такое простое число
, что , и сертификат о его простоте. Проверим простоту по сертификату и условие . Константу определим позднее.Далее будем вычислять значения и проверять равенства по модулю
.Пусть
.Попросим Prover 'а прислать Verifier 'у формулу
. Проверим следующее утверждение: .Заметим, что размер формулы
будет полином от длины входа Verifier 'а. Этот факт следует из того, что формула имеет степень меньшую либо равную , и она от одной переменной. Поэтому её можно представить так: , и попросить Prover 'а прислать только сами коэффициенты по модулю .Шаг 1.
Пусть
. Отправим программе Prover.Пусть
.Попросим Prover 'а прислать Verifier 'у формулу
. Проверим следующее утверждение: .Шаг 2.
...
Шаг
.Пусть
. Отправим программе Prover.Пусть
.Попросим программу Prover прислать Verifier 'у значение
. Проверим следующее утверждение: . А также сами подставим в и проверим правильность присланного значения .Возвращаем true.
Итак, остается доказать, что написанный Verifier - корректный Verifier для языка . Таким образом, нужно доказать:
- Построенный Verifier - вероятностная машина Тьюринга, совершающая не более полинома от длины входа действий.
- .
- .
Доказательство:
- Из программы Verifier видно, что она работает за .
- Если
- Присылает, например, первое простое число, большее , и сертификат.
- Считает сумму и присылает формулу.
- Получает .
- Считает сумму и присылает формулу.
- ...
имеет ровно удовлетворяющих наборов, то существует такая программа Prover, что . Такая программа:
- Пусть имеет не удовлетворяющих наборов. Тогда для того, что бы Verifier вернул true, необходимо Prover 'у посылать такие , чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:
Шаг 0.
Так как
имеет не удовлетворяющих наборов, то Prover не может послать правильное – не выполнится условие . Поэтому он посылает не , а некое .Шаг 1.
Во первых, отметим, что ситуация леммы Шварца-Зиппеля. Таким образом, с вероятностью большей либо равной и, ввиду того, что должно выполняться условие , получаем, что тоже будет неправильное, т.е. некоторое .
происходит с вероятностью меньшей либо равной для некоторого случайно выбранного , что следует изШаг 2.
...
Шаг
.С вероятностью
, и потому Verifier получит не , а .Из этого процесса заметим, что с вероятностью большей либо равной
мы дойдем до последнего шага и будем имееть вместо . Так как на шаге Verifier вычисляет и проверяет значение, то Verifier вернет false.Так как мы хотим сделать вероятность возврата false большую либо равную
, то выберем так, чтобы . Возьмем . Заметим, что длина есть . Из разложения функции по Тейлору получаем: . Так как - целое неотрицательное число, то: .Утверждение доказано.