# Boolean constraints for a connected component of a graph

Suppose I have an undirected graph $$G=(V,E)$$, and boolean variables $$x_v$$ (one for each vertex $$v \in V$$). These variables select a subset $$S \subseteq V$$ of vertices, namely the vertices $$S=\{v \mid x_v\}$$ whose corresponding boolean variable is true.

I want to express the constraint that $$S$$ is connected, i.e., that the vertices selected by the $$x_v$$'s form a connected component in $$G$$. How can I do that, in a way that can be used with a SAT solver or ILP solver?

Equivalently, this can be viewed as enforcing the constraint that all of the vertices in $$S$$ are reachable from each other, so this can be viewed as how to encode reachability constraints in SAT.

Here is one encoding. Introduce boolean variables $$x_{v,i}$$, with the intended meaning that $$x_{v,i}$$ is true if $$v$$ is selected and $$v$$ can by reached by a path of length $$\le i$$ from $$s$$ (where $$s$$ is some starting vertex).
You can force the $$x_{v,i}$$'s to have the desired meaning, by adding the following constraints:
• Exactly one of the $$x_{v,0}$$'s is true. For a SAT solver, this can be encoded using the methods in Encoding 1-out-of-n constraint for SAT solvers. An ILP solver can encode this directly.
• If $$x_{v,i}$$ is true, then $$x_{v,i+1}$$ is true. This can be enforced with the CNF clause $$\neg x_{v,i} \lor x_{v,i+1}$$ or the linear inequality $$x_{v,i} \le x_{v,i+1}$$.
• If $$x_{v,i+1}$$ is true, then there is a $$u$$ such that $$x_{u,i}$$ is true and either $$u=v$$ or $$u$$ is a neighbor of $$v$$. This can be enforced with the CNF clause $$\neg x_{v,i+1} \lor x_{v,i} \lor x_{u_1,i} \lor \cdots \lor x_{u_k,i}$$ where $$u_1,\dots,u_k$$ are the neighbors of $$v$$; or with the linear inequality $$x_{v,i+1} \le x_{v,i} + x_{u_1,i} + \dots + x_{u_k,i}$$.
• $$x_v = x_{v,n}$$ where $$n=|V|$$ is the number of vertices in the graph.