Решение, если количественная логическая формула, такая как
всегда оценивается как истина - это классическая PSPACE-полная проблема. Это можно рассматривать как игру двух игроков с чередующимися ходами. Первый игрок решает значение истинности переменных с нечетными номерами, а второй игрок решает значение истинности переменных с четными номерами. Первый игрок пытается сделать ложным, а второй игрок пытается сделать это правдой. Решение о том, кто имеет выигрышную стратегию, полностью завершено.
Я рассматриваю аналогичную проблему с двумя игроками, один пытается сделать булеву формулу истинной, а другой - ложной. Разница в том, что на ходу игрок может выбрать для него переменную и значение истины (например, в самом первом ходу игрок 1 может решить установить значение в true, а затем в следующем ходу игрок 2 может решить установить в false). Это означает, что игроки могут решить, какие из переменных (из тех, которым еще не было назначено значение истинности) они хотят назначить значение истинности, вместо того, чтобы играть в игру в порядке .
Задача задается булевой формулой для переменных, чтобы решить, имеет ли первый игрок (пытающийся сделать его ложным) или второй (пытающийся сделать это правдивым) выигрышную стратегию. Эта проблема явно осталась в PSPACE, поскольку дерево игр имеет линейную глубину.
Остаётся ли PSPACE завершенным?
Мы доказали, что эта игра является PSPACE-полной для 5-CNF, но имеет алгоритм линейного времени для 2-CNF. Предыдущий лучший результат был 6-CNF Ahlroth и Orponen.
Вы можете найти документ конференции на ISAAC 2018 .
Обновление: 16 ноября 2019 г.
Мы доказали, что игра доступна для 3-CNF с некоторыми ограничениями для 3-CNF. Мы также радикально предположили, что эта игра также доступна без ограничений для 3-CNF. Вы можете найти первоначальную версию на ECCC .
источник