5
$\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.

|cite|improve this question
$\endgroup$
  • $\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$ – Yuval Filmus Jul 2 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$ – David Richerby Jul 2 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$ – Peter Taylor Jul 2 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 at 22:21
7
$\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}$.
|cite|improve this answer
$\endgroup$
  • $\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$ – Emil Jeřábek Jul 2 at 16:13
  • $\begingroup$ Thanks for the correction! $\endgroup$ – Yuval Filmus Jul 2 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 at 20:33
  • $\begingroup$ Thanks, corrected. $\endgroup$ – Yuval Filmus Jul 2 at 20:35

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.