DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.28

Factoring Learned Clauses

Authors: Florian Pollitt, Zachary Battleman, Mathias Fleury, Yakir Vizel, Marijn J. H. Heule, Armin Biere, and Randal E. Bryant

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

Modern SAT solvers are based on the conflict-driven clause learning (CDCL) paradigm, which can be simulated by the resolution proof system. This limits solver effectiveness on instances known to be hard for resolution. Certain approaches, such as parity reasoning, have been shown to be effective in this context, but are hard to integrate with CDCL, in particular, with mainstream proof certificates. The powerful yet simple Extended Resolution (ER) proof system provides an alternative but is not widely used in SAT solving despite having proof certificates for decades and using it effectively remains an open challenge. This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL. We further propose a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally. Previous work on bounded variable addition focused on AND gates and original clauses only. Our experimental evaluation shows substantial improvements on hard combinatorial benchmark families without performance degradation on the SAT Competition.

Cite as

Florian Pollitt, Zachary Battleman, Mathias Fleury, Yakir Vizel, Marijn J. H. Heule, Armin Biere, and Randal E. Bryant. Factoring Learned Clauses. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{pollitt_et_al:LIPIcs.SAT.2026.28,
  author =	{Pollitt, Florian and Battleman, Zachary and Fleury, Mathias and Vizel, Yakir and Heule, Marijn J. H. and Biere, Armin and Bryant, Randal E.},
  title =	{{Factoring Learned Clauses}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.28},
  URN =		{urn:nbn:de:0030-drops-263343},
  doi =		{10.4230/LIPIcs.SAT.2026.28},
  annote =	{Keywords: SAT solving, Extended Resolution, CDCL, Inprocessing}
}

Document

Tool Paper

DOI: 10.4230/LIPIcs.SAT.2026.40

CaDiCaL 3.0 (Tool Paper)

Authors: Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

The propositional satisfiability (SAT) solver Kissat supports a relatively narrow feature set in favor of bare-metal performance and targeted improvements to core solving techniques, which helped it dominate the International SAT Competition since 2024. However, many applications rely on advanced SAT solver features such as incremental interaction schemes, finding direct consequences of assumed literals, or expressive proof logging that allows for real-time checking. This system description reports on how we successfully adapted Kissat’s award-winning techniques to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition. The main challenge was to support efficient linear proof production with hints. We further extended CaDiCaL’s API to extract implied literals under assumptions and applied advanced deterministic scheduling of inprocessing based on the ticks metric for approximating cache line accesses. Experiments confirm the benefits of these efforts.

Cite as

Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. CaDiCaL 3.0 (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 40:1-40:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{pollitt_et_al:LIPIcs.SAT.2026.40,
  author =	{Pollitt, Florian and Fleury, Mathias and Fazekas, Katalin and Froleyks, Nils and Schidler, Andr\'{e} and Schreiber, Dominik and Biere, Armin},
  title =	{{CaDiCaL 3.0}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{40:1--40:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.40},
  URN =		{urn:nbn:de:0030-drops-263465},
  doi =		{10.4230/LIPIcs.SAT.2026.40},
  annote =	{Keywords: Incremental SAT, CaDiCaL, SAT Solver}
}

Artifact

Software

DOI: 10.4230/artifacts.24025

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}
}

Document

DOI: 10.4230/LIPIcs.SAT.2023.21

Faster LRAT Checking Than Solving with CaDiCaL

Authors: Florian Pollitt, Mathias Fleury, and Armin Biere

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract

DRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs.

Cite as

Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT Checking Than Solving with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 21:1-21:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{pollitt_et_al:LIPIcs.SAT.2023.21,
  author =	{Pollitt, Florian and Fleury, Mathias and Biere, Armin},
  title =	{{Faster LRAT Checking Than Solving with CaDiCaL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{21:1--21:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.21},
  URN =		{urn:nbn:de:0030-drops-184837},
  doi =		{10.4230/LIPIcs.SAT.2023.21},
  annote =	{Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT}
}

Search Results

Documents authored by Pollitt, Florian

Factoring Learned Clauses

Abstract

Cite as

CaDiCaL 3.0 (Tool Paper)

Abstract

Cite as

Kissat Clause Reduction Version

Abstract

Cite as

Learn to Unlearn

Abstract

Cite as

Faster LRAT Checking Than Solving with CaDiCaL

Abstract

Cite as

Thanks for your feedback!

Could not send message