loading...
SAT Based BDD Solver for Quantified Boolean Formulas
Boca Raton, Florida November 15-November 17
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICTAI.2004.10616th IEEE International Conference on ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Gilles Audemard, Universit? d?Artois
Lakhdar Sa?, Universit? d?Artois
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
Usage of this product signifies your acceptance of the Terms of Use.