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.