Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT 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.
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.