DROPS

Artifact

Software

Kissat Clause Reduction Version

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

Abstract

Cite as

Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere. Kissat Clause Reduction Version (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{github,
   title = {{Kissat Clause Reduction Version}}, 
   author = {Gstrein, Bernhard and Pollitt, Florian and Schidler, Andr\'{e} and Fleury, Mathias and Biere, Armin},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b6a189824ab8c4ceab3f1a2f31c349423724cc19;origin=https://github.com/texmex76/kissat-cr;visit=swh:1:snp:5683baa56ab6acbc85aca46b16845fd3f6da4cf6;anchor=swh:1:rev:84d0d475780fa7e507cd7c9749e4c77465c35bfa}{\texttt{swh:1:dir:b6a189824ab8c4ceab3f1a2f31c349423724cc19}} (visited on 2025-08-07)},
   url = {https://github.com/texmex76/kissat-cr},
   doi = {10.4230/artifacts.24025},
}

Document

DOI: 10.4230/LIPIcs.SAT.2025.14

Learn to Unlearn

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

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{gstrein_et_al:LIPIcs.SAT.2025.14,
  author =	{Gstrein, Bernhard and Pollitt, Florian and Schidler, Andr\'{e} and Fleury, Mathias and Biere, Armin},
  title =	{{Learn to Unlearn}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{14:1--14:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.14},
  URN =		{urn:nbn:de:0030-drops-237480},
  doi =		{10.4230/LIPIcs.SAT.2025.14},
  annote =	{Keywords: Satisfiability solving, learned clause recycling, LBD}
}

Search Results

Documents authored by Gstrein, Bernhard

Kissat Clause Reduction Version

Abstract

Cite as

Learn to Unlearn

Abstract

Cite as

Thanks for your feedback!

Could not send message