Czy ta odmiana TQBF jest wciąż kompletna z PSPACE?

Decydowanie, czy skwantyfikowana formuła boolowska, taka jak

$\forall x_1 \exists x_2 \forall x_3\cdots \exists x_n \varphi(x_1, x_2,\ldots , x_n),$

zawsze ocenia na prawdę, to klasyczny problem z PSPACE. Można to postrzegać jako grę między dwoma graczami, z naprzemiennymi ruchami. Pierwszy gracz decyduje o wartości prawdziwej zmiennych o nieparzystych liczbach, a drugi gracz decyduje o wartości prawdziwej zmiennych o nieparzystych liczbach. Pierwszy gracz próbuje zrobić $\varphi$ fałszywe, a drugie stara zawodnika, aby to prawda. Podjęcie decyzji o zwycięskiej strategii jest kompletne z PSPACE.

Rozważam podobny problem z dwoma graczami, z których jeden próbuje sprawić, by boolowska formuła $\varphi$ prawdziwa, a drugi próbował sprawić, by była fałszywa. Różnica polega na tym, że podczas ruchu gracz może wybrać dla niego zmienną i wartość prawdy (na przykład, jako pierwszy ruch, gracz może zdecydować o ustawieniu $x_8$ na wartość true, a następnie w następnym ruchu gracz drugi może zdecyduj, aby ustawić $x_3$ na false). Oznacza to, że gracze mogą zdecydować, które ze zmiennych (spośród tych, którym nie przypisano jeszcze wartości prawdy), chcą przypisać wartość prawdy, zamiast grać w grę w kolejności $x_1 , \ldots , x_n$ .

Problem otrzymuje formułę boolowską $\varphi$ na $n$ zmiennych, aby zdecydować, czy gracz jeden (próbując uczynić to fałszywym), czy gracz drugi (próbując sprawić, by był prawdziwy) ma zwycięską strategię. Ten problem jest nadal widoczny w PSPACE, ponieważ drzewo gry ma liniową głębokość.

Czy PSPACE pozostaje kompletna?

Jest to gra z nieuporządkowanym ograniczeniem satysfakcji i jest kompletna z PSPACE, a niedawno udowodniono, że jest kompletna z PSPACE ; dowód można znaleźć w:

Lauri Ahlroth i Pekka Orponen, Unordered Constraint Satisfaction Games . Wykład Notatki z informatyki Tom 7464, 2012, s. 64–75.

Abstrakcyjny:Rozważamy gry satysfakcji dla dwóch graczy na systemach ograniczeń boolowskich, w których gracze na zmianę wybierają jedną z dostępnych zmiennych i ustawiają ją na true lub false, w celu maksymalizacji (dla Gracza I) lub minimalizacji (dla Gracza) II) liczba spełnionych ograniczeń. W przeciwieństwie do standardowych gier z przypisywaniem zmiennych typu QBF, nie narzucamy kolejności, w której zmienne mają być odtwarzane. To sprawia, że ​​konfiguracja gry jest bardziej naturalna, ale także trudniejsza do kontrolowania. Zapewniamy strategie przybliżania czasu wielomianowego o stałym współczynniku dla Gracza I, gdy ograniczenia są funkcjami parzystości lub funkcjami progowymi z progiem, który jest niewielki w porównaniu z rodzajem ograniczeń. Udowadniamy również, że problem z określeniem, czy gracz I może spełnić wszystkie ograniczenia, jest PSPACE kompletny nawet w tym nieuporządkowanym ustawieniu,

Z treści:

$C = \{c_1,...,c_m\}$$X = \{x_1,...,x_n\}$$C$

$C$

... Twierdzenie 4 : Problem decydowania o zgodności GBF z formułą logiczną jest kompletny z PSPACE.

EDYCJA : Daniel Grier's odkrył, że wynik został również rozstrzygnięty przez Schaefera w latach 70., zobacz jego odpowiedź na tej stronie w celach informacyjnych (i głosuj :-). Schaefer udowodnił, że gra jest wciąż kompletna z PSPACE, nawet jeśli ogranicza się do dodatnich wzorów CNF (tj. Wzorów zdań w spójnej normalnej postaci, w której nie występują zmienne negowane) z maksymalnie 11 zmiennymi w każdej koniunkcji.

Warto również zauważyć, że problem ten rozwiązał również w latach 70. Thomas Schaefer w  Złożoność problemów decyzyjnych opartych na skończonych dwuosobowych grach z doskonałą informacją . W rzeczywistości okazuje się nieco silniejszym wynikiem, ponieważ język pozostaje kompletny z PSPACE, nawet jeśli ogranicza się do dodatnich formuł CNF.

Udowodniliśmy, że ta gra jest kompletna z PSPACE dla 5-CNF, ale ma algorytm czasu liniowego dla 2-CNF. Poprzedni najlepszy wynik to 6-CNF Ahlrotha i Orponena.

Dokument konferencyjny można znaleźć na ISAAC 2018 .

Aktualizacja: 16 listopada 2019 r

Udowodniliśmy, że gra może być obsługiwana dla 3-CNF z pewnymi ograniczeniami dla 3-CNF. Dowiedzieliśmy się także radykalnie, że ta gra jest również możliwa do przełożenia pod żadnym pozorem na 3-CNF. Pierwszą wersję można znaleźć na ECCC .