PS-полнота языка верных булевых формул с кванторами (TQBF) — различия между версиями
Komarov (обсуждение | вклад) |
|||
Строка 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 Майкл Наки]. | ||
+ | |} | ||
+ | |||
{{Определение | {{Определение | ||
|definition=<tex>\mathrm{TQBF}</tex> расшифровывается как '''True Quantified Boolean Formula'''. Это язык верных булевых формул с кванторами.<br/> | |definition=<tex>\mathrm{TQBF}</tex> расшифровывается как '''True Quantified Boolean Formula'''. Это язык верных булевых формул с кванторами.<br/> |
Версия 09:03, 1 сентября 2022
НЕТ ВОЙНЕ |
24 февраля 2022 года российское руководство во главе с Владимиром Путиным развязало агрессивную войну против Украины. В глазах всего мира это военное преступление совершено от лица всей страны, всех россиян. Будучи гражданами Российской Федерации, мы против своей воли оказались ответственными за нарушение международного права, военное вторжение и массовую гибель людей. Чудовищность совершенного преступления не оставляет возможности промолчать или ограничиться пассивным несогласием. Мы убеждены в абсолютной ценности человеческой жизни, в незыблемости прав и свобод личности. Режим Путина — угроза этим ценностям. Наша задача — обьединить все силы для сопротивления ей. Эту войну начали не россияне, а обезумевший диктатор. И наш гражданский долг — сделать всё, чтобы её остановить. Антивоенный комитет России |
Распространяйте правду о текущих событиях, оберегайте от пропаганды своих друзей и близких. Изменение общественного восприятия войны - ключ к её завершению. |
meduza.io, Популярная политика, Новая газета, zona.media, Майкл Наки. |
Определение: |
. | расшифровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами.
Определение: |
— это пропозициональная формула с кванторами. Кванторы для каждой переменной записываются в начале выражения. |
Лемма (1): |
. |
Доказательство: |
Чтобы доказать это, просто приведём программу , решающую булеву формулу с кванторами на дополнительной памяти и работающую за конечное время.Эта программа требует if n == 0 return if return if return дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — . |
Лемма (2): |
. |
Доказательство: |
Рассмотрим язык . Построим такую функцию , что и , где — полином.Так как , то существует детерминированная машина Тьюринга , распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины есть , где — полином, а — длина входа.Пусть , — конфигурация . Конфигурация задаётся позицией и содержанием рабочей ленты. Введём обозначение — в конфигурации на -том месте стоит символ . Тогда размер конфигурации равен . Следовательно всего конфигураций .Под выражением будем понимать Аналогично выражение обозначаетРассмотрим функцию , проверяющую следующее условие: конфигурация достижима из конфигурации не более, чем за шагов.. . Общую длину получившейся формулы можно представить как . Заметим, что из-за умножения на 2 на каждом шаге рекурсии будет иметь экспоненциальный размер относительно . Нас это не устраивает, так как нам необходимо полиномиальное сведение. Поэтому воспользуемся квантором и перепишем её следующим образом:. Получившаяся формула верна, если существует такая промежуточная конфигурация , что для любых конфигураций и из того, что эти конфигурации нам интересны следует, что верно . А значит, конфигурация достижима из конфигурации не более, чем за шагов.За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как , где . Следовательно, размер полученной функции полиномиален относительно .Теперь мы можем записать функцию , которая будет переводить ДМТ и слово на ленте в формулу из .. Выражения и можно записать следующим образом:. .
Если , то существует путь из стартовой конфигурации в финишную, длины не более, чем , а значит формула верна.Если формула Таким образом, оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем . Значит, ДМТ допускает слово . Тогда . . |
Теорема: |
. |
Доказательство: |
Доказательство непосредственно следует из лемм. |