Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles
Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles
复制标题
用于排列问题绝对编码的高效 SAT 技术：在哈密顿循环中的应用
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Ping Gao
中科院分区：
文献类型：
--
作者：
M. Velev;Ping Gao
我们研究了通过翻译到布尔的满意度来解决硬组合问题的新方法（SAT）。 HCP），这些约束是置换中的两个相邻节点也应该是原始图中的邻居绝对的SAT编码置换量，其中n个对象中的每个对象中的每个对象中的每个位置都定义了谓词以指示该对象是否放置在该位置中。与以前已使用的对数编码，我们探索416个实例化的16个层次参数化编码。列举置换中的节点的可能邻居，而不是排除不可能的邻居的排他性邻接约束，并且以前已应用了11个启发式方法。以及静态CNF变量排序的8个启发式方法。相对于先前使用的用于通过SAT求解HCP的编码，因此加速随图形的大小而增加。
We study novel approaches for solving of hard combinatorial problems by translation to Boolean Satisfiability (SAT). Our focus is on combinatorial problems that can be represented as a permutation of n objects, subject to additional constraints. In the case of the Hamiltonian Cycle Problem (HCP), these constraints are that two adjacent nodes in a permutation should also be neighbors in the original graph for which we search for a Hamiltonian cycle. We use the absolute SAT encoding of permutations, where for each of the n objects and each of its pos- sible positions in a permutation, a predicate is defined to indicate whether the object is placed in that position. For implementation of this predicate, we compare the direct and logarithmic encodings that have been used previously, against 16 hierarchical parameterizable encodings of which we explore 416 instantiations. We propose the use of enumerative adjacency constraints—that enumerate the possible neighbors of a node in a permutation — instead of, or in addition to the exclusivity adjacency constraints — that exclude impossible neighbors, and that have been applied previously. We study 11 heuristics for efficiently choosing the first node in the Hamiltonian cycle, as well as 8 heuristics for static CNF variable ordering. We achieve at least 4 orders of magnitude average speedup on HCP benchmarks from the phase transition region, relative to the previously used encodings for solving of HCPs via SAT, such that the speedup is increasing with the size of the graphs.