Special cases of SAT and corresponding #SAT with complexity a most O(n^2) AND that have efficient algorithms for generating instances?

Question

I am interested in learning about special cases of boolean satisfiability problems that are known to be polynomial (or more realistically, O(N^2)). These cases should also have efficient algorithm for actually generating all satisfactory instances, where by efficient I mean it takes O(N #SAT) to generate a sequence of all the instances. It is possible that the second condition implies the first, but it is not clear to me.

Trivial example: 1SAT :)

Trivial example: 2SAT with "chains" of clauses, so that the graph joining variables with clauses is a line.

Is there a list of more somewhere? Thanks.

Answer 1

From The Complexity of Satisfiability Problems by Schaefer:

We show that (assuming P != NP) SAT(S) is polynomial-time decidable only if at least one of the following conditions holds:

(a) Every relation in S is satisfied when all variables are 0.

(b) Every relation in S is satisfied when all variables are 1.

(c) Every relation in S is definable by a CNF formula in which each conjunct has at most one negated variable.

(d) Every relation in S is definable by a CNF formula in which each conjunct has at most one unnegated variable.

(e) Every relation in S is definable by a CNF formula having at most 2 literals in each conjunct.

(f) Every relation in S is the set of solutions of a system of linear equation over the two-element field {0,1}.

The first two are solvable O(1), the next three O(n) and the last O(n^3) (I think). So the SAT instances you want are in one of the first five classes.