Satsuma: Structure-Based Symmetry Breaking in SAT

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., 2016) 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 provide benchmarks testing the effectiveness of our new implementation in conjunction with the state-of-the-art SAT solver Kissat. To this end, we compare satsuma, BreakID, and using no symmetry breaking. We find that satsuma successfully speeds up Kissat on last year’s SAT competition instances. Compared to BreakID, we observe significantly better breaking performance on instances with Johnson symmetry, and lower computational overhead across all tested families.