# SAT algorithm for determining if a graph is disjoint

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.

• Do you want a SAT instance which is satisfiable iff the graph is connected, or one which is satisfiable iff the graph is not connected? Jul 2, 2019 at 8:49
• OK but still, why don't you use a linear-time connectivity algorithm independently of your SAT constraints? Just because you have a hammer, that doesn't mean that all your problems are nails. Jul 2, 2019 at 9:42
• The justification of the last paragraph only makes sense if the graph is not fixed, but that contradicts the first paragraph. Please clarify. Jul 2, 2019 at 21:22
• For the application I'm asking this question for, the structure of the graph changes based on other constraints in the SAT. Jul 3, 2019 at 22:21

Given a graph $$G = (V,E)$$, here is a SAT instance which is satisfiable iff the graph is not connected.

Pick an arbitrary vertex $$v_0 \in V$$, and add the following clauses, over the variables $$x_v$$ for $$v \in V$$:

• $$x_{v_0}$$.
• For every $$(u,v) \in E$$, $$\lnot x_u \lor x_v$$ and $$\lnot x_v \lor x_u$$.
• $$\bigvee_{v \neq v_0} \lnot x_v$$.

Here is a SAT instance which is satisfiable iff the graph is connected.

Pick an arbitrary vertex $$v_0 \in V$$, and add the following clauses, over the variables $$x_{v,i}$$ for $$v \in V$$ and $$i \in \{0,\ldots,n-1\}$$:

• $$\lnot x_{v,0}$$ for all $$v \neq v_0$$.
• For every vertex $$v \in V$$ and $$i \in \{0,\ldots,n-2\}$$, $$\lnot x_{v,i+1} \lor x_{v,i} \lor \bigvee_{u\colon (u,v) \in E} x_{u,i}$$.
• For every vertex $$v \in V$$, $$x_{v,n-1}$$.
• The second CNF is always trivially satisfiable. You need to replace $x_{v_0,0}$ with the clauses $\neg x_{v,0}$ for all $v\ne v_0$. Jul 2, 2019 at 16:13
• Thanks for the correction! Jul 2, 2019 at 16:15
• For the first instance, the third bullet point should have $x_v$ instead of $x_{v_0}$, right? Jul 2, 2019 at 20:33
• Thanks, corrected. Jul 2, 2019 at 20:35

Yuval describes a boolean CNF formula that is satisfiable iff the graph is not connected, using $$|V|$$ variables; and a boolean CNF formula that is satisfiable iff the graph is connected, using $$|V|^2$$ variables.

I describe here a boolean CNF formula that is satisfiable iff the graph is connected, using $$O(|V| \lg |V| + |E|)$$ variables. If $$|V|$$ is large enough and the graph is sparse, this is better than Yuval's solution.

Introduce variables $$d_v$$, one for each vertex $$v \in V$$, over the domain $$d_v \in \{0,1,\dots,|V|-1\}$$, and variables $$y_{u,v}$$, one for each edge $$(u,v) \in E$$. Add the following constraints:

• $$d_{v_0} = 0$$
• $$d_v \le d_u + 1$$ for each $$(u,v) \in E$$
• for each $$v$$, there exists $$u$$ such that $$(u,v) \in E$$ and $$y_{u,v}$$
• $$y_{u,v} \implies d_v = d_u + 1$$

Here the intended interpretation of $$d_v$$ is that it captures the distance (length of the shortest path) from $$v_0$$ to $$v$$; and the intended interpretation of $$y_{u,v}$$ is that it should be true if the edge $$(u,v)$$ is part of a shortest path $$v_0 \leadsto v$$. Note that this system of constraints has a satisfying assignment iff the graph is connected.

Now you can convert this to SAT using "bit-blasting". In particular, for each $$d_v$$, introduce variables $$x_{v,i}$$ for $$i=0,1,\dots,\lceil \lg |V| \rceil -1$$; the intended meaning is that $$x_{v,i}$$ is the $$i$$th bit of $$d_v$$. Now we can express the constraint $$d_v \le d_u+1$$ using $$O(\lg |V|)$$ additional variables and clauses (e.g., by building a circuit for this comparison and using Tseitin's transform). Also, we can express the constraint "for each $$v$$, there exists $$u$$ such that..." using $$|V|$$ clauses, one for each $$v$$, each of which is a disjunction over the appropriate set of $$u$$. In this way, we obtain a set of CNF clauses that uses $$O(|V| \lg |V|)$$ variables for the bit-blasting of the $$d$$'s, and $$|E|$$ variables for the $$y$$'s. This yields a CNF formula as claimed above.