On Q-resolution and CDCL QBF solving. (English) Zbl 1475.68440

Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 402-418 (2016).
Summary: The proof system Q-resolution and its variations provide the underlying proof systems for the DPLL-based QBF solvers. While (long-distance) Q-resolution models a conflict driven clause learning (CDCL) QBF solver, the inverse relation is not well understood. This paper shows that CDCL solving not only does not simulate Q-resolution, but also that this is deeply embedded in the workings of the solver. This contrasts with SAT solving, where CDCL solvers have been shown to simulate resolution.
For the entire collection see [Zbl 1337.68009].


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)


Quaffle ; DepQBF
Full Text: DOI


[1] Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory Comput. 3(5), 81–102 (2007) · Zbl 1213.68303
[2] Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. (JAIR) 40, 353–373 (2011) · Zbl 1214.68340
[3] Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012) · Zbl 1284.68516
[4] Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319–351 (2004) · Zbl 1080.68651
[5] Beame, P., Sabharwal, A.: Non-restarting SAT solvers with simple preprocessing can efficiently simulate resolution. In: Brodley, C.E., Stone, P. (eds.) Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 2608–2615. AAAI Press (2014)
[6] Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) · Zbl 1183.68568
[7] Bonet, M.L., Esteban, J.L., Galesi, N., Johannsen, J.: Exponential separations between restricted resolution and cutting planes proof systems. In: 39th Annual Symposium on Foundations of Computer Science, FOCS, pp. 638–647. IEEE Computer Society (1998)
[8] Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. J. Autom. Reasoning 28(2), 101–142 (2002) · Zbl 1002.68165
[9] Chen, H.: Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP) (2016) · Zbl 1387.03067
[10] Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fund. Math. 49, 129–141, 13 (1961) · Zbl 0096.24303
[11] Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified Boolean formulas. J. Artif. Intell. Res. 26(1), 371–416 (2006) · Zbl 1183.68475
[12] Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere et al. [6], pp. 761–780
[13] Goerdt, A.: Davis-Putnam resolution versus unrestricted resolution. Ann. Math. Artif. Intell. 6(1–3), 169–184 (1992) · Zbl 0865.03010
[14] Goultiaeva, A., Seidl, M., Biere, A.: Bridging the gap between dual propagation and CNF-based QBF solving. In: DATE, pp. 811–814 (2013)
[15] Haken, A.: The intractability of resolution. Theoret. Comput. Sci. 39, 297–308 (1985) · Zbl 0586.03010
[16] Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theoret. Comput. Sci. 577, 25–42 (2015) · Zbl 1309.68168
[17] Kleine Büning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Biere et al. [6], pp. 735–760 · Zbl 1331.68199
[18] Büning Kleine, K., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995) · Zbl 0828.68045
[19] Klieber, W.: Formal Verification Using Quantified Boolean Formulas (QBF). Ph.D. thesis, Carnegie Mellon University (2014). http://www.cs.cmu.edu/ wklieber/thesis.pdf
[20] 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
[21] Kolaitis, P.G.: The expressive power of stratified programs. Inf. Comput. 90(1), 50–66 (1991) · Zbl 0727.68016
[22] Lonsing, F.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.D. thesis, Johannes Kepler Universität (2012). http://www.kr.tuwien.ac.at/staff/lonsing/diss/
[23] Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. JSAT 7(2–3), 71–76 (2010)
[24] Lonsing, F., Egly, U., Van Gelder, A.: Efficient clause learning for quantified boolean formulas via QBF pseudo unit propagation. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 100–115. Springer, Heidelberg (2013) · Zbl 1390.68579
[25] Mahajan, M., Shukla, A.: Level-ordered Q-resolution and tree-like Q-resolution are incomparable. Inf. Process. Lett. 116(3), 256–258 (2016) · Zbl 1348.03056
[26] Marques Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999) · Zbl 01935259
[27] Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011) · Zbl 1216.68235
[28] Van Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 647–663. Springer, Heidelberg (2012) · Zbl 1390.68585
[29] Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: AAAI. AAAI Press (2006)
[30] Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD, pp. 442–449 (2002)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.