Decydowanie, czy skwantyfikowana formuła boolowska, taka jak
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ć 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 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 na wartość true, a następnie w następnym ruchu gracz drugi może zdecyduj, aby ustawić 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 .
Problem otrzymuje formułę boolowską na 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?
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 .
źródło