  For Boolean satisfiability problems, the structure of the solution space is
characterized by the solution graph, where the vertices are the solutions, and
two solutions are connected iff they differ in exactly one variable. For this
implicitly defined graph, we here study the st-connectivity and connectivity
problems.
  Building on the work of Gopalan et al. ("The Connectivity of Boolean
Satisfiability: Computational and Structural Dichotomies", 2006/2009), we first
investigate satisfiability problems given by CSPs, more exactly CNF(S)-formulas
with constants (as considered in Schaefer's famous 1978 dichotomy theorem); we
prove a computational dichotomy for the st-connectivity problem, asserting that
it is either solvable in polynomial time or PSPACE-complete, and an aligned
structural dichotomy, asserting that the maximal diameter of connected
components is either linear in the number of variables, or can be exponential;
further, we show a trichotomy for the connectivity problem, asserting that it
is either in P, coNP-complete, or PSPACE-complete.
  Next we investigate two important variants: CNF(S)-formulas without
constants, and partially quantified formulas; in both cases, we prove analogous
dichotomies for st-connectivity and the diameter; for for the connectivity
problem, we show a trichotomy in the case of quantified formulas, while in the
case of formulas without constants, we identify fragments of a possible
trichotomy.
  Finally, we consider the connectivity issues for B-formulas, which are
arbitrarily nested formulas built from some fixed set B of connectives, and for
B-circuits, which are Boolean circuits where the gates are from some finite set
B; we prove a common dichotomy for both connectivity problems and the diameter;
for partially quantified B-formulas, we show an analogous dichotomy.
