Orbitopal Fixing in SAT

TL;DR

This paper introduces a practical orbitopal fixing method for SAT solvers that efficiently handles symmetry, resulting in consistent speedups on benchmarks with minimal impact on performance.

Contribution

It adapts orbitopal fixing from mixed-integer programming to SAT solving, enabling fast, proof-compatible symmetry breaking with minimal overhead.

Findings

Achieves speedups on symmetry-rich benchmarks

Adds only unit clauses to break symmetries

Produces succinct proof certificates

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.