16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04)
SAT Based BDD Solver for Quantified Boolean Formulas
Boca Raton, Florida
November 15-November 17
ISBN: 0-7695-2236-X
Solving Quantified Boolean Formulas (QBF) has become an attractive research area in Artificial intelligence. Many important artificial intelligence problems (planning, non monotonic reasoning, formal verification, etc.) can be reduced to QBFs. In this paper, a new DLL-based method is proposed that integrates binary decision diagram (BDD) to set free the variable ordering heuristics that are traditionally constrained by the static order of the QBF quantifiers. BDD is used to represent in a compact form the set of models of the boolean formula. Interesting reduction operators are proposed in order to dynamically reduce the BDD size and to answer the validity of the QBF. Experimental results on instances from the QBF?03 evaluation show that our approach can efficiently solve instances that are very hard for current QBF solvers.
Index Terms:
Quantified boolean formula, Binary decision diagram, Satisfiability
Citation:
Gilles Audemard, Lakhdar Sa?, "SAT Based BDD Solver for Quantified Boolean Formulas," ictai, pp.82-89, 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04), 2004