This article needs additional citations for verification. (June 2019) (Learn how and when to remove this template message) |

In computer science, the **Sharp Satisfiability Problem** (sometimes called **Sharp-SAT** or **#SAT**) is the problem of counting the number of interpretations that satisfies 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 is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments ( = TRUE, = FALSE), ( = FALSE, = FALSE),

( = TRUE, = TRUE), we have = 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 exponential number of possibilities.

#SAT is a well-known example of the class of counting problems, known as #P-complete (read as sharp 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.^{[2]}

## #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 (#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.

### #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 (deciding whether a 2CNF formula has a solution) 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.^{[3]}

### Planar #3SAT

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

### Planar Monotone Rectilinear #3SAT

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

## Tractable special cases

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

## Software

sharpSAT is software for solving practical instances of the #SAT problem."sharpSAT - Marc Thurley". *sites.google.com*. Retrieved 2019-04-30.

## References

**^**Valiant, L.G. (1979). "The complexity of computing the permanent".*Theoretical Computer Science*.**8**(2): 189–201. doi:10.1016/0304-3975(79)90044-6.**^**Vadhan, Salil Vadhan (20 November 2018). "Lecture 24: Counting Problems" (PDF).**^**Creignou, Nadia; Hermann, Miki (1996). "Complexity of Generalized Satisfiability Counting Problems".*Information and Computation*.**125**: 1–12. doi:10.1006/inco.1996.0016. hdl:10068/41883.**^**Lichtenstein, David (1982). "Planar Formulae and Their Uses".*SIAM Journal on Computing*.**11:2**: 329–343.- ^
^{a}^{b}Khosravi, Amirali; Berg, Mark de (2010). "Optimal Binary Space Partitions in the Plane".*undefined*. Retrieved 2019-05-01.