Document Open Access Logo

Quantified CDCL with Universal Resolution

Author Friedrich Slivovsky

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.24.pdf
  • Filesize: 0.9 MB
  • 16 pages

Document Identifiers

Author Details

Friedrich Slivovsky
  • TU Wien, Austria

Funding

  • Slivovsky, Friedrich: Vienna Science and Technology Fund (WWTF) Grant ICT19-060.

Acknowledgements

The author would like to thank the anonymous reviewers for their helpful comments towards improving this paper.

Cite AsGet BibTex

Friedrich Slivovsky. Quantified CDCL with Universal Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.24

Abstract

Quantified Conflict-Driven Clause Learning (QCDCL) solvers for QBF generate Q-resolution proofs. Pivot variables in Q-resolution must be existentially quantified. Allowing resolution on universally quantified variables leads to a more powerful proof system called QU-resolution, but so far, QBF solvers have used QU-resolution only in very limited ways. We present a new version of QCDCL that generates proofs in QU-resolution by leveraging propositional unit propagation. We detail how conflict analysis must be adapted to handle universal variables assigned by propagation, and show that the procedure is still sound and terminating. We further describe how dependency learning can be incorporated in the algorithm to increase the flexibility of decision heuristics. Experiments with crafted instances and benchmarks from recent QBF evaluations demonstrate the viability of the resulting version of QCDCL.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • QBF
  • Q-Resolution
  • QU-Resolution
  • CDCL

