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:
“If we focus exclusively on teaching our children to read, write, spell, and count in their first years of life, we turn our homes into extensions of school and turn bringing up a child into an exercise in curriculum development. We should be parents first and teachers of academic skills second.”
—Neil Kurshan (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)
“We [actors] are indeed a strange lot! There are times we doubt that we have any emotions we can honestly call our own. I have approached every dynamic scene change in my life the same way. When I married Charlie MacArthur, I sat down and wondered how I could play the best wife that ever was.... My love for him was the truest thing in my life; but it was still important that I love him with proper effect, that I act loving him with great style, that I achieve the ultimate in wifedom.”
—Helen Hayes (1900–1993)