Logic - Rearranging CNF formula Given a #2SAT problem such as


*

*how many ways can $(a \vee b) \wedge (\bar{a} \vee d) \wedge (\bar{b} \vee c) \wedge (\bar{c} \vee d)$ be satisfied?


I am trying to find a way to rearrange the clauses into collections of independent clauses. For this particular example, a desirable rearrangement would look like
$\big((a \vee b) \wedge (\bar{c} \vee d)\big) \wedge \big((\bar{b} \vee c) \wedge (\bar{a} \vee d)\big)$
since each of the two groupings contain each literal only once. My aim is to separate out the clauses in this way so that there are as a few groupings as possible. The example began with 4 groupings of 1 clause, the rearrangement has 2 groupings of 2 clauses.
A lower bound for the number of groupings is the number of times a literal appears. In this example, each literal appears twice so the number of groupings is at least 2.
My first thought was to represent each clause as a vertex of a graph and draw an edge between each pair of clauses that could be paired together. I would then search for the largest clique, then the next largest and so on. But this appears to be an NP-complete problem. 
I am trying to find polynomial-time tools to perform this rearrangement. 
Any help or direction is appreciated.
 A: Your problem is pretty "inherently" NP-Complete. You are trying to solve a graph coloring problem.
As you described, imagine your graph with clauses as vertices, and clauses that share variables have an edge. Suppose you have a solution with m groupings. Then take m colors, and color each vertex with the number based on which grouping that vertex is in. It will give you an m-coloring of the graph.
Asking if your problem can be solved in m groupings is equivalent to asking if there is an m coloring of the graph. Finding minimal colorings of graphs is NP-Complete.
Technically, this doesn't prove that your problem is NP-Complete, because not every graph will arise from a #2SAT problem. (The graphs you are getting are precisely the set of induced subgraphs of a "grid graph", that is, the conormal product of complete graphs.) But it is very strong evidence that your problem is NP-Complete.
For a solution to your problem, I would download some graph coloring software. Think carefully about whether you need the true optimum or just a decent approximation.
