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.

Holographic Algorithms

This post shows an introduction to Holographic Algorithms (HA). From my point of view, Holographic Algorithms were motivated by analogies to quantum computing and to overcome some of the obstacles that occur when one follows Leslie Valiant's original approach using the permanent and cyclic covers to count satisfying solutions for boolean formulas.

Again, the basic ingredient for HAs is the efficiently computable FKT-algorithm, which works because of the grateful fact that we are able to compute the determinant in polynomial time.

The literature of Holographic Algorithms (which are a generalization of CSP-Problems) is huge and is dominated by works of Valiant, Cai and Lu, see e.g. [1,2,3]. The central theorem is the Holant Theorem, which proofs the equality of the number of perfect matchings of a graph $\mathcal{G}$ and the value of the Holant Function. The Holant Function is applied to a matchgrid, that is a graph composed of certain subgraphs (called matchgates), such that the total graph (the matchgrid) is the graph $\mathcal{G}$ and its structure incorporates a combinatorial function.
The matchgrid $\Omega$ can be seen as a bipartite graph whereof the matchgates are the vertices. For the application to count satisfying assignments, we are always faced with bipartite graphs: on the left are the variable nodes and on the right the clause nodes. 
The Holant Function can be understood as a function that measures or counts particles that flow along the lines of the bipartite graph from the left nodes to the right nodes, i.e., from the variables to the clauses.

For HA two types of mathgates are sufficient: Generators and Recognizer. The generator generates patterns of particles along its output lines and the recognizer recognizes these patterns. Matchgates, i.e., generators and recognizers, are little graphs with only output and input nodes respectively.

In Figure 1, you see a simple generator, which is the box on the left denoted as A. It is just a small graph that connects two nodes and has one edge of weight 1. The two nodes are also the output nodes (thats why they are drawn of the outerface of the matchgate). Normally, there are more inner nodes.

Figure 1 - A generator and its signature configurations

An implementation of the FKT-algorithm

This post is dedicated to give you an implementation (in SAGE) of the FKT-algorithm. I coded this while spending some time on the ideas i explained in this blog post. I searched several hours to find an existing implementation without success. Since it took me a while to code this on my own, i think it is worth to present it, therewith other can use it in their own work. It works well, but if you find an error, please leave a note.

The FKT-algorithm can be used to count the number of perfect matchings in a planar graph. And a graph is planar if and only if it does not have K$_5$ or K$_{3,3}$ as a minor.

A paper that will be presented at the CCC conference this year is called:

Counting the Number of Perfect Matchings in $K_5$-free Graphs [in polynomial time] Simon Straub (Ulm University), Thomas Thierauf (Aalen University), Fabian Wagner (Ulm University)

I did not manage to read it yet, but i am curious to see, how they circumvent the K$_{3,3}$ minor problem.

########################################################################
# AUTHOR: Dr. Christian Schridde
# E-MAIL: christianschridde [at] googlemail [dot] com
#
# DESCRIPTION: Implementation of the FKT-algorithm
#
# INPUT:  Adjacency matrix A of a undirected loop-free planar graph G
# OUTPUT: Skew matrix M, such that PerfMatch(G) = Sqrt(Determinat(M))
########################################################################