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.

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.

This article is issued from Wikipedia - version of the 4/1/2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.