Quasi-linear reduction of Hamiltonian Cycle Problem (HCP) to Satisfiability Problem (SAT)
Publication Date: 2014-Jun-04
The IP.com Prior Art Database
This paper shows a way of converting any Hamiltonian Cycle problem (HCP) with n vertices and m directed edges to a Boolean Satisfiability problem (SAT) problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses. It uses vertex numbering using a linear feedback shift register (LFSR) sequence together with variables identifying active edges, and simple algebraic constraints between a vertex number and its successors' vertex number based on active edges. By adding redundant constraints on the edges a SAT solver can now solve HCP problems with 500 to 1000 vertices.