In computer science, the Sharp Satisfiability Problem (sometimes called Sharp-SAT, #SAT or model counting) is the problem of counting the number of interpretations that satisfy a given Boolean formula, introduced by Valiant in 1979.[1] In other words, it asks in how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. For example, the formula
a\lor\negb
a
b
a
b
a
b
a\lor\negb=sf{TRUE}.
#SAT is different from Boolean satisfiability problem (SAT), which asks if there exists a solution of Boolean formula. Instead, #SAT asks to enumerate all the solutions to a Boolean Formula. #SAT is harder than SAT in the sense that, once the total number of solutions to a Boolean formula is known, SAT can be decided in constant time. However, the converse is not true, because knowing a Boolean formula has a solution does not help us to count all the solutions, as there are an exponential number of possibilities.
#SAT is a well-known example of the class of counting problems, known as
(read as sharp P complete). In other words, every instance of a problem in the complexity class
can be reduced to an instance of the #SAT problem. This is an important result because many difficult counting problems arise in Enumerative Combinatorics, Statistical physics, Network Reliability, and Artificial intelligence without any known formula. If a problem is shown to be hard, then it provides a complexity theoretic explanation for the lack of nice looking formulas.[2]
#SAT is
. To prove this, first note that #SAT is obviously in #P.
Next, we prove that #SAT is #P-hard. Take any problem #A in #P. We know that A can be solved using a Non-deterministic Turing Machine M. On the other hand, from the proof for Cook-Levin Theorem, we know that we can reduce M to a boolean formula F. Now, each valid assignment of F corresponds to a unique acceptable path in M, and vice versa. However, each acceptable path taken by M represents a solution to A. In other words, there is a bijection between the valid assignments of F and the solutions to A. So, the reduction used in the proof for Cook-Levin Theorem is parsimonious. This implies that #SAT is #P-hard.
Counting solutions is intractable (#P-complete) in many special cases for which satisfiability is tractable (in P), as well as when satisfiability is intractable (NP-complete). This includes the following.
This is the counting version of 3SAT. One can show that any formula in SAT can be rewritten as a formula in 3-CNF form preserving the number of satisfying assignments. Hence, #SAT and #3SAT are counting equivalent and #3SAT is #P-complete as well.
Even though 2SAT (deciding whether a 2CNF formula has a solution) is polynomial, counting the number of solutions is
-complete.[3] The #P-completeness already in the monotone case, i.e., when there are no negations (#MONOTONE-2-CNF).
It is known that, assuming that NP is different from RP, #MONOTONE-2-CNF also cannot be approximated by a fully polynomial-time approximation scheme (FPRAS), even assuming that each variable occurs in at most 6 clauses, but that a fully polynomial-time approximation scheme (FPTAS) exists when each variable occurs in at most 5 clauses:[4] this follows from analogous results on the problem ♯IS of counting the number of independent sets in graphs.
Similarly, even though Horn-satisfiability is polynomial, counting the number of solutions is #P-complete. This result follows from a general dichotomy characterizing which SAT-like problems are #P-complete.[5]
This is the counting version of Planar 3SAT. The hardness reduction from 3SAT to Planar 3SAT given by Lichtenstein[6] is parsimonious. This implies that Planar #3SAT is #P-complete.
This is the counting version of Planar Monotone Rectilinear 3SAT.[7] The NP-hardness reduction given by de Berg & Khosravi is parsimonious. Therefore, this problem is #P-complete as well.
For disjunctive normal form (DNF) formulas, counting the solutions is also
By contrast, it is possible to tractably approximate the number of solutions of a disjunctive normal form formula using the Karp-Luby algorithm, which is an FPRAS for this problem.[8]
The variant of SAT corresponding to affine relations in the sense of Schaefer's dichotomy theorem, i.e., where clauses amount to equations modulo 2 with the XOR operator, is the only SAT variant for which the #SAT problem can be solved in polynomial time.[9]
If the instances to SAT are restricted using graph parameters, the #SAT problem can become tractable. For instance, #SAT on SAT instances whose treewidth is bounded by a constant can be performed in polynomial time.[10] Here, the treewidth can be the primal treewidth, dual treewidth, or incidence treewidth of the hypergraph associated to the SAT formula, whose vertices are the variables and where each clause is represented as a hyperedge.
Model counting is tractable (solvable in polynomial time) for (ordered) BDDs and for some circuit formalisms studied in knowledge compilation, such as d-DNNFs.
Weighted model counting (WMC) generalizes #SAT by computing a linear combination of the models instead of just counting the models. In the literal-weighted variant of WMC, each literal gets assigned a weight, such that
WMC(\phi;w)=\sumM\prodlw(l)
WMC is used for probabilistic inference, as probabilistic queries over discrete random variables such as in baysian networks can be reduced to WMC.[11]
Algebraic model counting further generalizes #SAT and WMC over arbitrary commutative semirings.[12]