Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT

Question

Is there a polynomial-time reduction from Directed Hamiltonian Path Problem to 3SAT which is linear in the number of vertices? That is, it reduces every directed graph $G$ with $n$ vertices to a formula $\varphi$ with at most $O(n)$ clauses within time at most $p(n)$ for some polynomial $p(n)$?

Since Cook Levin Theorem shows a reduction that proves 3SAT is NPC, almost all of the literature deals only with reductions from 3SAT, and only rarely one can find in the literature reductions to 3SAT.

After searching the web I found this and other cites that have the other direction of reduction (from 3SAT to dHamPath).

Referring to some source would be highly appreciated.

Answer 1

I don't know of a reference, but there's a standard reduction from Hamiltonian paths/cycles to SAT which is fairly well-known. The reduction from SAT to 3SAT is then done by introducing additional variables to break up clauses, e.g.:

$$v_1 \vee \neg v_2 \vee v_3 \vee \neg v_4 \Rightarrow \left( v_1 \vee \neg v_2 \vee X\right) \wedge \left( v_3 \vee \neg v_4 \vee \neg X\right)$$

Let $n$ be the number of nodes in the graph. Then define variables $x_{i,j}$ where $i,j \in \left\{1 \ldots n\right\}$, where $x_{i,j}$ is true if node $i$ appears in position $j$ in the Hamiltonian path.

Every node must appear somewhere on the path:

$$\bigwedge_{i} \left( \bigvee_{j} x_{i,j}\right)$$

Every position in the path must be occupied:

$$\bigwedge_{i} \left( \bigvee_{j} x_{j,i}\right)$$

No node appears on the path more than once:

$$\bigwedge_{i} \bigwedge_{j \ne k} \left( \neg x_{i,j} \vee \neg x_{i,k} \right)$$

No two distinct nodes occupy the same position:

$$\bigwedge_{i} \bigwedge_{j \ne k} \left( \neg x_{j,i} \vee \neg x_{k,i} \right)$$

Nonadjacent nodes cannot be adjacent on the path. If $E \subseteq N \times N$ is the set of edges:

$$\bigwedge_{k \ne \left|N\right|}\bigwedge_{(i,j) \not\in E} \left( \neg x_{k,i} \vee \neg x_{k+1,j}\right)$$

You can modify this in the obvious way if you're trying to find a Hamiltonian cycle.

On that, as a practical matter, if you are trying to find a Hamiltonian cycle and you intend to feed this to a SAT solver, you would normally assert a start node as another clause, e.g. $x_{1,1}$, to reduce the search space. Obviously for Hamiltonian paths, you don't do that.

Answer 2

This paper: Linearly-growing Reductions of Karp's 21 NP-complete Problems does not show any linear reductions, but references my quasi-linear reduction of Hamiltonian Cycle to SAT, and SAT to 3-SAT has a linear reduction.

My reduction reduces a 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. The reductions from Hamiltonian path to undirected Hamiltonian cycle and from undirected Hamiltonian cycle to directed Hamiltonian cycle are linear.

Some other techniques are discussed here: In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem including using a binary adder sequence numbering.

Filar, J., Haythorpe, M., & Taylor, R. (2018). Linearly-growing reductions of Karp's 21 NP-complete problems. Numerical Algebra, Control and Optimization, 8(1), 1-16

A. Johnson. Quasi-Linear Reduction of Hamiltonian Cycle Problem (HCP) to Satisfiability Problem (SAT), IP.com, Disclosure Number: IPCOM000237123D, 2014

Zhou, N. F. (2020, September). In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem. In International Conference on Principles and Practice of Constraint Programming (pp. 585-602). Springer, Cham.