Paper Info
Title
Backjumping for quantified Boolean logic satisfiability
Abstract
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 the satisfiability of QBFs: When applicable, conflict-directed backjumping allows search to skip over existentially quantified literals while backtracking. We introduce solution-directed backjumping, which allows the same behavior for universally quantified literals. We show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based decision procedure for satisfiability of QBFs. We also implement and test the procedure: The experimental analysis shows that, because of backjumping, significant speed-ups can be obtained.Summing up: We present the first algorithm that applies conflict and solution directed backjumping to QBF, and demonstrate the performance of this algorithm via an empirical study.
Year
DOI
Venue
2001
10.1016/S0004-3702(02)00373-9
Artificial Intelligence
Keywords
DocType
Volume
solution-directed backjumping,boolean logic satisfiability,decision procedure,dll-based decision procedure,qbf satisfiability,artificial intelligence,quantified boolean formulas,conflict-directed backjumping schema,loveland procedure,effective reasoning tool,propositional satisfiability,conflict-directed backjumping,satisfiability,artificial intelligent,experimental analysis
Conference
145
Issue
ISSN
ISBN
1-2
0004-3702
1-55860-812-5
Citations 
PageRank 
References 
49
2.77
21
Authors
3
Name
Order
Citations
PageRank
Enrico Giunchiglia12380164.28
Massimo Narizzano245130.41
Armando Tacchella31448108.82