CODEWITHSUNDEEP
algorithmgraphsat
csGeek
csGeek

Reputation: 43

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!

Upvotes: 2

Views: 1281

Answers (3)

Matt Timmermans
Matt Timmermans

Reputation: 59303

It probably wouldn't be too hard to come up with the kind of answer you're expecting, but here's the real answer instead:

"Reducing" a problem X to problem Y means transforming any instance of X to an instance of Y such that the answer to Y provides the answer to X. Usually, we require a P-time reduction, i.e., the transformation of the problem and the extraction of the answer must both happen in polynomial time.

Graph Reachability is easily solved in linear time, which is certainly polynomial time, so the reduction from Graph Reachability to SAT is very simple:

  1. Given a graph reachability problem, solve it in linear time;
  2. If the desired path exists, write out any satisfiable SAT instance, like (A). Otherwise, write out any unsatisfiable SAT instance like (A)&(~A)

Upvotes: 1

Jacob Soderlund
Jacob Soderlund

Reputation: 329

With respect to your first question: Since you're only devising a way to reduce a problem in P into a problem in NP (and not the other way around), this isn't actually a problem. You can turn any Graph Reachability problem into a SAT problem, but that doesn't mean you can turn any SAT problem into a Graph Reachability problem.

Upvotes: 0

CaptainTrunky
CaptainTrunky

Reputation: 1707

We did something similar to your task a few years ago. Our approach was based exactly on Floyd-Warshall (F.-W.) algorithm. Intuitively, you would like to something like this:

  1. Generate all possible paths using F.-W. for each pair of nodes
  2. Generate a clause representing each path. It could be described as "if a path is selected, then the following nodes must be selected"
  3. Generate a clause that unites all paths into a single CNF. Most likely it would be "exactly_one" clause.

A bit more formally:

  1. Assign a binary literal to each node in a graph. The literal has value True iff. it belongs to a path between two nodes.
  2. Run F.-W. for a pair of nodes
  3. Turn resulting path to a clause:
    nodes <- get_nodes_from_path(path)  
    node_lits <- logical_and([n.literal for n in nodes])
  1. Get new literal for a path path_lit <- get_new_literal()
  2. Add it to path a path: path_clause <- if_then_else(node_lits, path_lit)
  3. Go to 2, enumerate all pairs

Finally, you could the following:

all_paths <- exactly_one(all_path_clauses)
all_paths <- True

SAT solver would be forced to select one of paths and this would lead to selecting corresponding nodes.

Upvotes: 0

Related Questions