In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem

Abstract

SAT solvers have achieved remarkable successes in solving various combinatorial problems. Nevertheless, it remains a challenge to find an efficient SAT encoding for the Hamiltonian Cycle Problem (HCP), which is one of the most well-known NP-complete problems. A central issue in encoding HCP into SAT is how to prevent sub-cycles, and one well-used technique is to map vertices to different positions. The HCP can be modeled as a single-agent path-finding problem. If the agent occupies vertex i at time t, and occupies vertex j at time, then vertex j’s position must be the successor of vertex i’s. This paper compares three encodings for the successor function, namely, a unary encoding that uses a Boolean variable for each vertex-time pair, an optimized binary adder encoding that uses a special incrementor with no carry variables, and a LFSR encoding that uses a linear-feedback-shift register. This paper also proposes a preprocessing technique that rules out a position from consideration for a vertex and a time if the agent cannot occupy the vertex at the time. Our study has surprisingly revealed that, with optimization and preprocessing, the binary adder encoding is a clear winner: it solved some instances of the knight’s tour problem that had been beyond reach for eager encoding approaches, and performed the best on the HCP instances used in the 2019 XCSP competition.