Abstract
Recent solvers for quantified boolean formulas (QBFs) use a clause learning method based on a procedure proposed by Giunchiglia et al. (JAIR 2006), which avoids creating tautological clauses. The underlying proof system is Q-resolution. This paper shows an exponential worst case for the clause-learning procedure. This finding confirms empirical observations that some formulas take mysteriously long times to solve, compared to other apparently similar formulas.
Q-resolution is known to be refutation complete for QBF, but not all logically implied clauses can be derived with it. A stronger proof system called QU-resolution is introduced, and shown to be complete in this stronger sense. A new procedure called QPUP for clause learning without tautologies is also described.
A generalization of pure literals is introduced, called effectively depth-monotonic literals. In general, the variable-elimination resolution operation, as used by Quantor, sQueezeBF, and Bloqqer is unsound if the existential variable being eliminated is not at innermost scope. It is shown that variable-elimination resolution is sound for effectively depth-monotonic literals even when they are not at innermost scope.
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
Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a new technique for establishing completeness. JACM 17 (1970)
Balabanov, V., Jiang, J.-H.R.: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 149–164. Springer, Heidelberg (2011)
Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Bubeck, U., Kleine Büning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244–257. Springer, Heidelberg (2007)
Bubeck, U.: Model-based Transformations for Quantified Boolean Formulas. PhD thesis, University of Paderborn (2010) (DISKI, 329, IOS Press; also at http://www.ub-net.de/bubeck-qbf-transformations-2010.pdf )
Cook, S., Reckhow, R.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44, 36–50 (1979)
Egly, U.: On Sequent Systems and Resolution for QBFs. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 100–113. Springer, Heidelberg (2012)
Goultiaeva, A., Bacchus, F.: Exploiting QBF duality on a circuit representation. In: AAAI (2010)
Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 412–426. Springer, Heidelberg (2009)
Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Proc. IJCAI (2011)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for Quantified Boolean Logic Satisfiability. In: AAAI/IAAI, pp. 649–654 (2002)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Monotone Literals and Learning in QBF Reasoning. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 260–273. Springer, Heidelberg (2004)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26 (2006)
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified boolean formulas. Information and Computation 117, 12–18 (1995)
Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press (1999)
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.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. PhD thesis, Johannes Kepler University (2012)
Lonsing, F., Biere, A.: A Compact Representation for Syntactic Dependencies in QBFs. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 398–411. Springer, Heidelberg (2009)
Lonsing, F., Biere, A.: Integrating Dependency Schemes in Search-Based QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158–171. Springer, Heidelberg (2010)
Lonsing, F., Biere, A.: Failed Literal Detection for QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 259–272. Springer, Heidelberg (2011)
Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002)
Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFs: A comparison of state-of-the-art tools. AI Commun. 22(4), 191–210 (2009)
Van Gelder, A.: Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 141–146. Springer, Heidelberg (2009)
Van Gelder, A.: Generalized Conflict-Clause Strengthening for Satisfiability Solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 329–342. Springer, Heidelberg (2011)
Van Gelder, A.: Variable Independence and Resolution Paths for Quantified Boolean Formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789–803. Springer, Heidelberg (2011)
Van Gelder, A.: Producing and verifying extremely large propositional refutations: Have your cake and eat it too. AMAI (2012) (accepted subject to revisions)
Van Gelder, A., Wood, S.B., Lonsing, F.: Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 86–99. Springer, Heidelberg (2012)
Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proc. ICCAD, pp. 442–449 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Van Gelder, A. (2012). Contributions to the Theory of Practical Quantified Boolean Formula Solving. In: Milano, M. (eds) Principles and Practice of Constraint Programming. CP 2012. Lecture Notes in Computer Science, vol 7514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33558-7_47
Download citation
DOI: https://doi.org/10.1007/978-3-642-33558-7_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33557-0
Online ISBN: 978-3-642-33558-7
eBook Packages: Computer ScienceComputer Science (R0)