Document Open Access Logo

Learning Shorter Redundant Clauses in SDCL Using MaxSAT

Authors Albert Oliveras , Chunxiao Li, Darryl Wu, Jonathan Chung , Vijay Ganesh

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.18.pdf
  • Filesize: 0.78 MB
  • 17 pages

Document Identifiers

Author Details

Albert Oliveras
  • Technical University of Catalonia, Barcelona, Spain
Chunxiao Li
  • University of Waterloo, Canada
Darryl Wu
  • University of Waterloo, Canada
Jonathan Chung
  • University of Waterloo, Canada
Vijay Ganesh
  • University of Waterloo, Canada

Funding

  • Oliveras, Albert: Supported by grant PID2021-122830OB-C43, funded by MCIN/AEI/ 10.13039/501100011033 and by "ERDF: A way of making Europe".

Cite AsGet BibTex

Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh. Learning Shorter Redundant Clauses in SDCL Using MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.18

Abstract

In this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant clauses. We also perform a thorough empirical evaluation of our method and show that our SDCL solver solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • SAT
  • SDCL
  • MaxSAT

Metrics

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

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. URL: https://doi.org/10.1613/jair.3152.
  2. Florent Avellaneda. A short description of the solver EvalMaxSAT. In Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors, MaxSAT Evaluation 2020, pages 8-9, 2020. Google Scholar
  3. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  4. Armin Biere and Andreas Fröhlich. Evaluating CDCL variable scoring schemes. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 405-422. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_29.
  5. Armin Biere and Daniel Kröning. Sat-based model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 277-303. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_10.
  6. Avrim L Blum and Merrick L Furst. Fast planning through planning graph analysis. Artificial intelligence, 90(1-2):281-300, 1997. Google Scholar
  7. Cristian Cadar, Vijay Ganesh, Peter M Pawlowski, David L Dill, and Dawson R Engler. EXE: Automatically Generating Inputs of Death. ACM Transactions on Information and System Security (TISSEC), 12(2):1-38, 2008. Google Scholar
  8. Edmund M Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. Model Checking. MIT press, 2018. Google Scholar
  9. Stephen A. Cook. The Complexity of Theorem-Proving Procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pages 151-158, 1971. URL: https://doi.org/10.1145/800157.805047.
  10. Stephen A. Cook. A short proof of the pigeon hole principle using extended resolution. SIGACT News, 8(4):28-32, 1976. URL: https://doi.org/10.1145/1008335.1008338.
  11. Julian Dolby, Mandana Vaziri, and Frank Tip. Finding Bugs Efficiently With a SAT Solver. In Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 195-204, 2007. URL: https://doi.org/10.1145/1287624.1287653.
  12. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Short proofs without new variables. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 130-147. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_9.
  13. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Encoding redundancy for satisfaction-driven clause learning. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 41-58. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_3.
  14. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason., 64(3):533-554, 2020. URL: https://doi.org/10.1007/s10817-019-09516-0.
  15. Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. Pruning through satisfaction. In Ofer Strichman and Rachel Tzoref-Brill, editors, Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, Proceedings, volume 10629 of Lecture Notes in Computer Science, pages 179-194. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-70389-3_12.
  16. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 228-245. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  17. Lefteris M. Kirousis and Phokion G. Kolaitis. The complexity of minimal satisfiability problems. Inf. Comput., 187(1):20-39, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00037-3.
  18. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 123-140. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_9.
  19. João 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 - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  20. 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.
  21. Mukul R. Prasad, Armin Biere, and Aarti Gupta. A survey of recent advances in sat-based formal verification. Int. J. Softw. Tools Technol. Transf., 7(2):156-173, 2005. URL: https://doi.org/10.1007/s10009-004-0183-4.
  22. Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant. Preprocessing of propagation redundant clauses. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 106-124. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_8.
  23. João P. Marques Silva and Karem A. Sakallah. Invited tutorial: Boolean satisfiability algorithms and applications in electronic design automation. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, page 3. Springer, 2000. URL: https://doi.org/10.1007/10722167_3.
  24. Grigori S Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967-1970, pages 466-483, 1983. Google Scholar
  25. Yichen Xie and Alexander Aiken. Saturn: A SAT-Based Tool for Bug Detection. In Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005, pages 139-143, 2005. URL: https://doi.org/10.1007/11513988_13.
  26. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified boolean satisfiability solver. In Lawrence T. Pileggi and Andreas Kuehlmann, editors, Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, ICCAD 2002, San Jose, California, USA, November 10-14, 2002, pages 442-449. ACM / IEEE Computer Society, 2002. URL: https://doi.org/10.1145/774572.774637.
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