Sharp-SAT

The correct title of this article is #SAT. The substitution or omission of the # is because of technical restrictions.

In computational complexity theory, #SAT, or Sharp-SAT, a function problem related to the Boolean satisfiability problem, is the problem of counting the number of satisfying assignments of a given Boolean formula. It is well-known example for the class of counting problems, which are of special interest in computational complexity theory.

It is a #P-complete problem, as any NP machine can be encoded into a Boolean formula by a process similar to that in Cook's theorem, such that the number of satisfying assignments of the Boolean formula is equal to the number of accepting paths of the NP machine. Any formula in SAT can be rewritten as a formula in 3-CNF form preserving the number of satisfying assignments, and so #SAT and #3SAT are equivalent and #3SAT is #P-complete as well.

Intractable special cases

Model-counting is intractable in many special cases for which satisfiability is tractable. This includes the following.

• sets of Horn clauses
• sets of 2-literal clauses

Tractable special cases

Model-counting is tractable (solvable in polynomial time) for (ordered) BDDs and for d-DNNFs.