A Uniform Approach for Generating Proofs and Strategies for both True and False QBF Formulas
Alexandra Goultiaeva, Allen Van Gelder and Fahiem Bacchus
Many important problems can be compactly represented as quantified boolean formulas (QBF) and solved by general QBF solvers. This technique extends the `encoding to SAT' approach, which has been so successful in recent years, to many problems that do not have a compact SAT encoding. To date, QBF solvers have mainly focused on solving the decision problem; i.e., they determine whether or not the input QBF is true or false. In SAT, a range of useful applications have been made accessible by obtaining from the solver either a satisfying model or a proof of UNSAT. Such certificates often supply additional valuable information about the application. With QBF, however, the cases of true and false are more uniform, and either case might require a lengthy certificate. In this paper we show how the special features of a circuit-based QBF solver can be exploited to obtain proofs for both true and false QBF in a uniform way. Quantified boolean formulas also have a natural interpretation as a two-player game, and a winning strategy for one of the players is another important piece of information about the application. Strategies are somewhat analogous to a satisfying model in SAT. However, in QBF a strategy can be produced for both true and false formulas. In this paper we additionally show how such strategies can be easily computed from the proofs we have already generated.