Sharp SAT

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.

Contents

• Intractable special cases
• Tractable special cases
• References

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.