I was wondering, how could I define a propositional formula $\varphi_{G, H}$, which, given two finite graphs $G$ and $H$, is satisfiable exactly if theres a graph homomorphism from $G$ to $H$.
A graph homomorphism is defined like this:
$h : V(G) \to V (H)$
$\{u, v\} \in E(G) \to \{h(u), h(v)\} \in E(H)$
Well, what I said in the comment was not precise.
It is unknown, if for every two graphs $G,H$ CNF formula $\varphi_{G,H}$ with polynomial length in $G,H$, such that:
there is some isomorphism from $G$ to $H\iff\varphi_{G,H}$ is satisfiable. This is conjectured to be false.
As for your question, for graph homomorphism, this is possible, since deciding if two graphs are homomorphic, is an NP-Complete problem.
See Lectures note by Reinhard Pichler page 28, for the reduction to $3\text{-SAT}$ problem.