CNF restrictions that lead to exponential speedup

Blogposts are good place to write things up, because they do not magically disappear as most of the handwritten notes on my desktop. I was creating a list of different types of CNF formulas to mark which restrictions makes counting solutions or deciding satisfiability polynomial computable. Such an overview is certainly not new but i did not find a sufficiently complete list. So i tried to come up with such a list by myself and thought it could be of some interest for you. The restrictions i was aiming at have the following abbreviations:

• $\text{Ex3SAT}$ : Each clause has exact $3$ variables
• $\text{Pl}$ : The incidence graph of a formula $\Phi$ is planar
• $\text{Tree}$ : The incidence graph of a formula $\Phi$ is a tree
• $\text{Mon}$ : Monotone, i.e., each variable occurs only in positive form
• $\text{Rtw}$ : ReadTwice, i.e., each variable occurs at most twice
• $\text{x-in-N}$ : Exactly $x$ variables out of $N$ must be true in each clause. So $\text{1-in-3-3CNF}$ also forces that each clause has exactly 3 variables and not less. So $\text{1-in-3-Ex3CNF}$ is actually the same.
• $\text{RtwOpp}$ : The variable occurs twice but in opposite value, i.e., once negative and once positive
• $\text{Nae}$ : Not all equal, i.e., in a satisfying assignment, at least one variable in a clause must be false

Note, if you know the number $1-in-3$ solutions of a formula $\Phi$, then if you negate all variables, you get a $2-in-3$ solution.

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

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)