Extensions of SAT
An extension that has gained significant popularity since 2003 is Satisfiability modulo theories (SMT) that can enrich CNF formulas with linear constraints, arrays, all-different constraints, uninterpreted functions, etc. Such extensions typically remain NP-complete, but very efficient solvers are now available that can handle many such kinds of constraints.
The satisfiability problem becomes more difficult (PSPACE-complete) if we allow both "for all" and "there exists" quantifiers to bind the Boolean variables. An example of such an expression would be:
SAT itself uses only quantifiers. If we allow only quantifiers, it becomes the Co-NP-complete tautology problem. If we allow both, the problem is called the quantified Boolean formula problem (QBF), which can be shown to be PSPACE-complete. It is widely believed that PSPACE-complete problems are strictly harder than any problem in NP, although this has not yet been proved.
A number of variants deal with the number of variable assignments making the formula true. Ordinary SAT asks if there is at least one such assignment. MAJSAT, which asks if the majority of all assignments make the formula true, is complete for PP, a probabilistic class. The problem of how many variable assignments satisfy a formula, not a decision problem, is in #P. UNIQUE-SAT or USAT or Unambiguous SAT is the problem of determining whether a formula known to have either zero or one satisfying assignments has zero or has one. Although this problem seems easier, it has been shown that if there is a practical (randomized polynomial-time) algorithm to solve this problem, then all problems in NP can be solved just as easily.
The maximum satisfiability problem, an FNP generalization of SAT, asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient approximation algorithms, but is NP-hard to solve exactly. Worse still, it is APX-complete, meaning there is no polynomial-time approximation scheme (PTAS) for this problem unless P=NP.
Read more about this topic: Boolean Satisfiability Problem
Famous quotes containing the words extensions of, extensions and/or sat:
“The psychological umbilical cord is more difficult to cut than the real one. We experience our children as extensions of ourselves, and we feel as though their behavior is an expression of something within us...instead of an expression of something in them. We see in our children our own reflection, and when we don’t like what we see, we feel angry at the reflection.”
—Elaine Heffner (20th century)
“The psychological umbilical cord is more difficult to cut than the real one. We experience our children as extensions of ourselves, and we feel as though their behavior is an expression of something within us...instead of an expression of something in them. We see in our children our own reflection, and when we don’t like what we see, we feel angry at the reflection.”
—Elaine Heffner (20th century)
““you were with me all day; stood with me, sat with me, talked with me, looked at me, ate with me, drank with me; and yet, your last act was to clutch for a monster, not only an innocent man, but the most pitiable of all men. So far may even the best man err, in judging the conduct of one with the recesses of whose condition he is not acquainted.””
—Herman Melville (1819–1891)