Reducing Graph Reachability to SAT (CNF)
Maybe the solution is to use the 2-SAT problem which does have a polynomial solution.

For a 2-SAT problem, you can indeed build an implication graph. Basically a clause $(a \vee b)$ leads to the implications $\neg a \implies b$ and $\neg b \implies a$. The problem is satisfiable if there is no variable $x$ such that $x$ and $\neg x$ are in the same SCC of the implication graph. Being in same SCC is equivalent to double reachability:


it exists a path from $x$ to $\neg x$
it exists a path from $\neg x$ to $x$


So for any skew-symmetric (required property) graph, you can build a 2-SAT problem for which it is the implication graph.