QELL: QBF reasoning with extended clause learning and levelized SAT solving. (English) Zbl 1471.68263
Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 343-359 (2015).
Summary: 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-theart solvers and outperforms other solvers in certain instances.
For the entire collection see [Zbl 1323.68009].
For the entire collection see [Zbl 1323.68009].
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 68T05 | Learning and adaptive systems in artificial intelligence |
References:
| [1] | 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) · Zbl 1108.68569 · doi:10.1007/978-3-540-32275-7_20 |
| [2] | 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) · Zbl 1341.68181 · doi:10.1007/978-3-642-22438-6_10 |
| [3] | 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) · Zbl 1355.68105 |
| [4] | Balabanov, V., Jiang, J.-H.R.: Unified QBF Certification and its Applications. Formal Methods in System Design 41(1), 45–65 (2012) · Zbl 1284.68516 · doi:10.1007/s10703-012-0152-6 |
| [5] | 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) · Zbl 1423.68406 · doi:10.1007/978-3-319-09284-3_12 |
| [6] | 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) · Zbl 1002.68165 · doi:10.1023/A:1015019416843 |
| [7] | 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) · Zbl 1128.68366 · doi:10.1007/11499107_32 |
| [8] | 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) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37 |
| [9] | 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) · Zbl 1390.68573 · doi:10.1007/978-3-642-39071-5_8 |
| [10] | Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability. Artificial Intelligence Research 26, 371–416 (2006) · Zbl 1183.68475 |
| [11] | 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) · Zbl 1273.68178 · doi:10.1007/978-3-642-31612-8_10 |
| [12] | 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) · doi:10.1145/1687399.1687544 |
| [13] | 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) · Zbl 1330.68115 · doi:10.1007/978-3-642-21581-0_19 |
| [14] | Büning, H.K., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas. Information and Computation 117(1), 12–18 (1995) · Zbl 0828.68045 · doi:10.1006/inco.1995.1025 |
| [15] | 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) · Zbl 1306.68161 · doi:10.1007/978-3-642-14186-7_12 |
| [16] | Lonsing, F., Biere, A.: DepQBF: A Dependency Aware QBF Solver (system description). Journal on Satisfiability, Boolean Modeling and Computation 7, 71–76 (2010) |
| [17] | Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Computation 2, 293–304 (1986) · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1 |
| [18] | QBF Gallery (2014). http://qbf.satisfiability.org/gallery/ |
| [19] | Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: National Conference on Artificial Intelligence (AAAI), pp. 1045–1050 (2007) |
| [20] | The Quantified Boolean Formulas Satisfiability Library. http://www.qbflib.org/ |
| [21] | Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005) · Zbl 1153.68485 · doi:10.1007/11564751_43 |
| [22] | Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 466–483 (1970) · doi:10.1007/978-1-4899-5327-8_25 |
| [23] | 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) · doi:10.1109/VLSID.2014.22 |
| [24] | Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: Proc. National Conference on Artificial Intelligence (AAAI), pp. 143–150 (2006) |
| [25] | 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) · doi:10.1145/774572.774637 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
