DROPS

Artifact

Software

jreeves3/ulc-cadical

Authors: Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule

Abstract

Cite as

Aeacus Sheng, Joseph E. Reeves, Marijn J. H. Heule. jreeves3/ulc-cadical (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24212,
   title = {{jreeves3/ulc-cadical}}, 
   author = {Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:615c90061cfad33b59249832fb0043defef84419;origin=https://github.com/jreeves3/ulc-cadical;visit=swh:1:snp:f96217667e13be0663f27340946c119cf64504c9;anchor=swh:1:rev:bb9484ab042c423c1c37fa63dbac3679957afff1}{\texttt{swh:1:dir:615c90061cfad33b59249832fb0043defef84419}} (visited on 2025-08-07)},
   url = {https://github.com/jreeves3/ulc-cadical},
   doi = {10.4230/artifacts.24212},
}

Document

DOI: 10.4230/LIPIcs.SAT.2025.29

Reencoding Unique Literal Clauses

Authors: Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule

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

Abstract

We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements.

Cite as

Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule. Reencoding Unique Literal Clauses. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.SAT.2025.29,
  author =	{Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Reencoding Unique Literal Clauses}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{29:1--29:21},
  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.29},
  URN =		{urn:nbn:de:0030-drops-237635},
  doi =		{10.4230/LIPIcs.SAT.2025.29},
  annote =	{Keywords: Satisfiability solving, auxiliary variables, graph coloring}
}

Search Results

Documents authored by Sheng, Aeacus

jreeves3/ulc-cadical

Abstract

Cite as

Reencoding Unique Literal Clauses

Abstract

Cite as

Thanks for your feedback!

Could not send message