Document Open Access Logo

Should Decisions in QCDCL Follow Prefix Order?

Authors Benjamin Böhm , Tomáš Peitl , Olaf Beyersdorff

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.11.pdf
  • Filesize: 1.15 MB
  • 19 pages

Document Identifiers

Author Details

Benjamin Böhm
  • Friedrich Schiller Universität Jena, Germany
Tomáš Peitl
  • TU Wien, Vienna, Austria
Olaf Beyersdorff
  • Friedrich Schiller Universität Jena, Germany

Funding

  • Peitl, Tomáš: Austrian Science Fund FWF, grant no. J4361-N.
  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1.

Cite AsGet BibTex

Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff. Should Decisions in QCDCL Follow Prefix Order?. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.11

Abstract

Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions. We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system QCDCL^ANY is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses (QCDCL^UNI-ANI) and asserting cubes (QCDCL^EXI-ANY), respectively. We model all four approaches by formal proof systems and show that QCDCL^UNI-ANY is exponentially better than QCDCL on false formulas, whereas QCDCL^EXI-ANY is exponentially better than QCDCL on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems. We complement our theoretical study with some initial experiments that confirm our theoretical findings.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • CDCL
  • proof complexity
  • lower bounds

Metrics

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

Related Versions

Supplementary Materials

References

  1. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res., 40:353-373, 2011. Google Scholar
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Form. Methods Syst. Des., 41(1):45-65, 2012. Google Scholar
  3. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR), 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  4. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Logical Methods in Computer Science, 15(1), 2019. Google Scholar
  5. Olaf Beyersdorff and Benjamin Böhm. QCDCL with cube learning or pure literal elimination - what is best? Electron. Colloquium Comput. Complex., page 131, 2021. URL: https://eccc.weizmann.ac.il/report/2021/131.
  6. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. In Proc. Innovations in Theoretical Computer Science (ITCS), pages 12:1-12:20, 2021. Google Scholar
  7. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. Google Scholar
  8. Benjamin Böhm and Olaf Beyersdorff. Lower bounds for QCDCL via formula gauge. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021, pages 47-63, Cham, 2021. Springer International Publishing. Google Scholar
  9. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 233-350. IOS Press, 2021. Google Scholar
  10. Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An algorithm to evaluate quantified Boolean formulae. In Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference (AAAI), pages 262-267, 1998. Google Scholar
  11. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  12. Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. Reasoning with quantified Boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 761-780. IOS Press, 2009. Google Scholar
  13. Marijn Heule. Proofs of unsatisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, 2nd edition, Frontiers in Artificial Intelligence and Applications, pages 635-668. IOS press, 2021. Google Scholar
  14. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017. Google Scholar
  15. Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Portfolio-based algorithm selection for circuit qbfs. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 195-209. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_13.
  16. Mikolás Janota. On Q-Resolution and CDCL QBF solving. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 402-418, 2016. Google Scholar
  17. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  18. Mikoláš Janota and Joao Marques-Silva. An Achilles' heel of term-resolution. In Eugénio Oliveira, João Gama, Zita Vale, and Henrique Lopes Cardoso, editors, Progress in Artificial Intelligence, pages 670-680, Cham, 2017. Springer International Publishing. Google Scholar
  19. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  20. Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice. PhD thesis, Johannes Kepler University Linz, 2012. Google Scholar
  21. Florian Lonsing and Uwe Egly. DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In Proc. International Conference on Automated Deduction (CADE), pages 371-384, 2017. Google Scholar
  22. Florian Lonsing and Uwe Egly. Evaluating QBF solvers: Quantifier alternations matter. In Proc. Principles and Practice of Constraint Programming (CP), pages 276-294. Springer, 2018. Google Scholar
  23. João P. Marques Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  24. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Proc. IEEE/ACM International Conference on Computer-aided Design (ICCAD), pages 220-227, 1996. URL: https://doi.org/10.1145/244522.244560.
  25. M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: engineering an efficient sat solver. In Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232), pages 530-535, 2001. URL: https://doi.org/11.1145/378239.379017.
  26. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Combining resolution-path dependencies with dependency learning. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 306-318. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_22.
  27. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. J. Artif. Intell. Res., 65:180-208, 2019. Google Scholar
  28. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-distance Q-resolution with dependency schemes. J. Autom. Reasoning, 63(1):127-155, 2019. Google Scholar
  29. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  30. Marko Samer and Stefan Szeider. Backdoor sets of quantified Boolean formulas. Journal of Automated Reasoning, 42(1):77-97, 2009. URL: https://doi.org/10.1007/s10817-008-9114-5.
  31. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In Proc. IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 78-84, 2019. Google Scholar
  32. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theoretical Computer Science, 612:83-101, 2016. Google Scholar
  33. Ole Tange. GNU Parallel - The command-line power tool. login: The USENIX Magazine, February:42-47, 2011. Google Scholar
  34. Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2020. Google Scholar
  35. Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in Boolean satisfiability solver. In Proc. IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pages 279-285, 2001. Google Scholar
  36. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In Proc. IEEE/ACM International Conference on Computer-aided Design (ICCAD), pages 442-449, 2002. 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