Ist diese Variante von TQBF noch PSPACE-vollständig?

Entscheiden, ob eine quantifizierte Boolesche Formel wie

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

Immer wahr zu bewerten ist ein klassisches PSPACE-vollständiges Problem. Dies kann als ein Spiel zwischen zwei Spielern mit abwechselnden Zügen angesehen werden. Der erste Spieler bestimmt den Wahrheitswert der ungeradzahligen Variablen und der zweite Spieler den Wahrheitswert der geradzahligen Variablen. Der erste Spieler versucht, $\varphi$ falsch zu machen und der zweite Spieler versucht, es wahr zu machen. Die Entscheidung, wer eine Gewinnstrategie hat, ist PSPACE-vollständig.

Ich denke an ein ähnliches Problem mit zwei Spielern, von denen einer versucht, eine Boolesche Formel $\varphi$ wahr zu machen, und der andere versucht, sie falsch zu machen. Der Unterschied besteht darin, dass ein Spieler in einem Zug eine Variable und einen Wahrheitswert dafür auswählen kann (zum Beispiel, wenn er als allererster Zug entscheidet, $x_8$ auf wahr zu setzen , und im nächsten Zug kann er zwei wählen entscheide dich, $x_3$ auf false zu setzen). Dies bedeutet, dass die Spieler entscheiden können, welche der Variablen (von denen, denen noch kein Wahrheitswert zugewiesen wurde) sie einen Wahrheitswert zuweisen möchten, anstatt das Spiel in der Reihenfolge $x_1 , \ldots , x_n$ .

Das Problem erhält eine boolesche Formel $\varphi$ für $n$ Variablen, um zu entscheiden, ob Spieler eins (versucht, es falsch zu machen) oder Spieler zwei (versucht, es wahr zu machen) eine Gewinnstrategie hat. Dieses Problem ist eindeutig immer noch in PSPACE, da der Spielbaum eine lineare Tiefe hat.

Bleibt es PSPACE vollständig?

Es handelt sich um ein ungeordnetes Constraint Satisfaction-Spiel , das PSPACE-vollständig ist und sich erst kürzlich als PSPACE-vollständig erwiesen hat . Ein Beweis ist zu finden in:

Lauri Ahlroth und Pekka Orponen, Unordered Constraint Satisfaction Games . Lecture Notes in Computer Science Volume 7464, 2012, S. 64-75.

Abstrakt:Wir betrachten Zwei-Spieler-Constraint-Zufriedenheitsspiele auf Systemen mit Booleschen Constraints, bei denen die Spieler abwechselnd eine der verfügbaren Variablen auswählen und auf wahr oder falsch setzen, mit dem Ziel, sie zu maximieren (für Spieler I) oder zu minimieren (für Spieler I) II) die Anzahl der erfüllten Bedingungen. Im Gegensatz zu normalen QBF-Variablenzuweisungsspielen legen wir keine Reihenfolge fest, in der die Variablen gespielt werden sollen. Dies macht das Setup des Spiels natürlicher, aber auch schwieriger zu steuern. Für Player I stellen wir Näherungsstrategien mit Polynomzeit und konstantem Faktor bereit, wenn es sich bei den Einschränkungen um Paritätsfunktionen oder Schwellenwertfunktionen handelt, deren Schwellenwert im Vergleich zur Anzahl der Einschränkungen klein ist. Außerdem beweisen wir, dass das Problem, zu bestimmen, ob Player I alle Einschränkungen erfüllen kann, auch in dieser ungeordneten Umgebung PSPACE-vollständig ist.

Aus dem Inhalt:

...
Unser generisches Beispiel für ein ungeordnetes Constraint-Zufriedenheitsspiel ist das Game on Boolean Formulas ( GBF ). Eine Instanz dieses Spiels wird durch einen Satz von m nicht konstanter Boolesche Formeln über einen gemeinsamen Satz von n Variablen X = { x 1 , . . . , x n } . Wir bezeichnen die Formeln in C als Klauseln, obwohl wir im Allgemeinen nicht verlangen, dass sie Disjunktionen sind. ...$C = \{c_1,...,c_m\}$$X = \{x_1,...,x_n\}$$C$

Ein Spiel auf fortgesetzt, so dass der Spieler bei jedem Zug eine der zuvor nicht ausgewählten Variablen auswählt und dieser einen Wahrheitswert zuweist. Spieler I beginnt und das Spiel endet, wenn allen Variablen ein Wert zugewiesen wurde. In der Entscheidungsversion von GBF ist die Frage, ob Spieler I eine umfassende Gewinnstrategie hat, mit der sie alle Klauseln erfüllen kann, unabhängig davon, was Spieler II tut. Im positiven Fall sagen wir, dass die Instanz GBF-fähig ist. ..$C$

... Satz 4 : Das Problem bei der Entscheidung über die GBF-Erfüllbarkeit einer Booleschen Formel ist PSPACE-vollständig.

EDIT : Daniel Grier's hat herausgefunden, dass das Ergebnis auch von Schaefer in den 70ern festgelegt wurde. Siehe seine Antwort auf dieser Seite als Referenz (und stimme dem zu :-). Schaefer hat bewiesen, dass das Spiel PSPACE-vollständig ist, auch wenn es auf positive CNF-Formeln (dh Aussagenformeln in konjunktiver Normalform, in denen keine negierten Variablen vorkommen) mit höchstens 11 Variablen in jeder Konjunktion beschränkt ist.

Es kann auch erwähnenswert sein, dass dieses Problem auch in den 70er Jahren von Thomas Schäfer in  Komplexität von Entscheidungsproblemen auf der Grundlage endlicher Zwei-Personen-Vollkommen-Informationsspiele gelöst wurde . Tatsächlich zeigt er ein etwas stärkeres Ergebnis, dass die Sprache auch dann PSPACE-vollständig bleibt, wenn sie auf positive CNF-Formeln beschränkt ist.

Wir haben bewiesen, dass dieses Spiel für 5-CNFs PSPACE-vollständig ist, aber einen linearen Zeitalgorithmus für 2-CNFs hat. Das bisher beste Ergebnis waren die 6-CNFs von Ahlroth und Orponen.

Das Konferenzpapier finden Sie auf der ISAAC 2018 .

Update: 16. November 2019

Wir haben bewiesen, dass das Spiel für 3-CNFs unter gewissen Einschränkungen für 3-CNFs anwendbar ist. Wir haben auch radikal vermutet, dass dieses Spiel auch ohne Einschränkungen für 3-CNFs handhabbar ist. Die erste Version finden Sie bei ECCC .