Document Open Access Logo

Learn to Unlearn

Authors Bernhard Gstrein , Florian Pollitt , André Schidler , Mathias Fleury , Armin Biere

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.14.pdf
  • Filesize: 1.4 MB
  • 12 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.14.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Satisfiability solving
  • learned clause recycling
  • LBD

Metrics

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

Abstract

Clause learning is a significant milestone in the development of SAT solving. However, keeping all learned clauses without discrimination gradually slows down the solver. Thus, selectively removing some learned clauses during routine database reduction is essential. In this paper, we reexamine and test several long-standing ideas for clause removal in the modern solver Kissat. Our experiments show that retaining all clauses alters performance in all instances. For satisfiable instances, periodically removing all learned clauses surprisingly yields near state-of-the-art performance. For unsatisfiable instances, it is vital to always keep some learned clauses. Building on the influential Glucose paper, we find that it is crucial to always retain the clauses most likely to help, regardless of whether they are ranked by size or LBD in practice. Another key factor is whether a clause was used recently during conflict resolution steps. Eagerly keeping used clauses improves all unlearning strategies.

Cite As Get BibTex

Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere. Learn to Unlearn. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 14:1-14:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.14

Author Details

Bernhard Gstrein
  • University of Freiburg, Germany
Florian Pollitt
  • University of Freiburg, Germany
André Schidler
  • University of Freiburg, Germany
Mathias Fleury
  • University of Freiburg, Germany
Armin Biere
  • University of Freiburg, Germany

Funding

This work was supported by the state of Baden-Württemberg through bwHPC, the German Research Foundation (DFG) grant INST 35/1597-1 FUGG, and a gift from Intel Corp.

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In IJCAI, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  2. Gilles Audemard and Laurent Simon. Refining restarts strategies for SAT and UNSAT. In CP, volume 7514 of Lecture Notes in Computer Science, pages 118-126. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_11.
  3. Gilles Audemard and Laurent Simon. On the Glucose SAT solver. Int. J. Artif. Intell. Tools, 27(1):1840001:1-1840001:25, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  4. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2024 - Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 of Department of Computer Science Report Series B, pages 8-10. University of Helsinki, 2024. Google Scholar
  5. Armin Biere, Matti Järvisalo, Daniel Le Berre, Kuldeep S. Meel, and Stefan Mengel. The SAT practitioner’s manifesto, September 2020. URL: https://doi.org/10.5281/zenodo.4500928.
  6. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. URL: https://doi.org/10.1145/368273.368557.
  7. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  8. Rina Dechter. Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition. Artificial Intelligence, 41(3):273-312, 1990. URL: https://doi.org/10.1016/0004-3702(90)90046-3.
  9. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  10. Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, and Laurent Simon. Seeking practical CDCL insights from theoretical SAT benchmarks. In Jérôme Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 1300-1308. ijcai.org, 2018. URL: https://doi.org/10.24963/IJCAI.2018/181.
  11. Roman Gershman and Ofer Strichman. Haifasat: a SAT solver based on an abstraction/refinement model. J. Satisf. Boolean Model. Comput., 6(1-3):33-51, 2009. URL: https://doi.org/10.3233/SAT190061.
  12. Matthew L Ginsberg. Dynamic backtracking. Journal of Artificial Intelligence Research, 1:25-46, 1993. URL: https://doi.org/10.1613/JAIR.1.
  13. Matthew L Ginsberg. Satsisfiability and systematicity. Journal of Artificial Intelligence Research, 53:497-540, 2015. URL: https://doi.org/10.1613/JAIR.4684.
  14. Eugene Goldberg and Yakov Novikov. BerkMin: A fast and robust Sat-solver. Discret. Appl. Math., 155(12):1549-1561, 2007. URL: https://doi.org/10.1016/J.DAM.2006.10.007.
  15. Evguenii I. Goldberg and Yakov Novikov. Berkmin: A fast and robust Sat-solver. In 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), 4-8 March 2002, Paris, France, pages 142-149. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/DATE.2002.998262.
  16. Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere. Kissat Clause Reduction Version. Software, (visited on 2025-07-16). URL: https://github.com/texmex76/kissat-cr
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24025
  17. Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere. Learn to unlearn, April 2025. URL: https://doi.org/10.5281/zenodo.15146408.
  18. Said Jabbour, Jerry Lonlac, Lakhdar Sais, and Yakoub Salhi. Revisiting the learned clauses database reduction strategies. International Journal on Artificial Intelligence Tools, 27, February 2014. URL: https://doi.org/10.1142/S0218213018500331.
  19. Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 355-370. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  20. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Benjamin Kuipers and Bonnie L. Webber, editors, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island, USA, pages 203-208. AAAI Press / The MIT Press, 1997. URL: http://www.aaai.org/Library/AAAI/1997/aaai97-032.php.
  21. 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, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2nd edition, 2021. URL: https://doi.org/10.3233/FAIA200987.
  22. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  23. Chanseok Oh. Between SAT and UNSAT: the fundamental difference in CDCL SAT. 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 LNCS, pages 307-323. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_23.
  24. João P. Marques Silva and Karem A. Sakallah. GRASP - A new search algorithm for satisfiability. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996, pages 220-227. IEEE Computer Society / ACM, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  25. Laurent Simon. Post mortem analysis of SAT solver proofs. In Daniel Le Berre, editor, POS-14. Fifth Pragmatics of SAT workshop, volume 27 of EPiC Series in Computing, pages 26-40. EasyChair, 2014. URL: https://doi.org/10.29007/gpp8.
  26. Alan Jay Smith. Sequentiality and prefetching in database systems. ACM Trans. Database Syst., 3(3):223-247, 1978. URL: https://doi.org/10.1145/320263.320276.
  27. Mate Soos, Raghav Kulkarni, and Kuldeep S. Meel. CrystalBall: Gazing in the black box of SAT solving. 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 371-387. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_26.
  28. Richard M Stallman and Gerald J Sussman. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial intelligence, 9(2):135-196, 1977. URL: https://doi.org/10.1016/0004-3702(77)90029-7.
  29. Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining SAT solving using causal reasoning. In SAT, volume 271 of LIPIcs, pages 28:1-28:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.28.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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