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 a ∨ ¬ b {\displaystyle a\lor \neg b} {\displaystyle a\lor \neg b} is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments ( a = TRUE, b = FALSE), ( a = FALSE, b = FALSE),
( a = TRUE, 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 an 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.
Khosravi, Amirali; Berg, Mark de (2010). "Optimal Binary Space Partitions in the Plane". undefined. Retrieved 2019-05-01.
Undergraduate Texts in Mathematics
Graduate Studies in Mathematics
Hellenica World - Scientific Library
Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License
