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 procedures have been proposed in the last few years, most of them based on the Davis, Logemann, Loveland procedure (DLL) for propositional satisfiability (SAT). In this paper we show how it is possible to extend the conflict-directed backjumping schema for SAT to QBF: when applicable, it allows to jump over existentially quantified literals while backtracking. We introduce solution-directed backjumping, which allows the same for universally quantified literals. Then, we show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based decision procedure for QBF satisfiability. We also implement and test the procedure: The experimental analysis shows that, because of backjumping, significant speed-ups can be obtained. While there have been several propos...

• Type: Conference
• Year: 2001
• Where: IJCAI
• Authors: Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella
• Keywords: Decision Procedure, IJCAI 2001, IJCAI 2007, Quantified Boolean Formulas, Solution-directed Backjumping