Document Open Access Logo

Genuine Lower Bounds for QBF Expansion

Authors Olaf Beyersdorff, Joshua Blinkhorn

PDF
Thumbnail PDF

File

LIPIcs.STACS.2018.12.pdf
  • Filesize: 488 kB
  • 15 pages

Document Identifiers

Author Details

Olaf Beyersdorff
Joshua Blinkhorn

Cite AsGet BibTex

Olaf Beyersdorff and Joshua Blinkhorn. Genuine Lower Bounds for QBF Expansion. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.STACS.2018.12

Abstract

We propose the first general technique for proving genuine lower bounds in expansion-based QBF proof systems. We present the technique in a framework centred on natural properties of winning strategies in the 'evaluation game' interpretation of QBF semantics. As applications, we prove an exponential proof-size lower bound for a whole class of formula families, and demonstrate the power of our approach over existing methods by providing alternative short proofs of two known hardness results. We also use our technique to deduce a result with manifest practical import: in the absence of propositional hardness, formulas separating the two major QBF expansion systems must have unbounded quantifier alternations.
Keywords
  • QBF
  • proof complexity
  • lower-bound techniques
  • resolution

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Valeriy Balabanov, Jie-Hong Roland Jiang, Mikoláš Janota, and Magdalena Widl. Efficient extraction of QBF (counter)models from long-distance resolution proofs. In Conference on Artificial Intelligence (AAAI), pages 3694-3701, 2015. Google Scholar
  2. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 154-169, 2014. Google Scholar
  3. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. Google Scholar
  4. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 5(1-4):133-191, 2008. Google Scholar
  5. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Electronic Colloquium on Computational Complexity (ECCC), 24:35, 2017. Google Scholar
  6. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In ACM Conference on Innovations in Theoretical Computer Science (ITCS), pages 249-260, 2016. Google Scholar
  7. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 81-93, 2014. Google Scholar
  8. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. Proof complexity of resolution-based QBF calculi. In International Symposium on Theoretical Aspects of Computer Science (STACS), volume 30, pages 76-89, 2015. Google Scholar
  9. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. In International Colloquium on Automata, Languages, and Programming (ICALP), pages 180-192, 2015. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are short proofs narrow? QBF resolution is not simple. In Symposium on Theoretical Aspects of Computer Science (STACS), pages 15:1-15:14, 2016. Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-resolution size. Journal of Computer and System Sciences (in press), 2017. Google Scholar
  12. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A characterization of tree-like resolution size. Information Processing Letters, 113(18):666-671, 2013. Google Scholar
  13. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. In Conference on Foundations of Software Technology and Theoretical Computer Science (FCTTCS), 2017. Preprint available at ECCC, TR17-044. Google Scholar
  14. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  15. Michael Cashmore, Maria Fox, and Enrico Giunchiglia. Partially grounded planning as quantified Boolean formula. In International Conference on Automated Planning and Scheduling (ICAPS), 2013. Google Scholar
  16. Hubie Chen. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. In International Colloquium on Automata, Languages, and Programming (ICALP), pages 94:1-94:14, 2016. Google Scholar
  17. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge, 2010. Google Scholar
  18. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  19. William Craig. Linear reasoning. A new form of the Herbrand-Gentzen Theorem. J. Symb. Log., 22(3):250-268, 1957. Google Scholar
  20. Nachum Dershowitz, Ziyad Hanna, and Jacob Katz. Space-efficient bounded model checking. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 502-518. Springer, 2005. Google Scholar
  21. Uwe Egly. On stronger calculi for QBFs. In Theory and Applications of Satisfiability Testing (SAT), pages 419-434, 2016. Google Scholar
  22. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. Annals of Mathematics and Artificial Intelligence, 80(1):21-45, 2017. Google Scholar
  23. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pages 291-308, 2013. Google Scholar
  24. Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. Reasoning with quantified Boolean formulas. In Handbook of Satisfiability, pages 761-780. IOS Press, 2009. Google Scholar
  25. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. QBF reasoning on real-world instances. In International Conference on Theory and Applications of Satisfiability Testing (SAT), online proceedings, 2004. Google Scholar
  26. Mikolás Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Journal of Artificial Intelligence, 234:1-25, 2016. Google Scholar
  27. Mikoláš Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science, 577:25-42, 2015. Google Scholar
  28. Charles Jordan and Lukasz Kaiser. Experiments with reduction finding. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 192-207, 2013. Google Scholar
  29. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Information and Computation, 117(1):12-18, 1995. Google Scholar
  30. Roman Kontchakov, Luca Pulina, Ulrike Sattler, Thomas Schneider, Petra Selmer, Frank Wolter, and Michael Zakharyaschev. Minimal module extraction from DL-lite ontologies using QBF solvers. In International Joint Conference on Artificial Intelligence (IJCAI), pages 836-841. AAAI Press, 2009. Google Scholar
  31. Jan Krajícek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  32. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995. Google Scholar
  33. Andrew C. Ling, Deshanand P. Singh, and Stephen Dean Brown. FPGA logic synthesis using quantified boolean satisfiability. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 444-450, 2005. Google Scholar
  34. Florian Lonsing, Uwe Egly, and Martina Seidl. Q-resolution with generalized axioms. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 435-452, 2016. Google Scholar
  35. Hratch Mangassarian, Andreas G. Veneris, and Marco Benedetti. Robust QBF encodings for sequential circuits with applications to verification, debug, and test. IEEE Transactions on Computers, 59(7):981-994, 2010. Google Scholar
  36. Hratch Mangassarian, Andreas G. Veneris, Sean Safarpour, Marco Benedetti, and Duncan Exon Smith. A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In International Conference on Computer-Aided Design (ICCAD), pages 240-245, 2007. Google Scholar
  37. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long distance Q-resolution with dependency schemes. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 500-518, 2016. Google Scholar
  38. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for sat (preliminary version). In Symposium on Discrete Algorithms, pages 128-136, 2000. Google Scholar
  39. Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In National Conference on Artificial Intelligence (AAAI), pages 1045-1050. AAAI Press, 2007. Google Scholar
  40. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  41. Stefan Staber and Roderick Bloem. Fault localization and correction with QBF. In International Conference on Theory and Applications of Satisfiability Testing (SAT) 2007, pages 355-368, 2007. Google Scholar
  42. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Annual Symposium on Theory of Computing, pages 1-9. ACM, 1973. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact