Backjumping for Quantified Boolean Logic Satisfiability

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision proce- dures have been proposed in the last few years, most of them based on the Davis, Logemann, Love- land procedure (DLL) for propositional satisfiabil- ity (SAT). In this paper we show how it is pos- sible to extend the conflict-directed backjumping schema for SAT to QBF: when applicable, it al- lows to jump over existentially quantified literals while backtracking. We introduce solution-directed backjumping, which allows the same for univer- sally quantified literals. Then, we show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based de- cision procedure for QBF satisfiability. We also im- plement and test the procedure: The experimental analysis shows that, because of backjumping, sig- nificant speed-ups can be obtained. While there have been several proposals for backjumping in SAT, this is the first time –as far as we know– this idea has been proposed, implemented and experi- mented for QBFs.