Sharp-SAT


In computer science, the Sharp Satisfiability Problem is the problem of counting the number of interpretations that satisfies a given Boolean formula, introduced by Valiant in 1979. 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 is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments,,
, we have = TRUE.
#SAT is different from Boolean satisfiability problem, 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 exponential number of possibilities.
#SAT is a well-known example of the class of counting problems, known as #P-complete. In other words, every instance of a problem in the complexity class #P 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.

#P-Completeness

#SAT is #P-complete. 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.

Intractable special cases

Counting solutions is intractable in many special cases for which satisfiability is tractable, as well as when satisfiability is intractable. This includes the following.

#3SAT

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.

#2SAT

Even though 2SAT is polynomial, counting the number of solutions is #P-complete.

#Horn-SAT

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.

Planar #3SAT

This is the counting version of Planar 3SAT. The hardness reduction from 3SAT to Planar 3SAT given by Lichtenstein is parsimonious. This implies that Planar #3SAT is #P-complete.

Planar Monotone Rectilinear #3SAT

This is the counting version of Planar Monotone Rectilinear 3SAT. The NP-hardness reduction given by de Berg & Khosravi is parsimonious. Therefore, this problem is #P-complete as well.

Tractable special cases

Model-counting is tractable for BDDs and for d-DNNFs.

Software

sharpSAT is software for solving practical instances of the #SAT problem.