QBFソルバを書いている。 SATはいわば論理式 ∃X1 ∃X2 … ∃Xn. Φ の真偽を判定するという問題だが、 量化子に∃だけでなく∀も含まれる場合の真偽の判定がQBF。 SATとあまり変わらないように思えるかもしれないけれど、SATが高々NP完全でしかないのに対して、QBFはPSPACE完全とだいぶ難しい。
とりあえず実装したものは、 Solving QBF with Counterexample Guided Refinement のアルゴリズムの非常に素朴な実装。
http://sat.inesc-id.pt/~mikolas/sat12_talk.pdf
https://www.cs.cmu.edu/~wklieber/papers/qbf-cegar-sat-2012.pdf
うまいアイディアが思いつけば QBFEVAL'16 http://www.qbflib.org/qbfeval16.php に投稿してみたい。
https://github.com/msakai/toysolver/commit/aad483811243fe80a106bbb9ed2c2ee8ddb5d6ff