Abstract
In this paper we present a new technique to solve Quantified Boolean Formulas (QBF). Our technique applies the idea of dynamic partitioning to QBF solvers. Dynamic partitioning has previously been utilized in #SAT solvers that count the number of models of a propositional formula. One of the main differences with the #SAT case comes from the solution learning techniques employed in search based QBF solvers. Extending solution learning to a partitioning solver involves some considerable complexities which we show how to resolve. We have implemented our ideas in a new QBF solver, and demonstrate that dynamic partitioning is able to increase the performance of search based solvers, sometimes significantly. Empirically our new solver offers performance that is superior to other search based solvers and in many cases superior to non-search based solvers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bryant, R., Lahiri, S., Seshia, S.: Convergence testing in term-level bounded model checking. Technical Report CMU-CS-03-156, Carnegie Mellon University (2003)
Egly, U., et al.: Solving advanced reasoning tasks using quantified boolean formulas. In: AAAI/IAAI, pp. 417–422 (2000)
Rintanen, J.: Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)
Ali, M., et al.: Post-verification debugging of hierarchical designs. In: International Conf. on Computer Aided Design (ICCAD), pp. 871–876 (2005)
Bayardo Jr., R.J., Pehoushek, J.D.: Counting models using connected components. In: Proceedings of the AAAI National Conference (AAAI), pp. 157–162 (2000)
Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. Journal of Applied Non-Classical Logics 11(1-2), 11–34 (2001)
Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and Complexity Results for #SAT and Bayesian Inference. In: 44th Symposium on Foundations of Computer Science (FOCS), pp. 340–351 (2003)
Samulowitz, H., Bacchus, F.: QBF Solver 2clsQ (2006), available at http://www.cs.toronto.edu/~fbacchus/sat.html
Biere, A.: Resolve and Expand. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Benedetti, M.: sKizzo: a QBF decision procedure based on propositional skolemization and symbolic reasoning. Technical Report TR04-11-03 (2004)
Bacchus, F., Samulowitz, H., Davies, J.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 514–529. Springer, Heidelberg (2006)
Büning, H.K., Karpinski, M., Flügel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12–18 (1995)
Zhang, L., Malik, S.: Towards symmetric treatment of conflicts and satisfaction in quantified boolean satisfiability solver. In: Principles and Practice of Constraint Programming (CP2002), pp. 185–199 (2002)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: Eighteenth national conference on Artificial intelligence, pp. 649–654 (2002)
Benedetti, M.: Quantifier Trees for QBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 378–385. Springer, Heidelberg (2005)
Sang, T., et al.: Combining component caching and clause learning for effective model counting. In: SAT (2004)
Bacchus, F., Samulowitz, H.: Binary Clause Reasoning in QBF. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 353–367. Springer, Heidelberg (2006)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), http://www.qbflib.org
Giunchiglia, E., Tacchella, A., Narizzano, M.: QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, Springer, Heidelberg (2001)
Bacchus, F., Samulowitz, H.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005)
Giunchiglia, E., Narizzano, M., Tacchella, A.: The qbf2006 competition (2006) (2006), available on line at http://www.qbflib.org/
Samulowitz, H., Davies, J., Bacchus, F.: QBF Preprocessor Prequel (2006), available at http://www.cs.toronto.edu/~fbacchus/sat.html
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Samulowitz, H., Bacchus, F. (2007). Dynamically Partitioning for Solving QBF. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)