Generating effective symmetry-breaking predicates for search problems

Generating effective symmetry-breaking predicates for search problems
复制标题

为搜索问题生成有效的对称破缺谓词

DOI:
10.1016/j.dam.2005.10.018
复制
发表时间:
2001
期刊:
Discret. Appl. Math.
影响因子:
--
通讯作者:
I. Shlyakhter
I. Shlyakhter
中科院分区:
--
文献类型:
--
作者:
I. Shlyakhter

文献摘要

被引文献

相似文献

考虑满足一定条件P的n结点图G的存在性检验问题,该问题表示为邻接矩阵M的n×n个布尔项之间的布尔约束,这个问题归结为P(M)的可满足性问题。如果P被同构保持,则P(M)是可满足的当且仅当P(M)∧SB(M)是可满足的,其中SB(M)是对称破坏谓词--由每个同构类中至少一个矩阵M满足的谓词。P(M)∧SB(M)比P(M)有更多的约束,因此回溯求解比P(M)快--特别是当SB(M)排除每个同构类中的大多数矩阵时。这种由Crawford等人提出的方法不仅适用于图,而且还适用于测试满足任何尊重同构的性质的组合对象的存在性,只要该性质可以被紧凑地指定为对对象的二进制表示的布尔约束。我们给出了几类组合对象的对称破坏谓词的生成方法:非循环有向图、置换、函数和任意关系(直积)。我们为对称破坏谓词定义了一个一致的最优性度量,并根据这个度量评估我们的约束。结果表明,对于各自的对象类别,这些约束要么是最优的,要么是接近最优的。
Consider the problem of testing for existence of an n-node graph G satisfying some condition P, expressed as a Boolean constraint among the n×n Boolean entries of the adjacency matrix M. This problem reduces to satisfiability of P(M). If P is preserved by isomorphism, P(M) is satisfiable iff P(M)∧SB(M) is satisfiable, where SB(M) is a symmetry-breaking predicate—a predicate satisfied by at least one matrix M in each isomorphism class. P(M)∧SB(M) is more constrained than P(M), so it is solved faster by backtracking than P(M)—especially if SB(M) rules out most matrices in each isomorphism class. This method, proposed by Crawford et al., applies not just to graphs but to testing existence of a combinatorial object satisfying any property that respects isomorphism, as long as the property can be compactly specified as a Boolean constraint on the object's binary representation. We present methods for generating symmetry-breaking predicates for several classes of combinatorial objects: acyclic digraphs, permutations, functions, and arbitrary-arity relations (direct products). We define a uniform optimality measure for symmetry-breaking predicates, and evaluate our constraints according to this measure. Results indicate that these constraints are either optimal or near-optimal for their respective classes of objects.