QBF Solving Using Best First Search

Quantified Boolean Formula or QBF is similar to a two-player strategy game on a theoretical level. While most search-based QBF solvers are based on a depth-first search based QDPLL procedure, many game solvers use best-first search algorithms such as proof number search. In this paper, we examine how to design a best-first search based QBF solver that combines some well-known QBF solving techniques such as backjumping and clause learning. We evaluate the performance of the resulting algorithm on a set of standard QBF benchmarks.