satsuma: Structure-based Symmetry Breaking in SAT

TL;DR

Satsuma introduces a new symmetry breaking tool for SAT solving that detects diverse symmetry structures more efficiently, leading to improved reduction and faster performance compared to existing methods.

Contribution

The paper presents satsuma, a novel symmetry breaking tool that detects multiple symmetry types with new algorithms, enhancing reduction and efficiency over prior approaches like BreakID.

Findings

Improved symmetry reduction with Johnson symmetry.

Comparable performance with row-column symmetry.

Faster runtime despite identifying more 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.