Abstract
Quantified Boolean satisfiability (QSAT) is natural formulation of many decision problems and yet awaits further breakthroughs to reach the maturity enabling industrial applications. Recent advancements on quantified Boolean formula (QBF) proof systems sharpen our understanding of their proof complexities and shed light on solver improvement. Particularly QBF solving based on formula expansion has been theoretically and practically demonstrated to be more powerful than non-expansion based solving. However recursive expansion suffers from exponential formula explosion and has to be carefully managed. In this paper, we propose a QBF solver using levelized SAT solving in the flavor of formula expansion. New learning techniques based on circuit structure reconstruction, complete and incomplete ALLSAT learning, core expansion, bounded recursion, and other methods are devised to control formula growth. Experimental results on application benchmarks show that our prototype implementation is comparable with state-of-the-art solvers and outperforms other solvers in certain instances.
This work was supported in part by the Ministry of Science and Technology of Taiwan under grants MOST 103-2221-E-002-273 and 104-2628-E-002-013-MY3.
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.
Similar content being viewed by others
References
Benedetti, M.: Evaluating QBFs via symbolic skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 285–300. Springer, Heidelberg (2005)
Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 101–115. Springer, Heidelberg (2011)
Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-base QBF calculi. In: Proc. Symposium on Theoretical Aspects of Computer Science (STACS), pp. 76–89 (2015)
Balabanov, V., Jiang, J.-H.R.: Unified QBF Certification and its Applications. Formal Methods in System Design 41(1), 45–65 (2012)
Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154–169. Springer, Heidelberg (2014)
Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation. Journal of Automated Reasoning 28(2), 101–142 (2002)
Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 408–414. Springer, Heidelberg (2005)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Goultiaeva, A., Bacchus, F.: Recovering and utilizing partial duality in QBF. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 83–99. Springer, Heidelberg (2013)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability. Artificial Intelligence Research 26, 371–416 (2006)
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012)
Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating functions from large boolean relations. In: Proc. Int’l Conf. on Computer-Aided Design (ICCAD), pp. 779–784 (2009)
Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230–244. Springer, Heidelberg (2011)
Büning, H.K., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas. Information and Computation 117(1), 12–18 (1995)
Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128–142. Springer, Heidelberg (2010)
Lonsing, F., Biere, A.: DepQBF: A Dependency Aware QBF Solver (system description). Journal on Satisfiability, Boolean Modeling and Computation 7, 71–76 (2010)
Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Computation 2, 293–304 (1986)
QBF Gallery (2014). http://qbf.satisfiability.org/gallery/
Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: National Conference on Artificial Intelligence (AAAI), pp. 1045–1050 (2007)
The Quantified Boolean Formulas Satisfiability Library. http://www.qbflib.org/
Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005)
Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 466–483 (1970)
Yu, Y., Subramanyan, P., Tsiskaridze, N., Malik, S.: All-SAT using minimal blocking clauses. In: Proc. Int’l Conf. on VLSI Design, pp. 86–91 (2014)
Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: Proc. National Conference on Artificial Intelligence (AAAI), pp. 143–150 (2006)
Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proc. Int’l Conf. on Computer-Aided Design (ICCAD), pp. 442–449 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Tu, KH., Hsu, TC., Jiang, JH.R. (2015). QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-24318-4_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24317-7
Online ISBN: 978-3-319-24318-4
eBook Packages: Computer ScienceComputer Science (R0)