Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Efficient SAT Techniques for Relative Encoding of Permutations with Constraints
verfasst von : Miroslav N. Velev, Ping Gao
Erschienen in: AI 2009: Advances in Artificial Intelligence
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present new techniques for relative SAT encoding of permutations with constraints, resulting in improved scalability compared to the previous approach by Prestwich, when applied to searching for Hamiltonian cycles. We observe that half of the ordering variables and two-thirds of the transitivity constraints can be eliminated. We exploit minimal enumeration of transitivity, based on 12 triangulation heuristics, and 11 heuristics for selecting the first node in the Hamiltonian cycle. We propose the use of inverse transitivity constraints. We achieve 3 orders of magnitude average speedup on satisfiable random graphs from the phase transition region, 2 orders of magnitude average speedup on unsatisfiable random graphs, and up to 4 orders of magnitude speedup on satisfiable structured graphs from the DIMACS graph coloring instances.