Изменения

Для доказательства этого факта сведем задачу о выполнимости булевой формулы с предваряющими кванторами в форме КНФ (эта задача PS-трудная) к Generalized Geography за полиномиальное время. Для этого воспользуемся тем, что булеву формулу с кванторами можно интерпретировать как игру двух игроков ∃ и ∀.

Булева формула с кванторами имеет следующий вид: φ = Q₁''x''₁ Q₂''x''₂ Q₃''x''₃ ...''Q_kx_k''(ψ) где ''Q_i'' квантор ∃ или ∀, а ψ - некоторая булева формула. Заметим, что любую такую формулу можно преобразовать к виду φ = ∃''x''₁ ∀''x''₂ ∃''x''₃ ...∃''x_kn''(ψ) , добавив необходимое количество переменных с кванторами. Если булева формула возвращает TRUE после ходов Представим получившуюся формулу как игру игроков По∃ и ∀. Игрок ∃ здесь -любому и Существуетпервый игрок в Generalized Geography, а игрок ∀ - второй. Таким образом, если ∃ выигрывает в своей игре, то выиграл Существует, иначе выиграл По-любомупервый игрок обладает выигрышной стратегией в игре Generalized Geography. Осталось по булевой формуле с предваряющими кванторами получить соотвествующий граф для игры в Generalized Geography.

Построив Для любой формулы можно построить граф, аналогичный графу, приведенному на рисунке. Рассмотрим этот граф, и докажем, для любой что это сведение задачи о выполнимости булевой формулы с кванторами, мы сможем свести задачу о выигрывании игрока Существует к задаче о наличии выигрышной стратегии у первого игрока в Generalized Geography.

Левый столбец в этом графе описывает процедуру выборки игроками ∃ и ∀ значений переменных, если игрок выбирает TRUE, он идет в левую сторону, иначе в правую.

Зафиксировав значения переменных, игрок По-любому ∀ (т.к. в нашей КНФ-формуле с предворяющими кванторами последний квантор Существует∃) выбирает скобку, значение которой может должно быть FALSE (тогда он выиграет!). На рисунке каждая скобка - отдельная вершина cic_i.

После того, как игрок По-Любому ∀ зафиксировал скобку, игрок Существует выбирает ∃ долджен выбрать переменную, значение которой не ноль (игроки уже зафиксировали значения переменных в самом начале) и делает сделать переход в соответсвующую вершинку. Т.к. значение этой переменной не ноль, то игрок По-любому ∀ не сможет никуда пойти из этой вершины(тогда ∃ выиграл, первый игрок обладает выигрышной стратегией в игре Generalized Geography). Для этого проведем ребра из каждый скобки c_i в вершины, соответствующие противоположные выбору TRUE или FALSE значений переменных. Таким образом, если игрок ∃ выигрывает, то автоматически обладает выигрышной стратегией и первый игрок в Generalized Geography. Он знает, какие значения переменных надо выбрать, и в какую вершину пойти в конце. Аналогично, по выигрышной стратегии первого игрока в Generalized Geography можно узнать, какие значения переменных должен выбрать игрок ∃ для того, чтобы формула выполнилась.  Мы свели задачу о выполнимости булевой формулы с предваряющими кванторами к задача Generalized Geography. Значит, язык GG является PS-трудным, а так как выше мы доказали его принадлежность классу PS, то и PS-полным.