The solution graph of a Boolean formula on n variables is the subgraph of the hypercube Hn induced by the satisfying assignments of the formula. The structure of solution graphs has been the object of much research in recent years since it is important for the performance of SAT-solving procedures based on local search. Several authors have studied connectivity problems in such graphs focusing on how the structure of the original formula might affect the complexity of the connectivity problems in the solution graph [Gopalan2009,Schwerdtfeger2013].

In this paper we study the complexity of the isomorphism problem of solution graphs of Boolean formulas. We investigate how this complexity depends on the formula type, considering for this the classes of formulas introduced in [Gopalan2009,Schwerdtfeger2013].

We show that for general formulas the solution graph isomorphism problem can be solved in exponential time while in the cases of 2CNF formulas as well as for CPSS formulas, the problem is in the counting complexity class C = P , a subclass of PSPACE. We also prove a strong property on the structure of solution graphs of Horn formulas showing that they are just unions of partial cubes.

In addition we give a PSPACE lower bound for the problem on general Boolean functions. We use a recent result on the complexity of testing the number of perfect matchings Curticapean2015 to prove that for 2CNF as well as for CPSS formulas the solution graph isomorphism problem is hard for C = P under polynomial time many one reductions, thus matching the given upper bound.