Sharp-SAT

Last updated
The correct title of this article is #SAT. The substitution of the # is due to technical restrictions.

In computer science, the Sharp Satisfiability Problem (sometimes called Sharp-SAT, #SAT or model counting) is the problem of counting the number of interpretations that satisfy 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), and ( = TRUE, = TRUE), we have

Contents

#SAT is different from Boolean satisfiability problem (SAT), which asks if there exists a solution of Boolean formula. Instead, #SAT asks to enumerate allthe 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] The #P-completeness already in the monotone case, i.e., when there are no negations (#MONOTONE-2-CNF).

It is known that, assuming that NP is different from RP, #MONOTONE-2-CNF also cannot be approximated by a fully polynomial-time approximation scheme (FPRAS), even assuming that each variable occurs in at most 6 clauses, but that a fully polynomial-time approximation scheme (FPTAS) exists when each variable occurs in at most 5 clauses: [4] this follows from analogous results on the problem ♯IS of counting the number of independent sets in graphs.

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

Planar #3SAT

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

Planar Monotone Rectilinear #3SAT

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

#DNF

For disjunctive normal form (DNF) formulas, counting the solutions is also #P-complete, even when all clauses have size 2 and there are no negations: this is because, by De Morgan's laws, counting the number of solutions of a DNF amounts to counting the number of solutions of the negation of a conjunctive normal form (CNF) formula. Intractability even holds in the case known as #PP2DNF, where the variables are partitioned into two sets, with each clause containing one variable from each set. [8]

By contrast, it is possible to tractably approximate the number of solutions of a disjunctive normal form formula using the Karp-Luby algorithm, which is an FPRAS for this problem. [9]

Tractable special cases

Affine constraint satisfaction problems

The variant of SAT corresponding to affine relations in the sense of Schaefer's dichotomy theorem, i.e., where clauses amount to equations modulo 2 with the XOR operator, is the only SAT variant for which the #SAT problem can be solved in polynomial time. [10]

Bounded treewidth

If the instances to SAT are restricted using graph parameters, the #SAT problem can become tractable. For instance, #SAT on SAT instances whose treewidth is bounded by a constant can be performed in polynomial time. [11] Here, the treewidth can be the primal treewidth, dual treewidth, or incidence treewidth of the hypergraph associated to the SAT formula, whose vertices are the variables and where each clause is represented as a hyperedge.

Restricted circuit and diagram classes

Model counting is tractable (solvable in polynomial time) for (ordered) BDDs and for some circuit formalisms studied in knowledge compilation, such as d-DNNFs.

Generalizations

Weighted model counting (WMC) generalizes #SAT by computing a linear combination of the models instead of just counting the models. In the literal-weighted variant of WMC, each literal gets assigned a weight, such that .

WMC is used for probabilistic inference, as probabilistic queries over discrete random variables such as in baysian networks can be reduced to WMC. [12]

Algebraic model counting further generalizes #SAT and WMC over arbitrary commutative semirings. [13]

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether 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. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

In computational complexity theory, the complexity class #P (pronounced "sharp P" or, sometimes "number P" or "hash P") is the set of the counting problems associated with the decision problems in the set NP. More formally, #P is the class of function problems of the form "compute f(x)", where f is the number of accepting paths of a nondeterministic Turing machine running in polynomial time. Unlike most well-known complexity classes, it is not a class of decision problems but a class of function problems. The most difficult, representative problems of this class are #P-complete.

In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time.

In computational complexity theory, the Cook–Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete. That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.

In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn.

MAX-3SAT is a problem in the computational complexity subfield of computer science. It generalises the Boolean satisfiability problem (SAT) which is a decision problem considered in complexity theory. It is defined as:

In computational complexity theory, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. It is a generalization of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.

In computational complexity, problems that are in the complexity class NP but are neither in the class P nor NP-complete are called NP-intermediate, and the class of such problems is called NPI. Ladner's theorem, shown in 1975 by Richard E. Ladner, is a result asserting that, if P ≠ NP, then NPI is not empty; that is, NP contains problems that are neither in P nor NP-complete. Since it is also true that if NPI problems exist, then P ≠ NP, it follows that P = NP if and only if NPI is empty.

In computational complexity theory, a branch of computer science, Schaefer's dichotomy theorem, proved by Thomas Jerome Schaefer, states necessary and sufficient conditions under which a finite set S of relations over the Boolean domain yields polynomial-time or NP-complete problems when the relations of S are used to constrain some of the propositional variables. It is called a dichotomy theorem because the complexity of the problem defined by S is either in P or is NP-complete, as opposed to one of the classes of intermediate complexity that is known to exist by Ladner's theorem.

In computational complexity theory, a gadget is a subunit of a problem instance that simulates the behavior of one of the fundamental units of a different computational problem. Gadgets are typically used to construct reductions from one computational problem to another, as part of proofs of NP-completeness or other types of computational hardness. The component design technique is a method for constructing reductions by using gadgets.

In computational complexity theory, the language TQBF is a formal language consisting of the true quantified Boolean formulas. A (fully) quantified Boolean formula is a formula in quantified propositional logic where every variable is quantified, using either existential or universal quantifiers, at the beginning of the sentence. Such a formula is equivalent to either true or false. If such a formula evaluates to true, then that formula is in the language TQBF. It is also known as QSAT.

MAXEkSAT is a problem in computational complexity theory that is a maximization version of the Boolean satisfiability problem 3SAT. In MAXEkSAT, each clause has exactly k literals, each with distinct variables, and is in conjunctive normal form. These are called k-CNF formulas. The problem is to determine the maximum number of clauses that can be satisfied by a truth assignment to the variables in the clauses.

In computational complexity theory, the exponential time hypothesis is an unproven computational hardness assumption that was formulated by Impagliazzo & Paturi (1999). It states that satisfiability of 3-CNF Boolean formulas cannot be solved in subexponential time, . More precisely, the usual form of the hypothesis asserts the existence of a number such that all algorithms that correctly solve this problem require time at least The exponential time hypothesis, if true, would imply that P ≠ NP, but it is a stronger statement. It implies that many computational problems are equivalent in complexity, in the sense that if one of them has a subexponential time algorithm then they all do, and that many known algorithms for these problems have optimal or near-optimal time complexity.

In theoretical computer science, the circuit satisfiability problem is the decision problem of determining whether a given Boolean circuit has an assignment of its inputs that makes the output true. In other words, it asks whether the inputs to a given Boolean circuit can be consistently set to 1 or 0 such that the circuit outputs 1. If that is the case, the circuit is called satisfiable. Otherwise, the circuit is called unsatisfiable. In the figure to the right, the left circuit can be satisfied by setting both inputs to be 1, but the right circuit is unsatisfiable.

In computational complexity theory, a branch of computer science, the Max/min CSP/Ones classification theorems state necessary and sufficient conditions that determine the complexity classes of problems about satisfying a subset S of boolean relations. They are similar to Schaefer's dichotomy theorem, which classifies the complexity of satisfying finite sets of relations; however, the Max/min CSP/Ones classification theorems give information about the complexity of approximating an optimal solution to a problem defined by S.

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.

In computational complexity theory and game complexity, a parsimonious reduction is a transformation from one problem to another that preserves the number of solutions. Informally, it is a bijection between the respective sets of solutions of two problems. A general reduction from problem to problem is a transformation that guarantees that whenever has a solution also has at least one solution and vice versa. A parsimonious reduction guarantees that for every solution of , there exists a unique solution of and vice versa.

In computational complexity, not-all-equal 3-satisfiability (NAE3SAT) is an NP-complete variant of the Boolean satisfiability problem, often used in proofs of NP-completeness.

<span class="mw-page-title-main">Planar SAT</span> Boolean satisfiability problem restricted to a planar incidence graph

In computer science, the planar 3-satisfiability problem (abbreviated PLANAR 3SAT or PL3SAT) is an extension of the classical Boolean 3-satisfiability problem to a planar incidence graph. In other words, it asks whether the variables of a given Boolean formula—whose incidence graph consisting of variables and clauses can be embedded on a plane—can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

In theoretical computer science, monotone dualization is a computational problem of constructing the dual of a monotone Boolean function. Equivalent problems can also be formulated as constructing the transversal hypergraph of a given hypergraph, of listing all minimal hitting sets of a family of sets, or of listing all minimal set covers of a family of sets. These problems can be solved in quasi-polynomial time in the combined size of its input and output, but whether they can be solved in polynomial time is an open problem.

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. ↑ Valiant, Leslie G. (1979). "The complexity of enumeration and reliability problems". SIAM Journal on Computing . 8 (3): 410–421. doi:10.1137/0208032.
  4. ↑ Liu, Jingcheng; Lu, Pinyan (2015). FPTAS for Counting Monotone CNF. Society for Industrial and Applied Mathematics. pp. 1531–1548. arXiv: 1311.3728 . doi:10.1137/1.9781611973730.101. ISBN   978-1-61197-374-7.
  5. ↑ 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 .
  6. ↑ Lichtenstein, David (1982). "Planar Formulae and Their Uses". SIAM Journal on Computing. 11 (2): 329–343. doi:10.1137/0211025.
  7. 1 2 de Berg, Mark; Khosravi, Amirali (2010). "Optimal binary space partitions in the plane". In Thai, My T.; Sahni, Sartaj (eds.). Computing and Combinatorics: 16th Annual International Conference, COCOON 2010, Nha Trang, Vietnam, July 19-21, 2010, Proceedings. Lecture Notes in Computer Science. Vol. 6196. Berlin: Springer. pp. 216–225. doi:10.1007/978-3-642-14031-0_25. ISBN   978-3-642-14030-3. MR   2720098.
  8. ↑ Suciu, Dan; Olteanu, Dan; Ré, Christopher; Koch, Christoph (2011), Suciu, Dan; Olteanu, Dan; Ré, Christopher; Koch, Christoph (eds.), "The Query Evaluation Problem", Probabilistic Databases, Synthesis Lectures on Data Management, Cham: Springer International Publishing, pp. 45–52, doi:10.1007/978-3-031-01879-4_3, ISBN   978-3-031-01879-4 , retrieved 2023-09-16
  9. ↑ Karp, Richard M; Luby, Michael; Madras, Neal (1989-09-01). "Monte-Carlo approximation algorithms for enumeration problems". Journal of Algorithms. 10 (3): 429–448. doi:10.1016/0196-6774(89)90038-2. ISSN   0196-6774.
  10. ↑ Creignou, Nadia; Hermann, Miki (1996-02-25). "Complexity of Generalized Satisfiability Counting Problems". Information and Computation. 125 (1): 1–12. doi: 10.1006/inco.1996.0016 . ISSN   0890-5401.
  11. ↑ FICHTE, JOHANNES K.; HECHER, MARKUS; THIER, PATRICK; WOLTRAN, STEFAN (2021-03-12). "Exploiting Database Management Systems and Treewidth for Counting". Theory and Practice of Logic Programming. 22 (1): 128–157. arXiv: 2001.04191 . doi:10.1017/s147106842100003x. ISSN   1471-0684.
  12. ↑ Chavira, Mark; Darwiche, Adnan (April 2008). "On probabilistic inference by weighted model counting". Artificial Intelligence. 172 (6–7): 772–799. doi:10.1016/j.artint.2007.11.002.
  13. ↑ Kimmig, Angelika; Van den Broeck, Guy; De Raedt, Luc (July 2017). "Algebraic model counting". Journal of Applied Logic. 22: 46–62. arXiv: 1211.4475 . doi:10.1016/j.jal.2016.11.031.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.