Формулы с кванторами и игры: самые трудные задачи в PSPACE

Если ты вычислишь формулу с чередующимися кванторами, объяснишь, почему порядок кванторов менять нельзя, и покажешь, как вопрос о выигрыше в игре записывается такой формулой, - листай до «Теперь сам».

Как думаешь, что предъявить в доказательство выигрыша

Формула выполнима - предъявляешь набор значений, и любой проверит. Теперь позиция в игре, и ты утверждаешь, что у первого игрока есть выигрыш при любой игре второго.

Ответь себе до чтения: что служит сертификатом такого утверждения? Одного хода мало: противник спросит, что ты сделаешь в ответ на каждый из его ходов. Нужен ход, потом ответ на каждый возможный ответ, потом ответ на каждый ответ на эти ответы. Это дерево, и оно растёт экспоненциально с длиной партии. Короткого свидетельства не видно, и похоже, что его нет: задачи об играх труднее задач из NP, если только NP не совпадает с классом PSPACE из этой главы.

На что это похоже

Пари с придирчивым оппонентом. «Я назову число, и что бы ты ни назвал в ответ, я смогу назвать третье так, чтобы сумма делилась на семь». Ты ходишь первым, он пытается тебя опровергнуть, ты отвечаешь.

Утверждение истинно, если у тебя есть способ выигрывать пари всегда. Слова «существует» - твои ходы, слова «для любого» - его. От порядка всё зависит: «для любого его числа найдётся моё» и «найдётся моё число, годное для любого его» - разные пари, и второе выиграть гораздо труднее.

Механизм: кванторы, рекурсия и игры

Формула с кванторами - формула в КНФ, перед которой каждая переменная связана одним из двух слов: ∃ - «существует значение», ∀ - «при любом значении». Кванторы читаются слева направо.

∃x₁ ∃x₂ … ∃xₙ  формула          обычная выполнимость, SAT
∀x₁ ∀x₂ … ∀xₙ  формула          формула истинна на всех наборах
∃x₁ ∀x₂ ∃x₃ …  формула          чередование: игра

Порядок важен. Пусть формула утверждает x = y.

∀x ∃y  (x = y)      истинно:  для каждого x выбираем такой же y
∃y ∀x  (x = y)      ложно:    один y не равен обоим значениям x

Во втором случае y выбирается раньше, чем становится известен x.

Вычисление. Формула с первым квантором ∃x истинна, если она истинна при x = ложь или при x = истина; с первым квантором ∀x - если при обоих значениях. Получается рекурсия: подставить ложь, вычислить остаток; подставить истину, вычислить остаток; соединить через «или» либо «и». Глубина рекурсии равна числу переменных, на каждом уровне хранится одно значение. Память линейна. Время - порядка 2ⁿ вычислений формулы: дерево просматривается целиком.

Полнота. Задача «истинна ли формула с кванторами» лежит в PSPACE и полна в нём: любая задача, решаемая в полиномиальной памяти, сводится к ней за полиномиальное время. Идея та же, что в теореме Сэвича: «существует середина пути, такая что для обеих половин…» - это уже чередование «существует» и «для любого», записанное формулой. Чтобы формула не удваивалась на каждом уровне, две половины пишут один раз - под квантором «для любой пары концов, совпадающей с одной из двух нужных»: лишние пары отсекает условие внутри формулы. Кванторы здесь стоят над конфигурациями машины, а конфигурация - это набор булевых переменных, по одной на бит.

Игры. Двое ходят по очереди и видят все сделанные ходы, партия не длиннее полинома от размера позиции, а допустимость хода и исход партии проверяются в полиномиальной памяти. «У первого игрока есть выигрыш» значит:

существует мой ход, такой что
    для любого ответа противника
        существует мой ход, такой что
            …  в конце я выиграл

Позиция выигрышна для того, чей ход, если из неё есть ход в позицию, проигрышную для противника. Рекурсия по ходам совпадает с рекурсией по кванторам, и памяти ей нужно на одну позицию и один ход для каждого хода партии.

