Designing SAT for HCP

TL;DR

This paper presents a Boolean algebra-based SAT formulation for detecting Hamiltonian cycles in arbitrary graphs, linking satisfying assignments directly to Hamiltonian cycles, with potential exponential complexity.

Contribution

It introduces a novel SAT encoding for Hamiltonian cycle detection using Boolean algebra, directly relating solutions to graph cycles.

Findings

Boolean expression is true iff the graph has a Hamiltonian cycle

Each satisfying assignment corresponds to a Hamiltonian cycle

The Boolean expression may have exponential length in the worst case

Abstract

For arbitrary undirected graph $G$, we are designing SATISFIABILITY problem (SAT) for HCP, using tools of Boolean algebra only. The obtained SAT be the logic formulation of conditions for Hamiltonian cycle existence, and use $m$ Boolean variables, where $m$ is the number of graph edges. This Boolean expression is true if and only if an initial graph is Hamiltonian. That is, each satisfying assignment of the Boolean variables determines a Hamiltonian cycle of $G$, and each Hamiltonian cycle of $G$ corresponds to a satisfying assignment of the Boolean variables. In common case, the obtained Boolean expression may has an exponential length (the number of Boolean literals).