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.


2 Answers 2


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.

  • $\begingroup$ This has a lot more than $O(n)$ clauses. $\endgroup$
    – D.W.
    Commented Feb 3, 2020 at 3:59
  • $\begingroup$ Yes, but it's a polynomial reduction. $\endgroup$
    – Pseudonym
    Commented Feb 3, 2020 at 4:03
  • $\begingroup$ Absolutely, but the question specifies "with at most $O(n)$ clauses". $\endgroup$
    – D.W.
    Commented Feb 3, 2020 at 4:09
  • 1
    $\begingroup$ To which the answer is very likely to be "no" for a SAT reduction (although I have no proof at hand) because there aren't $O(n)$ edges/non-edges in general. But for 3SAT, the problem is simpler: there's a simple pigeonhole argument that if $|E| \approx \frac{|N|^2}{2}$ there is no reduction to 3SAT with $O(|N|)$ clauses. I'll leave that one as an exercise. $\endgroup$
    – Pseudonym
    Commented Feb 3, 2020 at 4:36
  • $\begingroup$ Hang on, let me rephrase. You can't encode the graph with that few 3SAT clauses. But, I guess you can encode the problem in the sense that you can "encode" a given HPP instance with "true"/"false" if you knew the answer. Still, I can't see a way around using $O(|N|^2)$ variables, which means you need $O(|N|^2)$ 3SAT clauses just to mention them all at least once. $\endgroup$
    – Pseudonym
    Commented Feb 3, 2020 at 5:00

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.