利用SAT中的同构子图（长版）
Exploiting Isomorphic Subgraphs in SAT (Long version)
摘要：
虽然静态对称破缺在SAT社区已经探索了几十年，但直到2010年，研究才集中在动态地利用相同的对称性，在SAT求解器运行期间，通过学习额外的子句。这两种方法是不同的，不兼容。前者修剪解决方案，而后者不修剪-它只修剪没有解决方案的搜索区域，如标准冲突条款。然而，这两种方法都需要我们称之为\emph{full symmetry}的东西，即文字之间的命题一致的映射$σ$，使得$σ(φ) \equiv φ$，其中$\equiv$表示句法等价模子句排序和子句内的文字排序。在这篇文章中，我们表明，这样的完全对称性是不是一个必要条件，增加额外的条款：同构之间的可能重叠的子图的着色关联图是充分的。虽然找到这样的子图是一个计算困难的问题，但在许多情况下，通过分析CNF所源自的问题的高级结构，可以检测到它们。我们证明了这一原则与几个著名的问题，包括范德瓦尔登数，有界模型检验和布尔毕达哥拉斯三元组。
英文摘要：
While static symmetry breaking has been explored in the SAT community for decades, only as of 2010 research has focused on exploiting the same discovered symmetry dynamically, during the run of the SAT solver, by learning extra clauses. The two methods are distinct and not compatible. The former prunes solutions, whereas the latter does not -- it only prunes areas of the search that do not have solutions, like standard conflict clauses. Both approaches, however, require what we call \emph{full symmetry}, namely a propositionally-consistent mapping $σ$ between the literals, such that $σ(φ) \equiv φ$, where here $\equiv$ means syntactic equivalence modulo clause ordering and literal ordering within the clauses. In this article we show that such full symmetry is not a necessary condition for adding extra clauses: isomorphism between possibly-overlapping subgraphs of the colored incidence graph is sufficient. While finding such subgraphs is a computationally hard problem, there are many cases in which they can be detected a priory by analyzing the high-level structure of the problem from which the CNF was derived. We demonstrate this principle with several well-known problems, including Van der Waerden numbers, bounded model checking and Boolean Pythagorean triples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
