Hamiltonian Path NP-Hard Reduction, in depth: the 3-SAT row gadget, both proof directions, undirected and cycle variants, and a brute-force check

The problem and the proof obligation

The source problem is 3-SAT: a formula over variables x1..xn with k clauses, each an OR of three literals. The target is directed Hamiltonian path with fixed endpoints: given a directed graph G and vertices s and t, is there a path from s to t that visits every vertex exactly once? A reduction is a function f, computable in polynomial time, such that the formula is satisfiable exactly when f's output has such a path. Both directions of that equivalence need proof. The direction people forget is the converse: every Hamiltonian path, including strange ones you did not design for, must yield a satisfying assignment.

Membership in NP is the easy half: the path is a certificate checked in linear time. Hardness plus membership makes the problem NP-complete. Direction matters: mapping 3-SAT into Hamiltonian path proves the latter at least as hard; mapping the other way only shows a SAT solver can find Hamiltonian paths.

The construction

Each variable gets a row of 3k+1 nodes, numbered 0 to 3k. Clause j (counting from 0) owns the adjacent pair at positions 3j+1 and 3j+2, called L and R. The positions 3j, which sit between pairs and at both ends, are separators and touch no clause node. Consecutive row nodes are joined by edges in both directions, so a path can sweep a row left to right or right to left. Hubs h0..hn sit between rows: h0 is s, hn is t, and hub h(i-1) has edges to both ends of row i, and both ends have edges to hub hi. Each row is therefore a diamond: from its top hub you can sweep the row either way and arrive at the next hub.

Then add one node per clause. If clause j contains xi, add edges from row i's L to c_j and from c_j to row i's R: a detour usable only while sweeping left to right. If it contains not xi, reverse them: R to c_j to L, usable only while sweeping right to left. Left to right means true; right to left means false.

Counting gives n(3k+1) row nodes, n+1 hubs and k clause nodes, so n(3k+1)+(n+1)+k vertices in total. For clauses over three distinct variables there are 6nk+4n+6k edges: 6k per row inside it, 4 per row to and from the hubs, and 2 per literal. For 100 variables and 430 clauses that is 129,631 vertices and 260,980 edges: polynomial, which is all a reduction needs. Rows reserve a pair for every clause, even ones that do not mention the variable, which keeps the proof uniform at O(nk) size.

Satisfying assignment to path

Suppose an assignment satisfies the formula. Start at s. For each variable in order, sweep its row left to right if the variable is true and right to left if it is false, then continue to the next hub. This visits every hub and row node once. For each clause, pick one true literal; say it is xi. Row i is swept left to right, so when the path reaches that clause's L in row i, it detours L to c_j to R and carries on. A true not xi works the same way during a right-to-left sweep. Every clause node is visited exactly once, because you chose exactly one literal per clause, and the path ends at t.

Path to satisfying assignment

Now take any Hamiltonian path from s to t, and assume clauses use distinct variables (duplicates can be removed first). The key lemma is that every detour is normal: if the path enters c_j from row i, it leaves c_j back to row i.

Suppose not, for a positive literal: the path goes L to c_j to some w outside row i. Consider R. Its only possible predecessors are L, c_j and the separator S to its right, and its only possible successors are L and S. L's successor is c_j, and c_j's successor is w, so R must be entered from S. Then R must leave to L, giving the segment S, R, L, c_j, w. Now look at the separator P on L's left. It touches no clause node, and L is used up in both directions. If P is an interior separator, its only remaining neighbour is the node to its own left, which cannot be both its predecessor and its successor. If P is the row's first node, it must be h(i-1), P, hi. But then hub hi already has its predecessor. The row's last node can only be entered from its left neighbour or h(i-1), which has already left to P, and it can only leave to that same neighbour or hi, which is taken. That is a contradiction. The negative case is the mirror image. The separators are what make this argument work: without them, P could be another clause's L and escape through a clause node.

Once every detour is normal, replace each detour L, c_j, R with the direct row edge. What remains is a Hamiltonian path of the clause-free diamond graph, and the same local argument forces each row to be swept in a single direction between its hubs. Set xi true if row i is swept left to right. Each clause node was visited by a detour, and a detour's direction matches its row's sweep only when the literal it encodes is true, so every clause is satisfied.

The reduction as tested code

Proofs like this fail in small ways: a reversed edge, an off-by-one, a missing separator. So build the reduction as code and check it against brute force. The solver is backtracking that gives up once some unvisited vertex has no remaining way in or out.

import itertools

def build(n, clauses):
    """3-SAT over x1..xn (clauses are lists of signed ints) -> (adj, s, t)."""
    k, adj = len(clauses), {}
    def add(u, v):
        adj.setdefault(u, set()).add(v); adj.setdefault(v, set())
    for i in range(1, n + 1):
        last = 3 * k
        for p in range(last):
            add(("r", i, p), ("r", i, p + 1)); add(("r", i, p + 1), ("r", i, p))
        for end in (0, last):
            add(("h", i - 1), ("r", i, end)); add(("r", i, end), ("h", i))
    for j, clause in enumerate(clauses):
        L, R = 3 * j + 1, 3 * j + 2
        for lit in clause:
            i = abs(lit)
            a, b = (L, R) if lit > 0 else (R, L)
            add(("r", i, a), ("c", j)); add(("c", j), ("r", i, b))
    return adj, ("h", 0), ("h", n)

