Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

New Resolution-Based QBF Calculi and Their Proof Complexity

New Resolution-Based QBF Calculi and Their Proof Complexity Modern QBF solvers typically use two different paradigms, conflict-driven clause learning (CDCL) solving or expansion solving. Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of these solvers, with Q-Resolution and its extensions relating to CDCL solving and Exp+Res relating to expansion solving. This article defines two novel calculi, which are resolution-based and enable unification of some of the principal existing resolution-based QBF calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based calculus Exp+Res. However, the proof complexity of the QBF resolution proof systems is currently not well understood. In this article, we completely determine the relative power of the main QBF resolution systems, settling in particular the relationship between the two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, universal, and long-distance Q-resolution) and proof systems for expansion-based solvers (Exp+Res and its generalizations IR-calc and IRM-calc defined here). The most challenging part of this comparison is to exhibit hard formulas that underlie the exponential separations of the aforementioned proof systems. To this end, we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths-of-proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems such as long-distance Q-resolution and extensions. With a completely different and novel counting argument, we show the hardness of the prominent formulas of Kleine Bning et al. [51] for the strong expansion-based calculus IR-calc. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png ACM Transactions on Computation Theory (TOCT) Association for Computing Machinery

New Resolution-Based QBF Calculi and Their Proof Complexity

Download PDF
42 pages

Loading next page...
 
/lp/association-for-computing-machinery/new-resolution-based-qbf-calculi-and-their-proof-complexity-52OtiRx7b0
Publisher
Association for Computing Machinery
Copyright
Copyright © 2019 ACM
ISSN
1942-3454
eISSN
1942-3462
DOI
10.1145/3352155
Publisher site
See Article on Publisher Site

Abstract

Modern QBF solvers typically use two different paradigms, conflict-driven clause learning (CDCL) solving or expansion solving. Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of these solvers, with Q-Resolution and its extensions relating to CDCL solving and Exp+Res relating to expansion solving. This article defines two novel calculi, which are resolution-based and enable unification of some of the principal existing resolution-based QBF calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based calculus Exp+Res. However, the proof complexity of the QBF resolution proof systems is currently not well understood. In this article, we completely determine the relative power of the main QBF resolution systems, settling in particular the relationship between the two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, universal, and long-distance Q-resolution) and proof systems for expansion-based solvers (Exp+Res and its generalizations IR-calc and IRM-calc defined here). The most challenging part of this comparison is to exhibit hard formulas that underlie the exponential separations of the aforementioned proof systems. To this end, we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths-of-proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems such as long-distance Q-resolution and extensions. With a completely different and novel counting argument, we show the hardness of the prominent formulas of Kleine Bning et al. [51] for the strong expansion-based calculus IR-calc.

Journal

ACM Transactions on Computation Theory (TOCT) – Association for Computing Machinery

Published: Sep 12, 2019

Keywords: Proof complexity

