Sharp-SAT

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 ${\displaystyle a\lor \neg b}$ is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments (${\displaystyle a}$ = TRUE, ${\displaystyle b}$ = FALSE), (${\displaystyle a}$ = FALSE, ${\displaystyle b}$ = FALSE),
(${\displaystyle a}$ = TRUE, ${\displaystyle b}$ = TRUE), we have ${\displaystyle a\lor \neg b}$ = 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

1. 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.
2. Vadhan, Salil Vadhan (20 November 2018). "Lecture 24: Counting Problems" (PDF).
3. 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.
4. Lichtenstein, David (1982). "Planar Formulae and Their Uses". SIAM Journal on Computing. 11:2: 329–343.
5. Khosravi, Amirali; Berg, Mark de (2010). "Optimal Binary Space Partitions in the Plane". undefined. Retrieved 2019-05-01.