What are some good algorithms to have a SAT (CNF) solver determine if a given graph is fully-connected or disjoint?
The best one I can think of is this:
- Number the nodes 1..N, where N is the number of nodes in the graph.
- define N^2 variables with the ordered pair (P, Q), where P = 1..N and Q = 0..N-1.
- Set (1,0) to true.
- Set (A,P+1) to true iff there is an edge connecting node A and node B and (B,P) is true.
- If there exists a true (X,Y) variable for all possible nodes X, then the graph is connected.
Effectively, (X,Y) means "Node X is Y steps away from node X".
This seems inefficient at O(N^2) variables. Can this be improved?
A comment (from when I posted this on cstheory.stackexchange.com) asked why I would need a SAT-based algorithm when O(N) algorithms for connectivity are well-known. The reason is simple -- I have many other SAT-based constraints on the graph that also need to be satisfied at the same time.