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.