通过拉姆齐型问题探索 Shatter 在 AllSAT 中的应用

在 SAT 求解器的背景下，Shatter 是一种用于 CNF 公式对称性破缺的流行工具。然而，关于其在 AllSAT 问题（即列出布尔公式所有模型的问题）中使用的讨论很少。AllSAT 由于其在模型检测、数据挖掘等领域的众多应用，近年来广受欢迎。AllSAT 对计算机科学其他领域一个特别直观的应用例子是计算拉姆齐理论。在本文中，我们研究了将 Shatter 纳入使用布尔公式生成避免指定单色子图的所有可能图边着色的工作流中的效果。生成完整的着色集是计算拉姆齐理论中的重要构建块。我们指出了将 Shatter 朴素地用于打破编码图拉姆齐型问题的布尔公式对称性时的两个缺陷：模型数量的“膨胀”和不完整着色集的生成。本工作中提出的问题并非意在阻止将 Shatter 用作组合计算中 AllSAT 问题的预处理工具，而是通过避免这些潜在陷阱来帮助研究人员正确使用该工具。为此，我们提供了应对使用 Shatter 处理 AllSAT 负面效应的策略和附加工具。尽管本文涉及的具体应用是拉姆齐型问题，但我们进行的分析适用于许多其他出现高度对称布尔公式且希望找到其所有模型的领域。