Reducing Graph Reachability to SAT (CNF) So I came across this problem in my textbook. I was wondering how to develop a reduction from the Graph Reachability problem to SAT (CNF) problem. (i.e. formula is satisfiable iff there exists a path in graph G from start to end node)

1) I can't wrap my head around how to go from something that can be solved in polynomial time (Graph Reachability) to something that is NP (SAT).

2) I can't seem to find a way to formulate these nodes/edges of Graph into actual clauses in CNF that correspond to reachability.

I tried to think about algorithms like Floyd-Warshall that determine if a path exists from start to end node but I can't seem to formulate that idea into actual CNF clauses. Help would be much appreciated!
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.