Metrics

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

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pages 399-404, 2009. Google Scholar
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods Syst. Des., 41(1):45-65, 2012. Google Scholar
  3. Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolas Janota, and Magdalena Widl. Efficient extraction of QBF (counter)models from long-distance resolution proofs. In AAAI, pages 3694-3701. AAAI Press, 2015. Google Scholar
  4. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In SAT, volume 8561 of Lecture Notes in Computer Science, pages 154-169. Springer, 2014. Google Scholar
  5. Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Comput. Surv., 51(3):50:1-50:39, 2018. Google Scholar
  6. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. J. Autom. Reason., 65(1):125-154, 2021. Google Scholar
  7. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. In ITCS, volume 185 of LIPIcs, pages 12:1-12:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  8. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory, 11(4):26:1-26:42, 2019. Google Scholar
  9. Olaf Beyersdorff, Luca Pulina, Martina Seidl, and Ankit Shukla. Qbffam: A tool for generating QBF families from proof complexity. In SAT, volume 12831 of Lecture Notes in Computer Science, pages 21-29. Springer, 2021. Google Scholar
  10. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Rance Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Proceedings, volume 1579 of Lecture Notes in Computer Science, pages 193-207. Springer, 1999. Google Scholar
  11. Nikolaj Bjørner, Mikolás Janota, and William Klieber. On conflicts and strategies in QBF. In LPAR (short papers), volume 35 of EPiC Series in Computing, pages 28-41. EasyChair, 2015. Google Scholar
  12. Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, and Martina Seidl. Two SAT solvers for solving quantified boolean formulas with an arbitrary number of quantifier alternations. Formal Methods Syst. Des., 57(2):157-177, 2021. Google Scholar
  13. Marco Cadoli, Marco Schaerf, Andrea Giovanardi, and Massimo Giovanardi. An algorithm to evaluate quantified boolean formulae and its experimental evaluation. J. Autom. Reason., 28(2):101-142, 2002. Google Scholar
  14. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, SAT 2003, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. Google Scholar
  15. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In LPAR, volume 8312 of Lecture Notes in Computer Science, pages 291-308. Springer, 2013. Google Scholar
  16. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT competition 2020. Artif. Intell., 301:103572, 2021. Google Scholar
  17. Allen Van Gelder. Contributions to the theory of practical quantified boolean formula solving. In CP, volume 7514 of Lecture Notes in Computer Science, pages 647-663. Springer, 2012. Google Scholar
  18. Allen Van Gelder, Samuel B. Wood, and Florian Lonsing. Extended failed-literal preprocessing for quantified boolean formulas. In SAT, volume 7317 of Lecture Notes in Computer Science, pages 86-99. Springer, 2012. Google Scholar
  19. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Clause/term resolution and learning in the evaluation of quantified boolean formulas. J. Artif. Intell. Res., 26:371-416, 2006. Google Scholar
  20. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause elimination for SAT and QSAT. J. Artif. Intell. Res., 53:127-168, 2015. Google Scholar
  21. Mikolás Janota. Towards generalization in QBF solving via machine learning. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), pages 6607-6614. AAAI Press, 2018. Google Scholar
  22. Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1-25, 2016. Google Scholar
  23. Mikolás Janota and João Marques-Silva. Solving QBF by clause selection. In IJCAI, pages 325-331. AAAI Press, 2015. Google Scholar
  24. Mikolás Janota and João Marques-Silva. An achilles' heel of term-resolution. In EPIA, volume 10423 of Lecture Notes in Computer Science, pages 670-680. Springer, 2017. Google Scholar
  25. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  26. William Klieber. Ghostq. J. Satisf. Boolean Model. Comput., 11(1):65-72, 2019. Google Scholar
  27. Florian Lonsing and Armin Biere. Integrating dependency schemes in search-based QBF solvers. In SAT, volume 6175 of Lecture Notes in Computer Science, pages 158-171. Springer, 2010. Google Scholar
  28. Florian Lonsing and Armin Biere. Failed literal detection for QBF. In SAT, volume 6695 of Lecture Notes in Computer Science, pages 259-272. Springer, 2011. Google Scholar
  29. Florian Lonsing and Uwe Egly. Evaluating QBF solvers: Quantifier alternations matter. In CP, volume 11008 of Lecture Notes in Computer Science, pages 276-294. Springer, 2018. Google Scholar
  30. Florian Lonsing, Uwe Egly, and Allen Van Gelder. Efficient clause learning for quantified boolean formulas via QBF pseudo unit propagation. In SAT, volume 7962 of Lecture Notes in Computer Science, pages 100-115. Springer, 2013. Google Scholar
  31. Florian Lonsing, Uwe Egly, and Martina Seidl. Q-resolution with generalized axioms. In SAT, volume 9710 of Lecture Notes in Computer Science, pages 435-452. Springer, 2016. Google Scholar
  32. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In DAC, pages 530-535. ACM, 2001. Google Scholar
  33. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. J. Artif. Intell. Res., 65:180-208, 2019. Google Scholar
  34. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (qbfeval'16 and qbfeval'17). Artif. Intell., 274:224-248, 2019. Google Scholar
  35. Markus N. Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In FMCAD, pages 136-143. IEEE, 2015. Google Scholar
  36. Olivier Roussel. Controlling a solver execution with the runsolver tool. J. Satisf. Boolean Model. Comput., 7(4):139-144, 2011. Google Scholar
  37. Horst Samulowitz and Fahiem Bacchus. Using SAT in QBF. In CP, volume 3709 of Lecture Notes in Computer Science, pages 578-592. Springer, 2005. Google Scholar
  38. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified boolean formulas. In ICTAI, pages 78-84. IEEE, 2019. Google Scholar
  39. Niklas Sörensson and Armin Biere. Minimizing learned clauses. In SAT, volume 5584 of Lecture Notes in Computer Science, pages 237-243. Springer, 2009. Google Scholar
  40. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. Google Scholar
  41. Martin Suda and Bernhard Gleiss. Local soundness for QBF calculi. In SAT, volume 10929 of Lecture Notes in Computer Science, pages 217-234. Springer, 2018. Google Scholar
  42. Leander Tentrup. Non-prenex QBF solving using abstraction. In SAT, volume 9710 of Lecture Notes in Computer Science, pages 393-401. Springer, 2016. Google Scholar
  43. Leander Tentrup. On expansion and resolution in CEGAR based QBF solving. In CAV (2), volume 10427 of Lecture Notes in Computer Science, pages 475-494. Springer, 2017. Google Scholar
  44. Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean satisfiability solvers and their applications in model checking. Proc. IEEE, 103(11):2021-2035, 2015. Google Scholar
  45. Ralf Wimmer, Christoph Scholl, and Bernd Becker. The (D)QBF preprocessor HQSpre - Underlying theory and its implementation. J. Satisf. Boolean Model. Comput., 11(1):3-52, 2019. Google Scholar
  46. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified boolean satisfiability solver. In ICCAD, pages 442-449. ACM / IEEE Computer Society, 2002. Google Scholar
  47. Lintao Zhang and Sharad Malik. Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In CP, volume 2470 of Lecture Notes in Computer Science, pages 200-215. Springer, 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