satsuma: Structure-based Symmetry Breaking in SAT

TL;DR

Addressing the challenge of symmetry in SAT, the paper argues static symmetry breaking provides solver-agnostic pruning but often yields limited reduction, motivating a broader, structure-based approach. Satsuma introduces new practical detection algorithms for symmetry subgroups—row interchangeability, row-column symmetry, Johnson symmetry, and combinations—based on the individualization-refinement framework and then emits lex-leader constraints $LL^{\prec}_\varphi$ tailored to the detected structure. The authors implement Satsuma as a prototype (open-source) that reuses BreakID components and runs as a preprocessor, comparing against BreakID on standard symmetric SAT families. Benchmarks show improved performance when Johnson symmetry is present, comparable results for row and row-column cases, and generally lower preprocessing overhead, suggesting a scalable advantage for diverse symmetry structures.

Abstract

Symmetry reduction is crucial for solving many interesting SAT instances in practice. Numerous approaches have been proposed, which try to strike a balance between symmetry reduction and computational overhead. Arguably the most readily applicable method is the computation of static symmetry breaking constraints: a constraint restricting the search-space to non-symmetrical solutions is added to a given SAT instance. A distinct advantage of static symmetry breaking is that the SAT solver itself is not modified. A disadvantage is that the strength of symmetry reduction is usually limited. In order to boost symmetry reduction, the state-of-the-art tool BreakID [Devriendt et. al] pioneered the identification and tailored breaking of a particular substructure of symmetries, the so-called row interchangeability groups. In this paper, we propose a new symmetry breaking tool called satsuma. The core principle of our tool is to exploit more diverse but frequently occurring symmetry structures. This is enabled by new practical detection algorithms for row interchangeability, row-column symmetry, Johnson symmetry, and various combinations. Based on the resulting structural description, we then produce symmetry breaking constraints. We compare this new approach to BreakID on a range of instance families exhibiting symmetry. Our benchmarks suggest improved symmetry reduction in the presence of Johnson symmetry and comparable performance in the presence of row-column symmetry. Moreover, our implementation runs significantly faster, even though it identifies more diverse structures.

Figures (17)

• Figure 1: An illustration of the $\mathop{\mathrm{IR}}\nolimits$ process. Individualization steps break symmetries or similarities (nodes marked with a cross are individualized). Refinement steps propagate this information.
• Figure 2: Various group structures used throughout the paper. Colors indicate orbits of the group.
• Figure 3: An illustration of the Johnson group $\mathcal{J}_5$.
• Figure 4: Illustrations of different aspects of row symmetry.
• Figure 5: Illustrations of different aspects of row-column symmetry.

Theorems & Definitions (15)

• Lemma 2.1
• Definition 2.2: Tinhofer Graph DBLP:journals/cc/ArvindKRV17DBLP:journals/dam/Tinhofer91
• Remark 2.3
• Lemma 3.1
• proof
• Theorem 3.1
• proof
• Lemma 3.2
• proof
• Theorem 3.2