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.

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}$.

StackExchange Computer Science Q#111410, answer score: 9