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!