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.

The Permanent and planar graphs

Computational Complexity is a really fascinating area of research. One particular surprising fact that i learned years ago is the discrepancy between the computational effort to compute the determinant of a matrix and the permanent of a matrix. The determinant is defined as:
\begin{equation}
\text{det}(\text{A}) = \sum_{\sigma \in S_n}\text{sign}(\sigma)\prod^n_{i=1}a_{i,\sigma_i}
\end{equation} and the permanent is
\begin{equation}
\text{perm}(\text{A}) = \sum_{\sigma \in S_n}\prod^n_{i=1}a_{i,\sigma_i}
\end{equation} The difference in notation is minimal. The determinant considers the sign of the permutations $\sigma$ whereof the permanent does not. This little difference is responsible for the huge gap between the necessary resources that are needed in order to compute the actual value of these functions. The determinant can be evaluated in time that is polynomial in the dimension $n$, whereof the permanent is only computable in time that is exponential in $n$, e.g., using the $\mathcal{O}(n2^n)$ algorithm of Ryser. In the year 1979 Leslie Valiant [1,2] showed that the permanent is even #P-complete and he shows the same for any computation of $\text{perm}(\text{A}) \mod{p}$ for $p > 2$. To proof this, Valiant created a graph that encodes a boolean formula $f$. Due to his clever construction, the permanent of the graph's adjacency matrix is equal to the number of satisfying solution of the boolean formula $f$. It is a beutiful result and shows clearly that the computation of the permanent can probably not be done in an efficient way, i.e., polynomial in the matrix dimension. Note that if someone could compute the number of satisfying solutions of a formula $f$, such an algorithm can also be used to:

1. Decide if a given formula $f$ satisfiable, i.e. to solve the $\text{SAT}$ problem
2. If $f$ is satisfiable, to give a satisfying assignment of its variables. (Can be used to factorize integers)