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...

• Type: Conference
• Year: 2009
• Where: SARA
• Authors: Miroslav N. Velev, Ping Gao 0002
• Keywords: Artificial Intelligence, Combinatorial Problems, Hamiltonian Cycle, Hamiltonian Cycle Problem, SARA 2009