Лемма о соотношении coNP и IP — различия между версиями
м  | 
				м (rollbackEdits.php mass rollback)  | 
				||
| (не показано 15 промежуточных версий 3 участников) | |||
| Строка 3: | Строка 3: | ||
{{Определение  | {{Определение  | ||
|definition=  | |definition=  | ||
| − | <tex>\#SAT=\{\langle \varphi, k \rangle | \varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>.  | + | <tex>\mathrm{\#SAT}=\{\langle \varphi, k \rangle \bigm| \varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>.  | 
}}  | }}  | ||
| Строка 9: | Строка 9: | ||
{{Лемма  | {{Лемма  | ||
|about=1  | |about=1  | ||
| − | |statement=<tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1  A_\phi(x_1, \ldots, x_m)=k \Leftrightarrow \langle\phi,k\rangle \in \#SAT</tex>.  | + | |statement=<tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1  A_\phi(x_1, \ldots, x_m)=k \Leftrightarrow \langle\phi,k\rangle \in \mathrm{\#SAT}</tex>.  | 
|proof=Следует из [[Арифметизация булевых формул с кванторами | леммы (1)]].  | |proof=Следует из [[Арифметизация булевых формул с кванторами | леммы (1)]].  | ||
}}  | }}  | ||
| Строка 16: | Строка 16: | ||
{{Лемма  | {{Лемма  | ||
|about=2  | |about=2  | ||
| − | |statement=<tex>\#SAT \in \mathrm{IP}</tex>.  | + | |statement=<tex>\mathrm{\#SAT} \in \mathrm{IP}</tex>.  | 
|proof=  | |proof=  | ||
Для доказательства леммы построим программы ''Verifier'' и ''Prover'' из [[Интерактивные протоколы. Класс IP. Класс AM#Класс IP|определения]] класса <tex>\mathrm{IP}</tex>.  | Для доказательства леммы построим программы ''Verifier'' и ''Prover'' из [[Интерактивные протоколы. Класс IP. Класс AM#Класс IP|определения]] класса <tex>\mathrm{IP}</tex>.  | ||
| Строка 22: | Строка 22: | ||
Сперва арифметизуем формулу <tex>\phi</tex>. Пусть полученный полином <tex>A(x_1, x_2, ..., x_m)</tex> имеет степень <tex>d</tex>.  | Сперва арифметизуем формулу <tex>\phi</tex>. Пусть полученный полином <tex>A(x_1, x_2, ..., x_m)</tex> имеет степень <tex>d</tex>.  | ||
| − | По лемме (1) вместо условия <tex>\langle \phi, k \rangle \in \#SAT</tex>, можно проверять условие <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1  A_\phi(x_1, \ldots, x_m)=k</tex>.  | + | По лемме (1) вместо условия <tex>\langle \phi, k \rangle \in \mathrm{\#SAT}</tex>, можно проверять условие <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1  A_\phi(x_1, \ldots, x_m)=k</tex>.  | 
Приступим к описанию ''Verifier'''а.  | Приступим к описанию ''Verifier'''а.  | ||
| Строка 30: | Строка 30: | ||
Если <tex>d=0</tex> или <tex>m=0</tex>, то ''Verifier'' может проверить указанное выше условие сам и вернуть соответствующий результат.  | Если <tex>d=0</tex> или <tex>m=0</tex>, то ''Verifier'' может проверить указанное выше условие сам и вернуть соответствующий результат.  | ||
Иначе запросим у ''Prover'''а такое простое число <tex>p</tex>, что <tex>3dm \le p \le 6dm</tex> (такое <tex>p</tex> существует в силу [http://ru.wikipedia.org/wiki/Постулат_Бертрана постулата Бертрана]).    | Иначе запросим у ''Prover'''а такое простое число <tex>p</tex>, что <tex>3dm \le p \le 6dm</tex> (такое <tex>p</tex> существует в силу [http://ru.wikipedia.org/wiki/Постулат_Бертрана постулата Бертрана]).    | ||
| − | Проверим <tex>p</tex> на простоту и на принадлежность заданному промежутку. Как мы [[Класс P#Примеры задач и языков из P|знаем]], <tex>Primes \in \mathrm{P}</tex>, следовательно на эти операции у ''Verifier'''а уйдёт полиномиальное от размера входа время.  | + | Проверим <tex>p</tex> на простоту и на принадлежность заданному промежутку. Как мы [[Класс P#Примеры задач и языков из P|знаем]], <tex>\mathrm{Primes} \in \mathrm{P}</tex>, следовательно на эти операции у ''Verifier'''а уйдёт полиномиальное от размера входа время.  | 
Далее будем проводить все вычисления модулю <tex>p</tex>.  | Далее будем проводить все вычисления модулю <tex>p</tex>.  | ||
Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_0(x_1)= \sum\limits_{x_2 = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(x_1, x_2, ..., x_m)</tex>.    | Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_0(x_1)= \sum\limits_{x_2 = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(x_1, x_2, ..., x_m)</tex>.    | ||
| − | Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длины входа ''Verifier'' 'а, так как <tex>A_0(x_1)</tex> полином   | + | Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длины входа ''Verifier'' 'а, так как <tex>A_0(x_1)</tex> — полином степени не выше, чем <tex>d</tex>, от одной переменной, а значит его можно представить в виде <tex>A_0(x) = \sum\limits_{i = 0}^{d} C_i \cdot x ^ i</tex>.  | 
Проверим следующее утверждение: <tex>A_0(0) + A_0(1) = k</tex> (*) (здесь и далее под словом «проверим» будем подразумевать следующее: если утверждение верно, ''Verifier'' продолжает свою работу, иначе он прекращает свою работу и возвращет '''false''').  | Проверим следующее утверждение: <tex>A_0(0) + A_0(1) = k</tex> (*) (здесь и далее под словом «проверим» будем подразумевать следующее: если утверждение верно, ''Verifier'' продолжает свою работу, иначе он прекращает свою работу и возвращет '''false''').  | ||
| Строка 41: | Строка 41: | ||
'''Шаг i'''  | '''Шаг i'''  | ||
| − | Пусть <tex>r_i = random(p)</tex>. Отправим <tex>r_i</tex> программе ''Prover''.  | + | Пусть <tex>r_i = random(0..p-1)</tex>. Отправим <tex>r_i</tex> программе ''Prover''.  | 
Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_i(x_{i+1}) = \sum\limits_{x_{i+2} = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(r_1,\ldots, r_i, x_{i+1}, ..., x_m)</tex>.  | Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_i(x_{i+1}) = \sum\limits_{x_{i+2} = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(r_1,\ldots, r_i, x_{i+1}, ..., x_m)</tex>.  | ||
| Строка 49: | Строка 49: | ||
'''Шаг m'''  | '''Шаг m'''  | ||
| − | Пусть <tex>r_m = random(p)</tex>. Отправим <tex>r_m</tex> программе ''Prover''.  | + | Пусть <tex>r_m = random(0..p-1)</tex>. Отправим <tex>r_m</tex> программе ''Prover''.  | 
Попросим программу ''Prover'' прислать ''Verifier'' 'у значение <tex>A_m()= A(r_1, r_2, ..., r_m)</tex>.  | Попросим программу ''Prover'' прислать ''Verifier'' 'у значение <tex>A_m()= A(r_1, r_2, ..., r_m)</tex>.  | ||
| Строка 60: | Строка 60: | ||
Докажем теперь, что построенный таким образом ''Verifier'' — корректный. Для этого нужно доказать следующие утверждения:  | Докажем теперь, что построенный таким образом ''Verifier'' — корректный. Для этого нужно доказать следующие утверждения:  | ||
# Построенный ''Verifier'' - вероятностная машина Тьюринга, совершающая не более полинома от длины входа действий.  | # Построенный ''Verifier'' - вероятностная машина Тьюринга, совершающая не более полинома от длины входа действий.  | ||
| − | # <tex>\langle \varphi, k \rangle \in \#SAT \Rightarrow \exists Prover : P(Verifier^{Prover}(\langle \varphi, k \rangle)) \ge 2/3</tex>.  | + | # <tex>\langle \varphi, k \rangle \in \mathrm{\#SAT} \Rightarrow \exists \mathit{Prover} : P(\mathit{Verifier^{Prover}}(\langle \varphi, k \rangle)=1) \ge 2/3</tex>.  | 
| − | # <tex>\langle \varphi, k \rangle \notin \#SAT \Rightarrow \forall Prover : P(Verifier^{Prover}(\langle \varphi, k \rangle)) \le 1/3</tex>.  | + | # <tex>\langle \varphi, k \rangle \notin \mathrm{\#SAT} \Rightarrow \forall \mathit{Prover} : P(\mathit{Verifier^{Prover}}(\langle \varphi, k \rangle)=1) \le 1/3</tex>.  | 
| + | |||
| + | Докажем эти утверждения.  | ||
#Первый факт следует из построения ''Verifier'' 'а.  | #Первый факт следует из построения ''Verifier'' 'а.  | ||
| − | #По [[Арифметизация булевых формул с кванторами | лемме (2)]], если <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1  A_\phi(x_1, \ldots, x_m)=k</tex>, то условия (*) выполнятются, следовательно существует такой ''Prover'', что <tex>P(Verifier^{Prover}(\langle\phi,k\rangle)) = 1</tex>, для любой пары <tex>\langle\phi,k\rangle \in \#SAT</tex>.  | + | #По [[Арифметизация булевых формул с кванторами | лемме (2)]], если <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1  A_\phi(x_1, \ldots, x_m)=k</tex>, то условия (*) выполнятются, следовательно существует такой ''Prover'', что <tex>P(\mathit{Verifier^{Prover}}(\langle\phi,k\rangle)) = 1</tex>, для любой пары <tex>\langle\phi,k\rangle \in \mathrm{\#SAT}</tex>.  | 
#Пусть количество наборов, удовлетворяющих <tex>\phi</tex>, не равно <tex>k</tex>. Для того, что бы ''Verifier'' вернул '''true''', ''Prover'' 'у необходимо посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:  | #Пусть количество наборов, удовлетворяющих <tex>\phi</tex>, не равно <tex>k</tex>. Для того, что бы ''Verifier'' вернул '''true''', ''Prover'' 'у необходимо посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:  | ||
:'''Шаг 0'''  | :'''Шаг 0'''  | ||
| − | :Так как количество наборов, удовлетворяющих <tex>\phi</tex>, не равно <tex>k</tex>, то ''Prover'' не может послать правильное <tex>A_0</tex>   | + | :Так как количество наборов, удовлетворяющих <tex>\phi</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>.  | 
| − | :'''Шаг   | + | :<tex>\ldots</tex>  | 
| − | :  | + | :'''Шаг i'''  | 
| + | :Заметим, что если на каком-то шаге <tex>A_{i-1}(r_i) = \tilde{A}_{i-1}(r_i)</tex>, то начиная со следующего шага ''Prover'' может посылать правильные <tex>A_j</tex> и в итоге ''Verifier'' вернёт '''true'''.  | ||
| + | :Для некоторого случайно выбранного <tex>r_i</tex> вероятность того, что <tex>A_{i-1}(r_i) = \tilde{A}_{i-1}(r_i)</tex>, то есть <tex>r_i</tex> — корень полинома <tex>(A_{i-1} - \tilde{A}_{i-1})(r_i)</tex>, имеющего степень не больше <tex>d</tex>, не превосходит <tex>\frac{d}{p}</tex>.  | ||
:<tex>\ldots</tex>  | :<tex>\ldots</tex>  | ||
:'''Шаг m'''  | :'''Шаг m'''  | ||
| − | :   | + | :Так как на последнем шаге ''Verifier'' полученным от ''Prover'' значение с непосредственно вычисленным, слово будет допущено только в том случае, когда ''Prover'' смог прислать верное значение, что в свою очередь возможно лишь если на одном из предыдущих шагов был верно угадан корень полинома.  | 
:  | :  | ||
| − | :  | + | :Вычислим вероятность того, что хотя бы раз корень был угадан.  | 
| − | :  | + | :<tex>P(\mathit{Verifier^{Prover}}(\langle \varphi, k \rangle)=1) = 1 - (1 - \frac d p)^m \le 1 - (1 - \frac d {3dm})^m \le \frac 1 3</tex>.  | 
| − | + | :В последнем переходе мы воспользовались [http://ru.wikipedia.org/wiki/Ряд_Тейлора формулой Тейлора] для логарифма и экспоненты, а также тем, что <tex>m>0</tex>.  | |
| − | |||
Таким образом, построенный нами ''Verifier'' корректен, а значит лемма доказана.  | Таким образом, построенный нами ''Verifier'' корректен, а значит лемма доказана.  | ||
| Строка 87: | Строка 90: | ||
|statement=<tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.  | |statement=<tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.  | ||
|proof=  | |proof=  | ||
| − | Сведём язык <tex>TAUT</tex> к языку <tex>\#SAT</tex> следующим образом: <tex>\phi \mapsto \langle \phi, 2^k \rangle </tex>, где <tex>k</tex> — количество различных переменных в формуле <tex>\phi</tex>.  | + | Сведём язык <tex>\mathrm{TAUT}</tex> к языку <tex>\mathrm{\#SAT}</tex> следующим образом: <tex>\phi \mapsto \langle \phi, 2^k \rangle </tex>, где <tex>k</tex> — количество различных переменных в формуле <tex>\phi</tex>.  | 
| − | Очевидно, что <tex>\phi \in TAUT \Leftrightarrow \langle \phi, 2^k \rangle \in \#SAT</tex>.  | + | Очевидно, что <tex>\phi \in \mathrm{TAUT} \Leftrightarrow \langle \phi, 2^k \rangle \in \mathrm{\#SAT}</tex>.  | 
| − | По лемме (2) <tex>\#SAT \in \mathrm{IP}</tex>. Тогда <tex>TAUT \in \mathrm{IP}</tex>. Так как <tex>TAUT \in \mathrm{coNPC}</tex>, то <tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.  | + | По лемме (2) <tex>\mathrm{\#SAT} \in \mathrm{IP}</tex>. Тогда <tex>\mathrm{TAUT} \in \mathrm{IP}</tex>. Так как <tex>\mathrm{TAUT} \in \mathrm{coNPC}</tex>, то <tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.  | 
}}  | }}  | ||
[[Категория: Теория сложности]]  | [[Категория: Теория сложности]]  | ||
Текущая версия на 19:05, 4 сентября 2022
| Определение: | 
| имеет ровно удовлетворяющих наборов . | 
| Лемма (1): | 
.  | 
| Доказательство: | 
| Следует из леммы (1). | 
| Лемма (2): | 
.  | 
| Доказательство: | 
| 
 Для доказательства леммы построим программы Verifier и Prover из определения класса . Сперва арифметизуем формулу . Пусть полученный полином имеет степень . По лемме (1) вместо условия , можно проверять условие . Приступим к описанию Verifier'а. Шаг 0 Если или , то Verifier может проверить указанное выше условие сам и вернуть соответствующий результат. Иначе запросим у Prover'а такое простое число , что (такое существует в силу постулата Бертрана). Проверим на простоту и на принадлежность заданному промежутку. Как мы знаем, , следовательно на эти операции у Verifier'а уйдёт полиномиальное от размера входа время. Далее будем проводить все вычисления модулю . Попросим Prover 'а прислать Verifier 'у формулу . Заметим, что размер формулы будет полином от длины входа Verifier 'а, так как — полином степени не выше, чем , от одной переменной, а значит его можно представить в виде . Проверим следующее утверждение: (*) (здесь и далее под словом «проверим» будем подразумевать следующее: если утверждение верно, Verifier продолжает свою работу, иначе он прекращает свою работу и возвращет false). Шаг i Пусть . Отправим программе Prover. Попросим Prover 'а прислать Verifier 'у формулу . Проверим следующее утверждение: (*). Шаг m Пусть . Отправим программе Prover. Попросим программу Prover прислать Verifier 'у значение . Проверим следующее утверждение: (*). А также сами подставим в и проверим правильность присланного значения . Возвращаем true. Докажем теперь, что построенный таким образом Verifier — корректный. Для этого нужно доказать следующие утверждения: 
 Докажем эти утверждения. 
 
  | 
| Лемма (3): | 
.  | 
| Доказательство: | 
| 
 Сведём язык к языку следующим образом: , где — количество различных переменных в формуле . Очевидно, что . По лемме (2) . Тогда . Так как , то . |