CONN-SAT is the problem of deciding whether a subgraph of a Hamming cube is connected or not, where the subgraph is induced by a set of satisfying assignments of Boolean formulas. As the complexity of SAT varies according to types of formulas (Horn SAT, XOR SAT, 2SAT, 3SAT etc.), the complexity of CONN-SAT is classified by such types. In this talk, I will give an overview on the classification of the complexity of CONN-SAT. I also mention an exponential time algorithm for CONN-SAT where formulas are k-CNFs (the problem is PSPACE-complete). This is a joint work with Kazuhisa Makino and Masaki Yamamoto.