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.

Weird exceptions

Some say Computational Complexity is all about the $1$-million worth question $$\mathsf{P} \overset{?}{=} \mathsf{NP}$$ Of course, this is far from being correct. There are many more complexity classes and many more models of computation. Technically, the two classes $\mathsf{P}$ and $\mathsf{NP}$ are not special. But they are of special interest, since they pose a barrier between what perhaps can be computed on our classical computers in a feasible amount of time and those problems that in many cases would require an exponential amount of time. Or, spoken in a more simple way, they show up the barrier between what can be computed and what can not be computed due resource constraints.

However, there are some problems that have some weird special cases, which seem to be missed accidentally by the claws of the $\mathsf{NP}$ monster and fell into the lower class of $\mathsf{P}$. Both examples are actual based on the beautiful work of Leslie Valiant who showed how to connect the problem to count satisfying assignments to counting perfect matchings in planar graphs. The first one is:

$\#_2$ $\mathsf{PL}$-$\mathsf{RTW}$-$\mathsf{MON}$-$3\mathsf{CNF}$ vs. $\#_7$ $\mathsf{PL}$-$\mathsf{RTW}$-$\mathsf{MON}$-$3\mathsf{CNF}$