TY - GEN
T1 - Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation
AU - Zhang, Lintao
AU - Malik, Sharad
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002
Y1 - 2002
N2 - In this paper, we describe a new framework for evaluating Quantified Boolean Formulas (QBF). The new framework is based on the Davis-Putnam (DPLL) search algorithm. In existing DPLL based QBF algorithms, the problem database is represented in Conjunctive Normal Form (CNF) as a set of clauses, implications are generated from these clauses, and backtracking in the search tree is chronological.In this work, we augment the basic DPLL algorithm with conflict driven learning as well as satisfiability directed implication and learning. In addition to the traditional clause database, we add a cube database to the data structure. We show that cubes can be used to generate satisfiability directed implications similar to conflict directed implications generated by the clauses. We show that in a QBF setting,conflicting leaves and satisfying leaves of the search tree both provide valuable information to the solver in a symmetric way. We have implemented our algorithm in the new QBF solver Quaffle.Experimental results show that for some test cases, satisfiability directed implication and learning significantly prunes the search.
AB - In this paper, we describe a new framework for evaluating Quantified Boolean Formulas (QBF). The new framework is based on the Davis-Putnam (DPLL) search algorithm. In existing DPLL based QBF algorithms, the problem database is represented in Conjunctive Normal Form (CNF) as a set of clauses, implications are generated from these clauses, and backtracking in the search tree is chronological.In this work, we augment the basic DPLL algorithm with conflict driven learning as well as satisfiability directed implication and learning. In addition to the traditional clause database, we add a cube database to the data structure. We show that cubes can be used to generate satisfiability directed implications similar to conflict directed implications generated by the clauses. We show that in a QBF setting,conflicting leaves and satisfying leaves of the search tree both provide valuable information to the solver in a symmetric way. We have implemented our algorithm in the new QBF solver Quaffle.Experimental results show that for some test cases, satisfiability directed implication and learning significantly prunes the search.
UR - http://www.scopus.com/inward/record.url?scp=84957000280&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84957000280&partnerID=8YFLogxK
U2 - 10.1007/3-540-46135-3_14
DO - 10.1007/3-540-46135-3_14
M3 - Conference contribution
AN - SCOPUS:84957000280
SN - 3540441204
SN - 9783540441205
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 200
EP - 215
BT - Principles and Practice of Constraint Programming- CP 2002 - 8th International Conference, CP 2002, Proceedings
A2 - Van Hentenryck, Pascal
PB - Springer Verlag
T2 - 8th International Conference on Principles and Practice of Constraint Programming, CP 2002
Y2 - 9 September 2002 through 13 September 2002
ER -