The Complexity of Symmetry Breaking Beyond Lex-Leader

TL;DR

This paper investigates the computational complexity of constructing complete symmetry breaking predicates (SBPs) for SAT under given permutation groups. It shows a fundamental barrier: efficient complete SBPs for key symmetry classes (notably row-column and Johnson actions) would imply $\,\mathrm{GI} \in \mathrm{coNP}$, tying SBP feasibility to graph non-isomorphism. It also provides constructive upper bounds, including a quasi-polynomial upper bound via Babai’s graph isomorphism algorithm and polynomial-size SBPs for automorphism groups of trees and certain wreath products. The results delineate hard vs. easy cases, explain why compact SBPs are elusive for matrix models, and offer principled paths to design SBPs for structured symmetries, guiding both theory and practice in SBP development.

Abstract

Symmetry breaking is a widely popular approach to enhance solvers in constraint programming, such as those for SAT or MIP. Symmetry breaking predicates (SBPs) typically impose an order on variables and single out the lexicographic leader (lex-leader) in each orbit of assignments. Although it is NP-hard to find complete lex-leader SBPs, incomplete lex-leader SBPs are widely used in practice. In this paper, we investigate the complexity of computing complete SBPs, lex-leader or otherwise, for SAT. Our main result proves a natural barrier for efficiently computing SBPs: efficient certification of graph non-isomorphism. Our results explain the difficulty of obtaining short SBPs for important CP problems, such as matrix-models with row-column symmetries and graph generation problems. Our results hold even when SBPs are allowed to introduce additional variables. We show polynomial upper bounds for breaking certain symmetry groups, namely automorphism groups of trees and wreath products of groups with efficient SBPs.

Figures (1)

• Figure 1: Complexity of computing symmetry breaking predicates for the stated families of groups in SAT. All groups can be handled in quasi-polynomial time using a circuit. The symbol $G$ refers to the permutation group of consideration. The parameter $n$ refers to the domain size of the permutation group, or, the number of variables of the formula. For "easy" families of groups, a CNF predicate can be computed in polynomial time. For "hard" families of groups, the existence of polynomial time symmetry breaking, even allowing the use of additional variables, implies that is in . Blue outlines indicate novel results proven in this paper.

Theorems & Definitions (32)

• Theorem 1.0
• Theorem 1.0
• Theorem 1.0
• Theorem 1.0
• Theorem 1.0
• Lemma 3.1
• proof
• proof : Proof of Theorem \ref{['thm:core']}
• Lemma 3.3
• proof