References

  • Computational Complexity -- A Modern Approach
    Arora, Sanjeev; Barak, Boaz
  • Bounded-width QBF is PSPACE-complete
    Atserias, Albert; Oliva, Sergi
  • Unified QBF certification and its applications
    Balabanov, Valeriy; Jiang, Jie-Hong R.
  • Efficient extraction of QBF (Counter)models from long-distance resolution proofs
    Balabanov, Valeriy; Jiang, Jie-Hong Roland; Janota, Mikoláš; Widl, Magdalena
  • QBF Resolution systems and their proof complexities
    Balabanov, Valeriy; Widl, Magdalena; Jiang, Jie-Hong R.
  • Short proofs are narrow - resolution made simple
    Ben-Sasson, Eli; Wigderson, Avi
  • Evaluating QBFs via symbolic Skolemization
    Benedetti, Marco
  • QBF-based formal verification: Experience and perspectives
    Benedetti, Marco; Mangassarian, Hratch
  • Dependency schemes in QBF calculi: Semantics and soundness
    Beyersdorff, Olaf; Blinkhorn, Joshua
  • Lower bounds: From circuits to QBF proof systems
    Beyersdorff, Olaf; Bonacina, Ilario; Chew, Leroy
  • On unification of QBF resolution-based calculi
    Beyersdorff, Olaf; Chew, Leroy; Janota, Mikoláš
  • Proof complexity of resolution-based QBF calculi
    Beyersdorff, Olaf; Chew, Leroy; Janota, Mikoláš
  • Extension variables in QBF resolution
    Beyersdorff, Olaf; Chew, Leroy; Janota, Mikoláš
  • Feasible interpolation for QBF resolution calculi
    Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil
  • Are short proofs narrow? QBF resolution is not so simple
    Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil
  • Lifting QBF resolution calculi to DQBF
    Beyersdorff, Olaf; Chew, Leroy; Schmidt, Renate A.; Suda, Martin
  • A game characterisation of tree-like Q-Resolution size
    Beyersdorff, Olaf; Chew, Leroy; Sreenivasaiah, Karteek
  • A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
    Beyersdorff, Olaf; Galesi, Nicola; Lauria, Massimo
  • A characterization of tree-like resolution size
    Beyersdorff, Olaf; Galesi, Nicola; Lauria, Massimo
  • Parameterized complexity of DPLL search procedures
    Beyersdorff, Olaf; Galesi, Nicola; Lauria, Massimo
  • Understanding Gentzen and Frege systems for QBF
    Beyersdorff, Olaf; Pich, Ján
  • Resolve and expand
    Biere, Armin
  • Handbook of Satisfiability
    Biere, Armin; Heule, Marijn; van Maaren, Hans; (Eds, Toby Walsh
  • Blocked clause elimination for QBF
    Biere, Armin; Lonsing, Florian; Seidl, Martina
  • On the relative complexity of resolution refinements and cutting planes proof systems
    Bonet, Maria Luisa; Esteban, Juan Luis; Galesi, Nicola; Johannsen, Jan
  • Bounded universal expansion for preprocessing QBF
    Bubeck, Uwe; Büning, Hans Kleine
  • Towards NP-P via proof complexity and search
    Buss, Samuel R.
  • Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness
    Chen, Hubie
  • QBF Proof Complexity
    Chew, Leroy
  • Relating size and width in variants of Q-resolution
    Clymo, Judith; Beyersdorff, Olaf
  • Logical Foundations of Proof Complexity
    Cook, Stephen A.; Nguyen, Phuong
  • The relative efficiency of propositional proof systems
    Cook, Stephen A.; Reckhow, Robert A.
  • On stronger calculi for QBFs
    Egly, Uwe
  • Conformant planning as a case study of incremental QBF solving
    Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas
  • Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving, See McMillan et al
    Egly, Uwe; Lonsing, Florian; Widl, Magdalena
  • Parity, circuits, and the polynomial-time hierarchy
    Furst, Merrick L.; Saxe, James B.; Sipser, Michael
  • Reasoning with quantified Boolean formulas
    Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo
  • sQueezeBF: An effective preprocessor for QBFs based on equivalence reasoning
    Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo
  • Clause/term resolution and learning in the evaluation of quantified Boolean formulas
    Giunchiglia, E.; Narizzano, M.; Tacchella, A.
  • Recovering and utilizing partial duality in QBF
    Goultiaeva, Alexandra; Bacchus, Fahiem
  • Bridging the gap between dual propagation and CNF-based QBF solving
    Goultiaeva, Alexandra; Seidl, Martina; Biere, Armin
  • A uniform approach for generating proofs and strategies for both true and false QBF formulas
    Goultiaeva, Alexandra; Van Gelder, Allen; Bacchus, Fahiem
  • Computational Limitations of Small-depth Circuits
    Håstad, Johan
  • Solution validation and extraction for QBF preprocessing
    Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
  • An Achilles’ heel of term-resolution
    Janota, Mikoláš
  • On QBF proofs and preprocessing, See McMillan et al
    Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao
  • Solving QBF with counterexample guided refinement
    Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
  • Expansion-based QBF solving versus Q-resolution
    Janota, Mikoláš; Marques-Silva, Joao
  • A first step towards a unified proof checker for QBF
    Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M.
  • Theory of quantified Boolean formulas
    Büning, Hans Kleine; Bubeck, Uwe
  • Resolution for quantified Boolean formulas
    Büning, Hans Kleine; Karpinski, Marek; Flögel, Andreas
  • Boolean functions as models for quantified Boolean formulas
    Büning, Hans Kleine; Subramani, K.; Zhao, Xishun
  • A non-prenex, non-clausal QBF solver with game-state learning
    Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund M.
  • Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic
    Krajíček, Jan
  • Integrating dependency schemes in search-based QBF solvers
    Lonsing, Florian; Biere, Armin
  • Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation
    Lonsing, Florian; Egly, Uwe; Van Gelder, Allen
  • Logic for Programming, Artificial Intelligence, and Reasoning, LPAR
    McMillan, Kenneth L.; Middeldorp, Aart; (Eds, Andrei Voronkov
  • Computational Complexity
    Papadimitriou, Christos H.
  • Long distance Q-resolution with dependency schemes
    Peitl, Tomás; Slivovsky, Friedrich; Szeider, Stefan
  • Lower bounds for resolution and cutting planes proofs and monotone computations
    Pudlák, Pavel
  • A lower bound for DLL algorithms for SAT
    Pudlák, Pavel; Impagliazzo, Russell
  • Asymptotically optimal encodings of conformant planning in QBF
    Rintanen, Jussi
  • Learning decision lists
    Rivest, Ronald L.
  • A machine-oriented logic based on the resolution principle
    Robinson, John Alan
  • Variable dependencies of quantified CSPs
    Samer, Marko
  • Backdoor sets of quantified Boolean formulas
    Samer, Marko; Szeider, Stefan
  • Binary clause reasoning in QBF
    Samulowitz, Horst; Bacchus, Fahiem
  • The complexity of propositional proofs
    Segerlind, Nathan
  • Soundness of Q-resolution with dependency schemes
    Slivovsky, Friedrich; Szeider, Stefan
  • Variable independence and resolution paths for quantified Boolean formulas
    Van Gelder, Allen
  • Contributions to the theory of practical quantified Boolean formula solving
    Van Gelder, Allen
  • Primal and dual encoding from applications into quantified Boolean formulas
    Van Gelder, Allen
  • Introduction to Circuit Complexity -- A Uniform Approach
    Vollmer, H.
  • Conflict driven learning in a quantified Boolean satisfiability solver
    Zhang, Lintao; Malik, Sharad
  • Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation
    Zhang, Lintao; Malik, Sharad