Counting satisfying solutions using planar bipartite double covers

🔲 This post is related to a paper of mine (Title: On the construction of graphs with a planar bipartite double cover from boolean formulas and its application to counting satisfying solutions) that will get published later this year in the Journal of Theoretical Computer Science. It is related to [this] blog post which i wrote already four years ago and settles some of its questions.

In a short overview, the paper adresses the following action chain:

1. Assume you have a boolean CNF formula $\Phi$
2. You build the incidence graph $\mathcal{I}$ of $\Phi$ using some techniques from the literature, e.g., each clause is represented by a node and also each variable is represented by a node. Then there is an edge between a clause-node and a variable-node if the variable occurs in that clause in $\Phi$.
3. You replace each node in $\mathcal{I}$ with a gadget, i.e., a small graph that has certain properties, which only have edge weights from 0 and 1. The properties of the gadgets ensure that the permanent of $\mathcal{G}$ contains #$\Phi$, as Valiant did in his paper.
4. You build the bipartite double cover $\mathcal{G}^{**}$ for which it holds that $$\text{PerfMatch}(\mathcal{G}^{**}) = \text{Permanent}(\textbf{A}_\mathcal{G})$$
5. If $\mathcal{G}^{**}$ is planar, then $\text{PerfMatch}(\mathcal{G}^{**})$ could be counted in polynomial time.

        //PerfMatch counts the number of Perfect Matchings of a graph

Sidenote: In [this] last blog post i talked about perfect matchings and setups which allow their efficient computation.

If you have an arbitrary CNF formula $\Phi$ and want to count its number of satisfying assignments, called #$\Phi$, then you are faced with a #$\text{P}$-complete problem that renders all of your approaches void. However, in some cases, there is hope. Either you can use Holographic Algorithms, which i explained [here], or test the action chain listed above. The first 4 steps from the list describe how to build a graph $\mathcal{G}$ and indeed those 4 steps are easy and can be done efficiently for any input formula $\Phi$. Point 5 is the crucial one.

The paper shows up, which requirements the gadgets from Step 3 have to have in order to allow a planar bipartite double cover in Step 5, provided the incidence graph $\mathcal{I}$ is already planar.
Note that this requirement (that $\mathcal{I}$ is planar) is not a restriction, since also $\text{Planar}$-$\text{3SAT}$ is already $\text{NP}$-$\text{complete}$ as shown by Lichtenstein [1], i.e., one could transform a formula $\Phi$ to a planar formula $\Phi$ without changing satisfyability.

The paper makes use of graphs that are outer planar or to be more precise $S$-outerplanar as we define in the paper.

Definition (S-outerplanar graph). Given a graph $\mathcal{G} = (V,E)$ with $S \subset V$ then $\mathcal{G}$ is $S$-outerplanar if:

1. $\mathcal{G}$ is planar
2. Each node $v \in S$ is on the boundary of the outer face

Whenever one wants to build a graph $\mathcal{G}$ such that the permanent of its adjacency matrix $\mathbf{M}_\mathcal{G}$ contains the number of solutions of a formula $\Phi$, one has to come up with a certain idea what kind of gadgets to use and what they are representing. Valiant in his famous paper [2] used three gadgets:

1. Variable gadget, for each variable in $\Phi$
2. Clause gadget, for each clause in $\Phi$
3. XOR gadget that connects a variable gadget to a clause gadget

His approach works for every 3CNF formula $\Phi$. To make the idea work, Valiant introduced a set of rules for the XOR gadget that have to do with the permanent values of minors obtained from the adjacency matrices of those gadgets. We asked our self:

Q: Can one substitute the gadgets (especially the XOR gadget) from Valiant such that the rules are preserved (or at least hold modulo some prime $p$) and concurrently that their bipartite double covers are planar?

We realized that the existence of such gadgets that would work over the integers $\mathbb{Z}$, would contradict well known complexity assumptions. However, reducing the rules modulo a prime number $p$ might work. Surprisingly, we found several XOR gadgets with the correct set of rules for e.g., $p = 5$, very easily. The nodes of the XOR gadget that have edges to the variable and clause gadgets are forming the set $S$. However, none of those gadgets had a $S$-outerplanar bipartite double cover. So we assumed, that there is a relationship between the set of rules and the $S$-outerplanarity of the bipartite double cover. And indeed we proved this relationship in the paper. I can not restate it here, but i can show a little example based on the following question:

"Can we use this to count solutions for at least some special formula classes like Holographic Algorithms are able to do?" 

Yes, we can. For example $\text{Pl}-2\text{CNF}$ can be counted with this approach in polynomial time (see example below). However, our approach probably works for other types of formula if you can find suitable an incidence graph representation. To illustrate our approach in the $\text{Pl}-2\text{CNF}$ case, let $\Phi$ be the following formula: $$ \Phi = (\overline{v_1} \vee v_2) \wedge (v_2 \vee v_3) \wedge (\overline{v}_3 \vee \overline{v}_4) \wedge (v_4 \wedge \overline{v}_1)$$

Graph $\mathcal{I}$

On the left you can see the incidence graph we chose for $\Phi$. Each node represents a clause and the nodes are connected if they share a variable.

For each type of 4 possible clauses (for simplicity we assume here that all clauses contain exactly two variables and all variables appear exactly twice) positive/positive; positive/negative; negative/positive; negative/negative we found a working gadget. So we can "redraw" the graph $\mathcal{I}$ by substituting each node with the appropriate gadget, which results into the graph $\mathcal{G}$ shown below on the left side. The gadgets are constructed such that if you build the total bipartite double cover (BDC) of $\mathcal{G}$ then this bipartite double cover graph (right side) is planar. 

Graph $\mathcal{G}$ (left) and the bipartite double cover of $\mathcal{G}$ (right)

It is well known that given a graph $\mathcal{G}$ and its adjacency matrix $\text{A}$, then 
$$\text{permanent(A)} = \text{NumberOfPerfectMatchings(BDC)}$$ Finally, since the number of perfect  matchings in a planar graphs can be counted in polynomial time using the FKT algorithm (see here), the number of solutions of the original formula $\Phi$ are also countable in polynomial time.

[1] D. Lichtenstein, Planar formulae and their uses, SIAM Journal of Computing, Volume 11, Issue 2, Pages. 329-343, 1982

[2] Leslie Valiant, The complexity of computing the permanent, Journal of Theoretical Computer Science, Volume 8, Issue 2, Pages 189-201, 1979, Elsevier