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.

翻译：对称性破缺是增强约束规划求解器（如SAT或MIP求解器）的一种广泛流行的方法。对称性破缺谓词通常对变量施加顺序，并在每个赋值轨道中选出词典序领导者。尽管寻找完整的词典序领导者对称性破缺谓词是NP困难的，但不完整的词典序领导者对称性破缺谓词在实践中被广泛使用。本文研究了为SAT问题计算完整对称性破缺谓词（无论是词典序领导者还是其他类型）的复杂性。我们的主要结果证明了一个自然障碍：图非同构的高效可验证性。我们的结果解释了为何难以针对重要约束规划问题（如具有行列对称性的矩阵模型和图生成问题）获得简短对称性破缺谓词。即使允许对称性破缺谓词引入额外变量，我们的结论依然成立。我们展示了针对特定对称群（即树的自同构群以及具有高效对称性破缺谓词的群的环积）的多项式时间上界。