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.


1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.