摘要

本文探讨了约束编程中对称性破缺的复杂性，特别是在SAT问题中的应用。对称性破缺谓词（SBPs）通常通过对变量施加顺序来选择每个赋值轨道中的字典序领导者（lex-leader）。尽管找到完整的lex-leader SBPs是NP难的，但实际中广泛使用不完整的lex-leader SBPs。本文的主要结果证明了高效计算SBPs的自然障碍：图非同构的有效认证。本文解释了在重要CP问题（如具有行-列对称性的矩阵模型和图生成问题）中获得短SBPs的困难性。即使允许引入额外变量，这些结果仍然成立。本文还展示了对于某些对称性群（如树的自同构群和具有高效SBPs的群的 wreath 积），可以获得多项式上界。

原理

本文通过研究对称性破缺谓词（SBPs）的计算复杂性，特别是在SAT问题中的应用，揭示了高效计算SBPs的自然障碍。SBPs通过对变量施加顺序来选择每个赋值轨道中的字典序领导者（lex-leader）。尽管找到完整的lex-leader SBPs是NP难的，但实际中广泛使用不完整的lex-leader SBPs。本文的主要结果证明了图非同构的有效认证是高效计算SBPs的自然障碍。此外，本文还展示了对于某些对称性群（如树的自同构群和具有高效SBPs的群的 wreath 积），可以获得多项式上界。这些结果不仅解释了在重要CP问题（如具有行-列对称性的矩阵模型和图生成问题）中获得短SBPs的困难性，还为对称性破缺的复杂性提供了深入的洞察。

流程

本文的工作流程主要包括以下几个关键步骤：

1. 问题定义：明确对称性破缺谓词（SBPs）在约束编程中的定义和应用背景，特别是在SAT问题中的应用。
2. 复杂性分析：分析计算完整lex-leader SBPs的复杂性，并指出尽管NP难，但实际中广泛使用不完整的lex-leader SBPs。
3. 主要结果证明：通过证明图非同构的有效认证是高效计算SBPs的自然障碍，解释了在重要CP问题中获得短SBPs的困难性。
4. 额外变量分析：即使允许引入额外变量，这些结果仍然成立，展示了在某些对称性群中可以获得多项式上界。
5. 应用前景：讨论了这些结果在实际中的应用前景，特别是在约束编程和图生成问题中的应用。

应用

本文的研究成果在约束编程和图生成问题中具有广泛的应用前景。对称性破缺谓词（SBPs）的有效计算可以帮助提高SAT求解器的性能，特别是在处理具有复杂对称性的问题时。此外，本文的结果还可以应用于其他领域，如组合优化和图论，以提高算法的效率和解决问题的能力。通过深入理解对称性破缺的复杂性，研究人员可以设计更有效的算法和策略，以应对实际问题中的对称性挑战。