2026-10-08T15:24:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23763 2025-11-12T12:00:20Z ddc:004 open_access

Reencoding Unique Literal Clauses Sheng, Aeacus Reeves, Joseph E. Heule, Marijn J. H. Satisfiability solving auxiliary variables graph coloring 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aeacus Sheng and Joseph E. Reeves and Marijn J. H. Heule 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.29 urn:nbn:de:0030-drops-237635 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.29 eng https://creativecommons.org/licenses/by/4.0/legalcode