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.