Для многих игр, обобщённых на поле произвольного размера, вопрос о победителе полон в PSPACE; обобщение нужно, потому что на поле одного размера позиций конечное число и говорить о росте сложности не о чем. Так обстоит дело с игрой, где по очереди называют города на последнюю букву, не повторяясь, с гексом (на шестиугольной сетке соединяют два своих края), с реверси. Туда же попадают головоломки для одного игрока: передвижение ящиков по складу, выезд машины из пробки. Противника в них нет, но решение бывает экспоненциально длинным и коротким сертификатом не служит; в PSPACE они лежат как достижимость в графе позиций, по теореме Сэвича.

Правило

Формула с кванторами ∃ и ∀ вычисляется рекурсией по переменным: ∃ - «или» двух ветвей, ∀ - «и». Память линейна, время 2ⁿ. Задача полна для PSPACE. Вопрос «есть ли выигрыш» в игре двух лиц с открытыми ходами и полиномиальной длиной партии - формула с чередующимися кванторами; позиция выигрышна, если есть ход в проигрышную для противника.

Разбор: одна формула, четыре расстановки кванторов

Функция istinna получает строку кванторов - E для «существует», A для «для любого» - и формулу в КНФ. Счётчик считает вызовы. Первая формула утверждает x₁ = x₂: скобки (x₁ ∨ ¬x₂) и (¬x₁ ∨ x₂) вместе запрещают разные значения. Вторая - четыре скобки над четырьмя переменными. Переменные нумеруются с единицы, нулевая ячейка набора не используется.

def istinna(kvantory, formula, nabor, i, schyot):
    schyot[0] = schyot[0] + 1
    if i == len(kvantory):
        for skobka in formula:
            est = False
            for literal in skobka:
                if (literal > 0) == nabor[abs(literal)]:
                    est = True
            if not est:
                return False
        return True
    nabor[i + 1] = False
    pri_lozhnom = istinna(kvantory, formula, nabor, i + 1, schyot)
    nabor[i + 1] = True
    pri_istinnom = istinna(kvantory, formula, nabor, i + 1, schyot)
    if kvantory[i] == "E":
        return pri_lozhnom or pri_istinnom
    return pri_lozhnom and pri_istinnom

ravny = [[1, -2], [-1, 2]]
for kvantory in ["EE", "AE", "EA", "AA"]:
    schyot = [0]
    print(kvantory, istinna(kvantory, ravny, [False] * 3, 0, schyot),
          schyot[0])
formula = [[1, 2, -3], [-1, 3, 4], [-2, -4], [3, -4, 1]]
for kvantory in ["EEEE", "EAEA", "AEAE", "AAAA"]:
    schyot = [0]
    print(kvantory, istinna(kvantory, formula, [False] * 5, 0, schyot),
          schyot[0])

EE True 7
AE True 7
EA False 7
AA False 7
EEEE True 31
EAEA False 31
AEAE True 31
AAAA False 31

Первые четыре строки - формула x₁ = x₂. При ∃∃ она истинна: значения можно выбрать равными. При ∀∃ тоже: x₂ выбирается после x₁ и подстраивается. При ∃∀ ложна: x₁ выбран заранее, а x₂ пробегает оба значения. При ∀∀ ложна тем более. Одна формула, четыре разных утверждения.

Вторая формула выполнима (EEEE) и не тождественно истинна (AAAA). Между этими крайностями ответ зависит от того, кому какая переменная досталась: EAEA ложно, AEAE истинно. В первом случае противнику достались x₂ и x₄: он берёт обе истинными, и скобка (¬x₂ ∨ ¬x₄) ложна, что бы ни выбрал игрок «существует». Во втором эти переменные у самого игрока, и он отвечает на ходы противника.

Вызовов 7 и 31 - полное дерево высоты два и четыре. Память - список nabor и стек глубиной в число переменных: одна ветвь за раз. Для ста переменных это сто значений и порядка 2¹⁰¹ вызовов.

