Orbitopal Fixing in SAT
This addresses performance issues for SAT solver users by reducing redundant computations, though it is an incremental adaptation of an existing technique.
The paper tackled the problem of symmetry causing SAT solvers to waste time exploring redundant search regions, by adapting orbitopal fixing from mixed-integer programming to break symmetries with unit clauses, resulting in consistent speedups on symmetry-rich benchmarks with negligible regressions.
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.