7
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$ Jul 2 '19 at 8:49
  • $\begingroup$ 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. $\endgroup$ Jul 2 '19 at 9:42
  • $\begingroup$ The justification of the last paragraph only makes sense if the graph is not fixed, but that contradicts the first paragraph. Please clarify. $\endgroup$ Jul 2 '19 at 21:22
  • $\begingroup$ For the application I'm asking this question for, the structure of the graph changes based on other constraints in the SAT. $\endgroup$
    – onigame
    Jul 3 '19 at 22:21
9
+100
$\begingroup$

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}$.
$\endgroup$
4
  • $\begingroup$ 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$. $\endgroup$ Jul 2 '19 at 16:13
  • $\begingroup$ Thanks for the correction! $\endgroup$ Jul 2 '19 at 16:15
  • $\begingroup$ For the first instance, the third bullet point should have $x_v$ instead of $x_{v_0}$, right? $\endgroup$
    – onigame
    Jul 2 '19 at 20:33
  • $\begingroup$ Thanks, corrected. $\endgroup$ Jul 2 '19 at 20:35
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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