Sharp-SAT

This article needs additional citations for verification. Please help by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources:  –  ·  ·  · scholar · JSTOR (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 ${\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 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.^[3]

#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.^[4]

Planar #3SAT[]

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

Planar Monotone Rectilinear #3SAT[]

This is the counting version of Planar Monotone Rectilinear 3SAT.^[6] The NP-hardness reduction given by de Berg & Khosravi^[6] 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.

References[]