def ham_path(adj, s, t):
    pred = {v: set() for v in adj}
    for u in adj:
        for v in adj[u]:
            pred[v].add(u)
    path, seen = [s], {s}
    def dead(u):
        return any(v not in seen and (
            not any(w == u or w not in seen for w in pred[v]) or
            (v != t and not any(w not in seen for w in adj[v]))) for v in adj)
    def dfs(u):
        if len(path) == len(adj):
            return u == t
        if dead(u):
            return False
        for v in adj[u]:
            if v in seen or (v == t and len(path) != len(adj) - 1):
                continue
            seen.add(v); path.append(v)
            if dfs(v):
                return True
            seen.discard(v); path.pop()
        return False
    return list(path) if dfs(s) else None

def satisfiable(n, clauses):
    return any(all(any(bits[abs(l) - 1] == (l > 0) for l in c) for c in clauses)
               for bits in itertools.product([False, True], repeat=n))

def read_assignment(path, n, k):          # row swept left to right means true
    pos = {v: i for i, v in enumerate(path)}
    return [pos[("r", i, 0)] < pos[("r", i, 3 * k)] for i in range(1, n + 1)]

def check(n, clauses):
    path = ham_path(*build(n, clauses))
    assert (path is not None) == satisfiable(n, clauses)
    if path:
        a = read_assignment(path, n, len(clauses))
        assert all(any(a[abs(l) - 1] == (l > 0) for l in c) for c in clauses)

pool = sorted({tuple(sorted(c)) for c in itertools.product([1, -1, 2, -2], repeat=3)})
for k in (1, 2, 3):                        # 20 + 190 + 1,140 = 1,350 formulas
    for clauses in itertools.combinations(pool, k):
        check(2, [list(c) for c in clauses])

The test enumerates every two-variable formula of one to three clauses drawn from the 20 distinct literal triples: 1,350 formulas, 62 unsatisfiable. It compares satisfiability with path existence and decodes every path found back into an assignment. All assertions held, in under 2 seconds. 200 random three-variable formulas also agreed, but all were satisfiable, so only the unsatisfiable cases and the read-back test the backward direction.

Worked example

Take (x1 or not x2 or x3) and (not x1 or x2 or not x3). With n = 3 and k = 2, the graph has 27 vertices and 60 edges, as the formulas predict. The solver returns a path that sweeps all three rows left to right, so the assignment is x1 = x2 = x3 = true. It detours through c0 between positions 1 and 2 of row 1, since x1 satisfies the first clause, and through c1 between positions 4 and 5 of row 2, since x2 satisfies the second. Row 3 is swept straight through. Now take the unsatisfiable formula (x1 or x1 or x1) and (not x1 or not x1 or not x1). Its 11-vertex graph has no Hamiltonian path: c0 needs row 1 swept left to right and c1 needs it swept right to left, and a row is swept only once.

Undirected graphs, free endpoints and cycles

Directed to undirected. Replace each vertex v with three vertices v_in, v_mid and v_out joined in a chain, and turn each directed edge u to v into an undirected edge between u_out and v_in. Then ask for a path from s_in to t_out. The middle vertex has degree 2, so any Hamiltonian path must pass through each chain in one piece, and since in-ends meet only out-ends, every chain is crossed in the same direction. Without v_mid, a path could enter and leave a vertex's pair in ways no directed path allows. The split was checked on 41 small formulas (3 unsatisfiable) with 0 mismatches. The search took 219 seconds, though, against under 2 seconds for 1,350 directed instances, because the tripled, undirected graph gives the backtracker far more dead ends to explore.

Fixed endpoints to free endpoints. Add a new vertex adjacent only to s and another adjacent only to t. A vertex of degree 1 can only be an endpoint, so every Hamiltonian path of the new graph runs between the two new vertices through s and t.

Path to cycle. Add an edge from t back to s (or, in undirected graphs, one new vertex adjacent to both). A Hamiltonian cycle must use it, and removing it gives the path. The cycle problem then reduces to TSP by giving edges weight 1 and non-edges weight 2, as Karp reductions, in depth shows.

Easy special cases. Hardness is about general graphs. In a DAG, a Hamiltonian path exists exactly when the topological order is unique, which can be checked in linear time. Every tournament has a Hamiltonian path. Grid graphs and planar cubic graphs stay hard.

Failure modes

• Reducing the wrong way. Encoding Hamiltonian path as SAT proves nothing about hardness. The source must be the known-hard problem.
• Forgetting the converse. Showing that satisfying assignments give paths is half a proof. The detour lemma is the other half, and it is where separators earn their place.
• Edge direction for negative literals. Copying the positive gadget for negative literals breaks the backward direction. In the harness above, that bug gave all 62 unsatisfiable formulas a path, and 574 paths on satisfiable formulas decoded to assignments that fail; a test that only checks path existence on satisfiable input sees none of it.
• Only testing satisfiable inputs. Random 3-SAT formulas with few clauses per variable are almost always satisfiable. Enumerate small formulas so that unsatisfiable ones appear.
• Treating the reduced graph as a benchmark. Reduction outputs are deliberately structured and large. They prove a point; they are poor proxies for the graphs your users have.

What to do next

1. Run the code, then delete the separators (positions 3j) and see whether the 1,350-formula test still passes; explain any failure using the detour lemma.
2. Flip the edge direction for negative literals and confirm that both the unsatisfiable formulas and the witness read-back expose the bug.
3. Implement the in/mid/out split and the degree-1 endpoint trick, and test both on small formulas.
4. Rework the rows to give each variable pairs only for the clauses that contain it, and test whether the proof still holds.
5. If a production problem contains Hamiltonian path, compare backtracking with Held-Karp dynamic programming in TSP by dynamic programming on your real input sizes.