17
правок
Изменения
предвАряющий
== Утверждение ==
== Доказательство ==
Левый столбец в этом графе описывает процедуру выборки игроками ∃ и ∀ значений переменных, если игрок выбирает TRUE, он идет в левую сторону, иначе в правую.
Зафиксировав значения переменных, игрок ∀ (т.к. в нашей КНФ-формуле с предворяющими предваряющими кванторами последний квантор ∃) выбирает скобку, значение которой должно быть FALSE (тогда он выиграет!). На рисунке каждая скобка - отдельная вершина c<sub>i</sub>.
После того, как игрок ∀ зафиксировал скобку, игрок ∃ долджен выбрать переменную, значение которой не ноль (игроки уже зафиксировали значения переменных в самом начале) и сделать переход в соответсвующую вершинку. Т.к. значение этой переменной не ноль, то игрок ∀ не сможет никуда пойти из этой вершины (тогда ∃ выиграл, первый игрок обладает выигрышной стратегией в игре Generalized Geography). Для этого проведем ребра из каждый скобки c<sub>i</sub> в вершины, противоположные выбору TRUE или FALSE значений переменных.