Разбор: игра в камни как формула

В кучке лежат камни; за ход можно взять один, три или четыре. Проигрывает тот, кому нечего брать. Функция vyigryvaet отвечает, выигрывает ли тот, чей ход: есть ли ход, после которого противник в проигрышной позиции.

def vyigryvaet(kamnej, hody, schyot):
    schyot[0] = schyot[0] + 1
    for h in hody:
        if h <= kamnej and not vyigryvaet(kamnej - h, hody, schyot):
            return True
    return False

itogi = ""
for n in range(15):
    schyot = [0]
    if vyigryvaet(n, [1, 3, 4], schyot):
        itogi = itogi + "В"
    else:
        itogi = itogi + "П"
print(itogi)
for n in [10, 14, 18, 22]:
    schyot = [0]
    print(n, vyigryvaet(n, [1, 3, 4], schyot), schyot[0])

ПВПВВВВПВПВВВВП
10 True 68
14 False 545
18 True 2184
22 True 8738

Первая строка - позиции от нуля до четырнадцати камней: П - проигрыш того, чей ход, В - выигрыш. Ноль камней - проигрыш: ходить нечем. Один - выигрыш: берём камень и оставляем противнику ноль. Два - проигрыш: единственный ход ведёт в выигрышную для противника позицию. Узор ПВПВВВВ повторяется с периодом семь.

Функция в одну строку по смыслу: «существует ход, после которого противник не выигрывает». Слово «не» переворачивает точку зрения: «у противника не существует выигрышного хода» - то же, что «для любого его хода он оказывается в проигрыше». Отрицание превращает «существует» в «для любого», и получается то самое чередование.

Число вызовов растёт экспоненциально: 68, 545, 2184, 8738 - в несколько раз на каждые четыре камня. При этом разных позиций всего n + 1, и запоминание ответов сделало бы счёт линейным. Игра в камни лёгкая, потому что позиций мало. У игр на доске позиция - расстановка фигур, позиций экспоненциально много, и запоминание уже не спасает: это и отличает полные для PSPACE игры от игры в камни.

Что ломается без этого

Кванторы переставлены. «Для каждого запроса есть сервер, который его обслужит» и «есть сервер, который обслужит каждый запрос» - разные требования к системе.

Игру пытаются решить как выполнимость. Решатель выполнимости находит один набор. Игре нужен ответ на каждый ход противника; это формула с чередованием, и инструменты для неё другие и слабее.

Стратегию принимают за ход. «Лучший ход» без ответа на все возражения - не доказательство выигрыша.

Запоминание считают спасением. Оно помогает, когда позиций полиномиально много. На доске их экспоненциально много, и таблица не поместится.

Зачем это в работе

Планирование против неопределённости. «Существует ли план, который достигает цели при любом отказе одного узла» - формула с двумя кванторами. Такие вопросы труднее обычного планирования, и это надо знать до того, как обещать «устойчивое» расписание.

Синтез и проверка управляющих программ. Контроллер играет против среды: на любое её действие у него должен быть безопасный ответ. Проверка таких свойств - вычисление игры на графе состояний.

Игровые программы. Перебор «мой ход - его ответ» с отсечениями - прямое вычисление формулы с кванторами: ветвь «для любого» бросают, найдя одно опровержение, ветвь «существует» - найдя одно подтверждение.

Теперь сам

1. Истинно ли ∃x ∀y (x ∨ y)? А ∀y ∃x (x ∨ y)?
2. Формула утверждает x ≠ y. При каких из четырёх расстановок кванторов она истинна?
3. В игре с ходами 1, 3, 4 в кучке девять камней. Кто выигрывает - тот, чей ход, или его противник?
4. Сколько памяти и сколько времени нужно рекурсии для формулы с пятьюдесятью переменными?
5. Почему для игры на доске запоминание позиций не делает перебор полиномиальным?