Теорема Шамира - История изменений

Maintenance script: rollbackEdits.php mass rollback

2022-09-04T16:20:43Z

rollbackEdits.php mass rollback

194.26.192.187 в 05:23, 1 сентября 2022

2022-09-01T05:23:53Z

AndrewD в 18:04, 4 июня 2012

2012-06-04T18:04:32Z

AndrewD в 02:09, 4 июня 2012

2012-06-04T02:09:44Z

AndrewD в 23:52, 3 июня 2012

2012-06-03T23:52:53Z

AndrewD в 13:46, 3 июня 2012

2012-06-03T13:46:51Z

192.168.0.2 в 12:05, 20 мая 2010

2010-05-20T12:05:04Z

192.168.0.2 в 12:03, 20 мая 2010

2010-05-20T12:03:10Z

192.168.0.2 в 16:49, 19 мая 2010

2010-05-19T16:49:31Z

192.168.0.2: /* PS ⊂ IP */

2010-05-19T16:15:54Z

‎PS ⊂ IP

← Предыдущая		Версия 16:20, 4 сентября 2022
Строка 1:		Строка 1:
−	~~{\| class="wikitable" align="center" style="color: red; background-color: black; font-size: 56px; width: 800px;"~~
−	\|+
−	~~\|-align="center"~~
−	~~\|'''НЕТ ВОЙНЕ'''~~
−	~~\|-style="font-size: 16px;"~~
−	\|
−	24 февраля 2022 года российское руководство во главе с Владимиром Путиным развязало агрессивную войну против Украины. В глазах всего мира это военное преступление совершено от лица всей страны, всех россиян.
−
−	Будучи гражданами Российской Федерации, мы против своей воли оказались ответственными за нарушение международного права, военное вторжение и массовую гибель людей. Чудовищность совершенного преступления не оставляет возможности промолчать или ограничиться пассивным несогласием.
−
−	Мы убеждены в абсолютной ценности человеческой жизни, в незыблемости прав и свобод личности. Режим Путина — угроза этим ценностям. Наша задача — обьединить все силы для сопротивления ей.
−
−	Эту войну начали не россияне, а обезумевший диктатор. И наш гражданский долг — сделать всё, чтобы её остановить.
−
−	~~''Антивоенный комитет России''~~
−	~~\|-style="font-size: 16px;"~~
−	\|Распространяйте правду о текущих событиях, оберегайте от пропаганды своих друзей и близких. Изменение общественного восприятия войны - ключ к её завершению.
−	~~\|-style="font-size: 16px;"~~
−	\|[https://meduza.io/ meduza.io], [https://www.youtube.com/c/popularpolitics/videos Популярная политика], [https://novayagazeta.ru/ Новая газета], [https://zona.media/ zona.media], [https://www.youtube.com/c/MackNack/videos Майкл Наки].
−	\|}
−
	{{Теорема		{{Теорема
	\|author=Шамир		\|author=Шамир

← Предыдущая		Версия 05:23, 1 сентября 2022
Строка 1:		Строка 1:
		+	{\| class="wikitable" align="center" style="color: red; background-color: black; font-size: 56px; width: 800px;"
		+	\|+
		+	\|-align="center"
		+	\|'''НЕТ ВОЙНЕ'''
		+	\|-style="font-size: 16px;"
		+	\|
		+	24 февраля 2022 года российское руководство во главе с Владимиром Путиным развязало агрессивную войну против Украины. В глазах всего мира это военное преступление совершено от лица всей страны, всех россиян.
		+
		+	Будучи гражданами Российской Федерации, мы против своей воли оказались ответственными за нарушение международного права, военное вторжение и массовую гибель людей. Чудовищность совершенного преступления не оставляет возможности промолчать или ограничиться пассивным несогласием.
		+
		+	Мы убеждены в абсолютной ценности человеческой жизни, в незыблемости прав и свобод личности. Режим Путина — угроза этим ценностям. Наша задача — обьединить все силы для сопротивления ей.
		+
		+	Эту войну начали не россияне, а обезумевший диктатор. И наш гражданский долг — сделать всё, чтобы её остановить.
		+
		+	''Антивоенный комитет России''
		+	\|-style="font-size: 16px;"
		+	\|Распространяйте правду о текущих событиях, оберегайте от пропаганды своих друзей и близких. Изменение общественного восприятия войны - ключ к её завершению.
		+	\|-style="font-size: 16px;"
		+	\|[https://meduza.io/ meduza.io], [https://www.youtube.com/c/popularpolitics/videos Популярная политика], [https://novayagazeta.ru/ Новая газета], [https://zona.media/ zona.media], [https://www.youtube.com/c/MackNack/videos Майкл Наки].
		+	\|}
		+
	{{Теорема		{{Теорема
	\|author=Шамир		\|author=Шамир

← Предыдущая		Версия 18:04, 4 июня 2012
Строка 22:		Строка 22:

	Пусть дана формула <tex>Q_1 \ldots Q_m \phi(x_1, \ldots ,x_m)</tex>. В процессе [[Арифметизация булевых формул с кванторами\|арифметизации]] она перейдет в <tex>R_1 \ldots R_m A_\phi(x_1,\ldots,x_m)</tex>. Воспользуемся протоколом, описанным в [[Лемма о соотношении coNP и IP\|доказательстве принадлежности #SAT к классу IP]]. Для этого необходимо, чтобы степень полиномов <tex>A_i(x_{i+1})</tex> была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду <tex>R_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \ldots L_m A_\phi(x_1,\ldots,x_m)</tex>. Размер новой формулы не превосходит квадрата исходной, степень полиномов не превосходит двух. Тогда, используя условия, описанные в [[Арифметизация булевых формул с кванторами\|леммах 2 и 3]], для проверки ответов, присылаемых ''Prover'' 'ом, можно построить искомый протокол. Значит <tex>\mathrm{TQBF} \in \mathrm{IP}</tex>, следовательно <tex>\mathrm{PS} \subset \mathrm{IP}</tex>.		Пусть дана формула <tex>Q_1 \ldots Q_m \phi(x_1, \ldots ,x_m)</tex>. В процессе [[Арифметизация булевых формул с кванторами\|арифметизации]] она перейдет в <tex>R_1 \ldots R_m A_\phi(x_1,\ldots,x_m)</tex>. Воспользуемся протоколом, описанным в [[Лемма о соотношении coNP и IP\|доказательстве принадлежности #SAT к классу IP]]. Для этого необходимо, чтобы степень полиномов <tex>A_i(x_{i+1})</tex> была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду <tex>R_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \ldots L_m A_\phi(x_1,\ldots,x_m)</tex>. Размер новой формулы не превосходит квадрата исходной, степень полиномов не превосходит двух. Тогда, используя условия, описанные в [[Арифметизация булевых формул с кванторами\|леммах 2 и 3]], для проверки ответов, присылаемых ''Prover'' 'ом, можно построить искомый протокол. Значит <tex>\mathrm{TQBF} \in \mathrm{IP}</tex>, следовательно <tex>\mathrm{PS} \subset \mathrm{IP}</tex>.
−	}},	+	}}

@@ Строка 18: / Строка 18: @@
 В цикле <tex>(1)</tex> перебираются все ''Prover'' 'ы, которые отвечают на <tex>f(n)</tex> запросов, каждый ответ имеет размер <tex>p(n)</tex>. В цикле <tex>(2)</tex> перебираются все вероятностные ленты размера <tex>p(n)</tex>. Так как <tex>V</tex> {{---}} корректен, то если нашелся ''Prover'', при котором <tex>V</tex> допускает слово с вероятностью, большей <tex>\frac{2}{3}</tex>, то данное слово принадлежит <tex>L</tex>, иначе {{---}} не принадлежит. Очевидно, что данная программа требует полином дополнительной памяти. Значит <tex>L \in \mathrm{PS}</tex>, следовательно <tex>\mathrm{IP} \subset \mathrm{PS}</tex>.
 * <tex>\mathrm{PS} \subset \mathrm{IP}</tex>
-== Формулировка ==
+Докажем, что <tex>\mathrm{TQBF} \in \mathrm{IP}</tex>. Так как <tex>\mathrm{TQBF} \in \mathrm{PSC}</tex>, то из этого будет следовать, что <tex>\mathrm{PS} \subset \mathrm{IP}</tex>.
-Введем следующую арифметизацию булевых формул с кванторами:
+Пусть дана формула <tex>Q_1 \ldots Q_m \phi(x_1, \ldots ,x_m)</tex>. В процессе [[Арифметизация булевых формул с кванторами|арифметизации]] она перейдет в <tex>R_1 \ldots R_m A_\phi(x_1,\ldots,x_m)</tex>. Воспользуемся протоколом, описанным в [[Лемма о соотношении coNP и IP|доказательстве принадлежности #SAT к классу IP]]. Для этого необходимо, чтобы степень полиномов <tex>A_i(x_{i+1})</tex> была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду <tex>R_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \ldots L_m A_\phi(x_1,\ldots,x_m)</tex>. Размер новой формулы не превосходит квадрата исходной, степень полиномов не превосходит двух. Тогда, используя условия, описанные в [[Арифметизация булевых формул с кванторами|леммах 2 и 3]], для проверки ответов, присылаемых ''Prover'' 'ом, можно построить искомый протокол. Значит <tex>\mathrm{TQBF} \in \mathrm{IP}</tex>, следовательно <tex>\mathrm{PS} \subset \mathrm{IP}</tex>.
-* <tex>\lnot x \to 1-X</tex>
+}},

@@ Строка 4: / Строка 4: @@
 |proof=
 * <tex>\mathrm{IP} \subset \mathrm{PS}</tex>
-Рассмотрим язык <tex>L \in \mathrm{IP}</tex>, а также ''Verifier'' и ''Prover'', соответствующие этому языку. Так как ''Verifier'' ограничен полиномиальным временем работы, то можно считать, что размер вероятностной ленты, размер ответов ''Prover'' 'а и количество дополнительной памяти, используемой ''Verifier'' 'ом тоже ограничены некоторым полиномом. Построим программу, которая будет перебирать все возможные вероятностные ленты и для каждой из них будет симулировать работу ''Verifier'' 'а, перебирая все возможные ответы ''Prover'' 'а, а затем вернет наиболее часто встречающийся результат, возвращаемый ''Verifier'' 'ом. Данная программа использует полиномиальное количество дополнительной памяти. Значит <tex>L \in \mathrm{PS}</tex>. Поэтому <tex>\mathrm{IP} \subset \mathrm{PS}</tex>
+Рассмотрим язык <tex>L \in \mathrm{IP}</tex>. Пусть <tex>V</tex> {{---}} ''Verifier'', соответствующий <tex>L</tex>, <tex>p(n)</tex> {{---}} время его работы, <tex>f(n)</tex> {{---}} количество его запросов к ''Prover'' 'у. Напишем программу, распознающую язык <tex>L</tex> на полиномиальной памяти.
 * <tex>\mathrm{PS} \subset \mathrm{IP}</tex>
 }}

@@ Строка 1: / Строка 1: @@
 == Формулировка ==
 '''[[Класс IP|IP]]''' = '''[[Класс PS|PS]]'''
@@ Строка 9: / Строка 18: @@
 Введем следующую арифметизацию булевых формул с кванторами:
 * <tex>\lnot x \to 1-X</tex>
-* <tex>x \land y \to XY</tex>
+* <tex>x \land y \to XY</tex>x
 * <tex>x \lor y \to X+Y-XY = 1-(1-X)(1-Y)</tex>
 * <tex>\exists x \varphi(x) \to \sum\limits_{X=0}^{1} A_\varphi(X)</tex>, где <tex>A_\varphi</tex> — полином, получившийся в результате арифметизации <tex>\varphi</tex>

← Предыдущая		Версия 12:05, 20 мая 2010
Строка 26:		Строка 26:
	Хотелось бы воспользоваться протоколом из [[Sharp SAT\|доказательства принадлежности #SAT к классу IP]], проверяя <tex>A_i(1)\cdot A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда <tex>x_i</tex> связан квантором <tex>\forall</tex>, и <tex>A_i(1)+A_i(0)=A_{i-1}(r_{i})</tex> для квантора <tex>\exists</tex>. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза, а это может потребовать передачи по протоколу полиномов экспоненциальной длины, что не уложится по времени.		Хотелось бы воспользоваться протоколом из [[Sharp SAT\|доказательства принадлежности #SAT к классу IP]], проверяя <tex>A_i(1)\cdot A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда <tex>x_i</tex> связан квантором <tex>\forall</tex>, и <tex>A_i(1)+A_i(0)=A_{i-1}(r_{i})</tex> для квантора <tex>\exists</tex>. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза, а это может потребовать передачи по протоколу полиномов экспоненциальной длины, что не уложится по времени.

−	Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора <tex>\forall</tex>. Для этого заменим все суффиксы вида <tex>\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})</tex> на <tex>\forall x_{i+1} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\land \tau(x_1', x_2', \ldots, x_i', x_{i+1})</tex>. Это преобразование не изменит выполнимости формулы, количество ее переменных увеличится лишь в полином от их первоначального количества раз, а сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из [[Sharp SAT\|#SAT]], передаваться будут полиномы константной степени.	+	Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора <tex>\forall</tex>. Для этого заменим все суффиксы вида <tex>\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})</tex> на <tex>\forall x_{i+1} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\land \tau(x_1', x_2', \ldots, x_i', x_{i+1})</tex>. Это преобразование не изменит выполнимости формулы, количество ее переменных увеличится лишь в полином от их первоначального количества раз, а сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из [[Sharp SAT\|#SAT]] для получившейся формулы, передаваться будут полиномы константной степени.

@@ Строка 24: / Строка 24: @@
 * ''P'' выбирает простое <tex>p</tex> и <tex>k \equiv A_\psi \pmod{p}</tex> и посылает их ''V'' (<tex>p</tex> посылается вместе с его сертификатом простоты).
 * ''V'' проверяет <tex>p</tex> на простоту, а <tex>k</tex> на неравенство нулю.
-Хотелось бы воспользоваться протоколом из [[Sharp SAT|доказательства принадлежности #SAT к классу IP]], проверяя <tex>A_i(1)\cdot A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда <tex>x_i</tex> связан квантором <tex>\forall</tex>, и <tex>A_i(1)+A_i(0)=A_{i-1}(r_{i})</tex> для квантора <tex>\exists</tex>. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза. Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора <tex>\forall</tex>. Для этого заменим все суффиксы вида <tex>\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})</tex> на <tex>\forall x_{i+1} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\tau(x_1', x_2', \ldots, x_i', x_{i+1})</tex>. От такого преобразования количество переменных увеличится лишь в полином от их первоначального количества раз, сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из [[Sharp SAT|#SAT]], передаваться будут полиномы не выше второй степени.
+Хотелось бы воспользоваться протоколом из [[Sharp SAT|доказательства принадлежности #SAT к классу IP]], проверяя <tex>A_i(1)\cdot A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда <tex>x_i</tex> связан квантором <tex>\forall</tex>, и <tex>A_i(1)+A_i(0)=A_{i-1}(r_{i})</tex> для квантора <tex>\exists</tex>. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза, а это может потребовать передачи по протоколу полиномов экспоненциальной длины, что не уложится по времени.