Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems.
Miroslav N. Velev, Ping Gao · 2010
We study portfolios of parallel strategies for Boolean Satisfiability (SAT) based solving of Hamiltonian Cycle Problems (HCPs). The strategies are based on our techniques for relative SAT encoding of permutations with constraints, and exploit: 1) encodings that eliminate half of the ordering Boolean variables and two-thirds of the transitivity constraints; 2) 12 triangulation heuristics for minimal enumeration of transitivity; 3) 11 heuristics for selecting the first node in the Hamiltonian cycle; 4) inverse transitivity constraints; and 5) exclusivity successor constraints between neighbors. We achieve up to 3 orders of magnitude speedup on random graphs that have Hamiltonian cycles and are in the phase transition region.