Изменения

Для доказательства этого факта сведем [[Интерпретация_БФ_с_кванторами_как_игры_для_двух_игроков|задачу об игре двух игроков ∃ <tex> \exists </tex> и ∀<tex> \forall </tex>]] в булевой КНФ-формуле с предваряющими кванторами (эта задача [[Класс_PS|PS-трудная]]) к Generalized Geography за полиномиальное время.

Для игры двух игроков ∃ и ∀ наша формула представима Если в следующем виде: φ = ∃''x''нашей формуле с предваряющими кванторами последний квантор - не <subtex>1\exists </subtex> ∀''x'', то добавим его, введя дополнительную переменную. Таким образом для игры двух игроков <subtex>2\exists </subtex> ∃''x''и <subtex>3\forall </subtex> наша формула представима в следующем виде:<tex> \varphi = \exists x_1 \forall x_2 \exists x_3 ...∃''x\exists x_n ( \psi ) <sub/tex>n, где <tex> \psi </subtex>''(ψ) , где ψ - некая КНФ-формула.

[[Файл:Generalized_geography_3.png|thumb|350px| Модель графа для сведения задачи об игре двух игроков ∃ <tex> \exists </tex> и ∀ <tex> \forall </tex> к задаче GG]]

Для любой такой КНФ-формулы с предваряющими кванторами можно построить граф, аналогичный приведенному на рисунке. Рассмотрим этот граф, и докажем, что это сведение задачи об игре игроков ∃ <tex> \exists </tex> и ∀ <tex> \forall </tex> к задаче Generalized Geography.

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

Зафиксировав значения переменных, игрок ∀ <tex> \forall </tex> (т.к. в нашей КНФ-формуле с предваряющими кванторами последний квантор ∃<tex> \exists </tex>) выбирает скобку, значение которой должно быть FALSE (тогда он выиграет!). На рисунке каждая скобка - отдельная вершина c<subtex>ic_i </subtex>.

После того, как игрок ∀ <tex> \forall </tex> зафиксировал скобку, игрок ∃ <tex> \exists </tex> долджен выбрать переменную, значение которой не ноль (игроки уже зафиксировали значения переменных в самом начале) и сделать переход в соответсвующую вершинку. Т.к. значение этой переменной не ноль, то игрок ∀ <tex> \forall </tex> не сможет никуда пойти из этой вершины (тогда ∃ <tex> \exists </tex> выиграл, первый игрок обладает выигрышной стратегией в игре Generalized Geography). Для этого проведем ребра из каждый скобки c<subtex>ic_i </subtex> в вершины-переменные, учавствующие в этой скобке, а от них проведем ребра к вершинам левого столбца, соответсвующим выборам TRUE или FALSE значений переменных.

Таким образом, если игрок ∃ <tex> \exists </tex> выигрывает, то автоматически обладает выигрышной стратегией и первый игрок в Generalized Geography. Он знает, какие значения переменных надо выбрать, и в какую вершину пойти в конце. Аналогично, по выигрышной стратегии первого игрока в Generalized Geography можно узнать, какие значения переменных должен выбрать игрок ∃ <tex> \exists </tex> для того, чтобы удовлетворить формулу.

Мы свели задачу об игре игроков ∃ <tex> \exists </tex> и ∀ <tex> \forall </tex> к задаче Generalized Geography. Очевидно, сведение будет произведено за полиномиальное время. Значит, язык GG является PS-трудным, а так как выше мы доказали его принадлежность классу PS, то и PS-полным.