Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Orbitopal Fixing in SAT

Markus Anders, Cayden Codel, Marijn J. H. Heule

TL;DR

This work tackles the challenge of symmetry in SAT solving while maintaining compatibility with formal proof logging. It adapts orbitopal fixing from mixed-integer programming to introduce three unit-clause symmetry-breaking methods—orbitopal fixing, clausal fixing, and negation fixing—that leverage row symmetry and unique literal clauses, producing succinct substitution redundancy (sr) proofs. Implemented in the satsuma tool, the approach yields substantial speedups on symmetry-rich benchmarks with negligible preprocessing overhead and less regression on satisfiable instances compared to lex-leader methods. The study demonstrates practical impact by achieving improvements in CaDiCaL performance across multiple benchmark suites and provides a pathway for integrating surgical symmetry reasoning that remains lightweight and proof-friendly.

Abstract

Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones already explored. While symmetry handling is routine in other solving paradigms, integrating it into state-of-the-art proof-producing SAT solvers is difficult: added reasoning must be fast, non-interfering with solver heuristics, and compatible with formal proof logging. To address these issues, we present a practical static symmetry breaking approach based on orbitopal fixing, a technique adapted from mixed-integer programming. Our approach adds only unit clauses, which minimizes downstream slowdowns, and it emits succinct proof certificates in the substitution redundancy proof system. Implemented in the satsuma tool, our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.

Orbitopal Fixing in SAT

TL;DR

This work tackles the challenge of symmetry in SAT solving while maintaining compatibility with formal proof logging. It adapts orbitopal fixing from mixed-integer programming to introduce three unit-clause symmetry-breaking methods—orbitopal fixing, clausal fixing, and negation fixing—that leverage row symmetry and unique literal clauses, producing succinct substitution redundancy (sr) proofs. Implemented in the satsuma tool, the approach yields substantial speedups on symmetry-rich benchmarks with negligible preprocessing overhead and less regression on satisfiable instances compared to lex-leader methods. The study demonstrates practical impact by achieving improvements in CaDiCaL performance across multiple benchmark suites and provides a pathway for integrating surgical symmetry reasoning that remains lightweight and proof-friendly.

Abstract

Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones already explored. While symmetry handling is routine in other solving paradigms, integrating it into state-of-the-art proof-producing SAT solvers is difficult: added reasoning must be fast, non-interfering with solver heuristics, and compatible with formal proof logging. To address these issues, we present a practical static symmetry breaking approach based on orbitopal fixing, a technique adapted from mixed-integer programming. Our approach adds only unit clauses, which minimizes downstream slowdowns, and it emits succinct proof certificates in the substitution redundancy proof system. Implemented in the satsuma tool, our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.
Paper Structure (5 sections, 1 theorem, 1 figure)

This paper contains 5 sections, 1 theorem, 1 figure.

Table of Contents

  1. Introduction
  2. Contribution.
  3. Preliminaries
  4. Unique Literal Clauses
  5. Syntactic Symmetry of Formulas

Key Result

lemma thmcounterlemma

Let $F$ be a formula, and let $C \in F$ be a ULC. If $F$ is satisfiable, then it can be satisfied by a truth assignment that sets exactly one literal in $C$ to true.

Figures (1)

  • Figure 1: A graph modeling the symmetries of the formula $(x \vee y \vee z) \land (\overline x \vee \overline y) \land (\overline x \vee \overline z) \land (\overline y \vee \overline z)$. Every clause is connected to its component literals, and every literal is adjacent to its negation. On the left, the green arrows indicate the symmetry mapping $x$ to $y$, $y$ to $z$, and $z$ to $x$. On the right, the colors indicate the orbits of the vertices.

Theorems & Definitions (1)

  • lemma thmcounterlemma: ShengRH25, Lemma 4