Apakah variasi TQBF ini masih lengkap dengan PSPACE?

Memutuskan apakah formula boolean yang dikuantifikasi seperti

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

selalu mengevaluasi benar adalah masalah PSPACE-lengkap klasik. Ini dapat dilihat sebagai permainan antara dua pemain, dengan gerakan bergantian. Pemain pertama menentukan nilai kebenaran dari variabel bernomor ganjil dan pemain kedua memutuskan nilai kebenaran dari variabel genap. Pemain pertama mencoba untuk membuat $\varphi$ salah dan pemain kedua mencoba untuk menjadikannya benar. Memutuskan siapa yang memiliki strategi kemenangan adalah PSPACE-complete.

Saya sedang mempertimbangkan masalah yang sama dengan dua pemain, satu berusaha membuat formula boolean $\varphi$ benar dan yang lain mencoba membuatnya salah. Perbedaannya adalah bahwa pada saat bergerak, pemain dapat memilih variabel dan nilai kebenaran untuknya (misalnya, sebagai langkah pertama, pemain dapat memutuskan untuk mengatur $x_8$ ke true dan kemudian pada langkah berikutnya, pemain dua mungkin putuskan untuk mengatur $x_3$ ke false). Ini berarti bahwa para pemain dapat memutuskan variabel mana (dari variabel yang belum diberi nilai kebenaran) yang ingin mereka berikan nilai kebenaran, alih-alih harus memainkan permainan dalam urutan $x_1 , \ldots , x_n$ .

Masalahnya diberikan rumus boolean $\varphi$ pada $n$ variabel untuk memutuskan apakah pemain satu (mencoba membuatnya salah) atau pemain dua (berusaha membuatnya benar) memiliki strategi kemenangan. Masalah ini jelas masih di PSPACE, karena pohon permainan memiliki kedalaman linier.

Apakah PSPACE tetap lengkap?

Ini adalah sebuah permainan Satisfaction Constraint Constraint dan merupakan PSPACE-complete dan telah terbukti sebagai PSPACE-complete baru-baru ini ; sebuah bukti dapat ditemukan di:

Lauri Ahlroth dan Pekka Orponen, Game Satisfaction Constraint Constraint . Catatan Kuliah di Ilmu Komputer Volume 7464, 2012, hal 64-75.

Abstrak:Kami mempertimbangkan permainan kepuasan kendala dua pemain pada sistem kendala Boolean, di mana para pemain bergiliran dalam memilih salah satu variabel yang tersedia dan mengaturnya menjadi benar atau salah, dengan tujuan memaksimalkan (untuk Pemain I) atau meminimalkan (untuk Pemain) II) jumlah kendala puas. Tidak seperti dalam game tugas variabel tipe-QBF standar, kami tidak menentukan urutan variabel mana yang akan dimainkan. Ini membuat pengaturan game lebih alami, tetapi juga lebih menantang untuk dikendalikan. Kami menyediakan waktu polinomial, strategi pendekatan faktor konstan untuk Pemain I ketika kendala adalah fungsi paritas atau fungsi ambang batas dengan ambang batas yang kecil dibandingkan dengan arity kendala. Juga, kami membuktikan bahwa masalah menentukan apakah Pemain I dapat memenuhi semua kendala adalah PSPACE-lengkap bahkan dalam pengaturan yang tidak berurutan ini,

Dari konten:

$C = \{c_1,...,c_m\}$ lebih dari satu set variabel n umum $X = \{x_1,...,x_n\}$. Kami merujuk ke rumus di$C$sebagai klausa meskipun secara umum kita tidak mensyaratkannya sebagai disjungsi.
...
Game menyala$C$melanjutkan sehingga pada setiap belokan pemain untuk bergerak memilih salah satu dari variabel yang sebelumnya tidak dipilih dan memberikan nilai kebenaran padanya. Pemain I mulai, dan permainan berakhir ketika semua variabel telah diberi nilai. Dalam versi keputusan GBF , pertanyaannya adalah apakah Player I memiliki strategi kemenangan yang komprehensif, yang dengannya dia dapat membuat semua klausa puas tidak peduli apa yang dilakukan Player II. Dalam kasus positif, kami mengatakan bahwa instance tersebut memenuhi GBF...

... Teorema 4 : Masalah dalam menentukan GBF-satisfiability dari formula Boolean adalah PSPACE-complete.

EDIT : Daniel Grier's telah menemukan bahwa hasilnya juga diselesaikan oleh Schaefer di tahun 70-an, lihat jawabannya di halaman ini untuk referensi (dan upvote :-). Schaefer membuktikan bahwa permainan ini masih PSPACE-complete bahkan jika terbatas pada rumus CNF positif (yaitu rumus proposisional dalam bentuk normal konjungtif di mana tidak ada variabel yang dinegasikan terjadi) dengan paling banyak 11 variabel di setiap konjungsi.

Mungkin juga bermanfaat untuk dicatat bahwa masalah ini juga diselesaikan pada tahun 70-an oleh Thomas Schaefer dalam  Kompleksitas masalah keputusan berdasarkan pada permainan informasi sempurna dua orang yang terbatas . Bahkan, ia membuktikan hasil yang sedikit lebih kuat karena bahasanya tetap lengkap PSPACE bahkan ketika terbatas pada formula CNF positif.

Kami membuktikan bahwa game ini adalah PSPACE-complete untuk 5-CNFs tetapi memiliki algoritma Linear Time untuk 2-CNFs. Hasil terbaik sebelumnya adalah Ahlroth dan Orponen 6-CNF.

Anda dapat menemukan makalah konferensi di ISAAC 2018 .

Pembaruan: 16 Nov 2019

Kami membuktikan bahwa gim ini dapat ditelusuri untuk 3-CNF di bawah beberapa batasan pada 3-CNF. Kami juga secara radikal menduga bahwa game ini juga dapat ditelusuri tanpa batasan pada 3-CNF. Anda dapat menemukan versi awal di ECCC .