超越Lex-Leader的对称性破坏复杂度

对称性破坏是约束编程中（如SAT或MIP求解器）提高性能的流行方法。对称性破坏谓词（SBPs）通常对变量施加顺序，在每个赋值轨道中确定字典领导者（lex-leader）。虽然找到完整的lex-leader SBPs是NP难的，但不完整的lex-leader SBPs在实际中广泛使用。本文我们研究了计算SAT的完整SBPs复杂度。我们的主要结果证明了一个自然的障碍：高效认证图非同构性。我们的结果解释了为重要的CP问题（如具有行列对称性的矩阵模型和图生成问题）获得简短SBPs的困难。即使允许SBPs引入额外变量，我们的结论也成立。我们展示了对于某些对称群（如树的自同构群和群与其他群的乘积的高效SBPs），存在多项式上界。