# Orbitopal Fixing in SAT

arXiv: https://arxiv.org/abs/2601.16855 · HTML: https://mlsanity.com/paper/2601.16855/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 38 references that are in the map.
- First posted on arXiv 23 Jan 2026.

## Builds on (most cited first, 10 of 10)

- [Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs](https://mlsanity.com/paper/2209.12185/) (2022)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [A Commentary on "Breaking Row and Column Symmetries in Matrix Models"](https://mlsanity.com/paper/1910.01423/) (2019)
- [satsuma: Structure-based Symmetry Breaking in SAT](https://mlsanity.com/paper/2406.13557/) (2024)
- [An adaptive prefix-assignment technique for symmetry reduction](https://mlsanity.com/paper/1706.08325/) (2017)
- [Search Problems in Trees with Symmetries: near optimal traversal strategies for individualization-refinement algorithms](https://mlsanity.com/paper/2011.01726/) (2020)
- [Parallel Computation of Combinatorial Symmetries](https://mlsanity.com/paper/2108.04590/) (2021)
- [DRAT and Propagation Redundancy Proofs Without New Variables](https://mlsanity.com/paper/1909.00520/) (2019)
- [Even shorter proofs without new variables](https://mlsanity.com/paper/2307.12098/) (2023)
- [State-of-the-art Methods for Pseudo-Boolean Solving with SCIP](https://mlsanity.com/paper/2501.03390/) (2025)

## Abstract (arXiv)

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.