Sciweavers

Share
SARA
2009
Springer

Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles

10 years 4 months ago
Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles
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 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 possible 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— inst...
Miroslav N. Velev, Ping Gao 0002
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SARA
Authors Miroslav N. Velev, Ping Gao 0002
Comments (0)
books