Boolean satisfiability problem: Difference between revisions

Revision as of 15:17, 7 May 2009

Latest revision as of 05:39, 26 August 2025

(716 intermediate revisions by more than 100 users not shown)

Line 1:

{{short description|Problem of determining if a Boolean formula could be made true}}

{{Redirect|3SAT|the television network|3sat}}

{{Redirect|3SAT|the Central European television network|3sat}}

In [[logic]] and [[computer science]], the '''Boolean satisfiability problem''' (sometimes called '''propositional satisfiability problem''' and abbreviated '''SATISFIABILITY''', '''SAT''' or '''B-SAT''') asks whether there exists an [[Interpretation (logic)|interpretation]] that [[Satisfiability|satisfies]] a given [[Boolean logic|Boolean]] [[Formula (mathematical logic)|formula]]. In other words, it asks whether the formula's variables can be consistently replaced by the values TRUE or FALSE to make the formula evaluate to TRUE. If this is the case, the formula is called ''satisfiable'', else ''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.

'''Satisfiability''' is the problem of determining if the variables of a given

[[Boolean logic|Boolean]] formula can be assigned in such a way as to make the formula

evaluate to TRUE. Equally important is to determine whether no such assignments

exist, which would imply that the function expressed by the formula is identically FALSE

for all possible variable assignments. In this latter case, we would say

that the function is unsatisfiable; otherwise it is satisfiable. To emphasize

the binary nature of this problem, it is frequently referred to as '''Boolean'''

or '''propositional satisfiability'''. The shorthand "'''SAT'''" is also commonly used

to denote it, with the implicit understanding that the function and its variables

are all binary-valued.

SAT is the first problem that was proven to be [[NP-complete]]—this is the [[Cook–Levin theorem]]. This means that all problems in the complexity class [[NP (complexity)|NP]], which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves each SAT problem (where "efficiently" means "deterministically in [[Time complexity#Polynomial time|polynomial time]]"). Although such an algorithm is generally believed not to exist, this belief has not been proven or disproven mathematically. Resolving the question of whether SAT has a [[polynomial-time]] algorithm would settle the [[P versus NP problem]] - one of the most important open problems in the theory of computing.<ref>{{cite journal |author=Fortnow, L. |year=2009 |title=The status of the P versus NP problem |url=https://www.cs.cmu.edu/~15326-f23/CACM-Fortnow.pdf |journal=Communications of the ACM |volume=52 |issue=9 |pages=78–86 |doi=10.1145/1562164.1562186 |s2cid=5969255}}</ref><ref>{{cite journal |author=Fortnow, L. |year=2021 |title=Fifty Years of P Versus NP and the Possibility of the Impossible |url=https://lance.fortnow.com/papers/files/pvnp50.pdf |journal=Proceedings of ACM Conference (Conference'17)}}</ref>

== Basic definitions, terminology and applications ==

Nevertheless, as of 2007, heuristic SAT-algorithms are able to solve problem instances involving tens of thousands of variables and <!---"clauses" hasn't been introduced here:--->formulas consisting of millions of symbols,<ref name="Codish.Ohrimenko.Stuckey.2007"/> which is sufficient for many practical SAT problems from, e.g., [[artificial intelligence]], [[circuit design]],<ref>{{Cite book|last1=Hong|first1=Ted|last2=Li|first2=Yanjing|last3=Park|first3=Sung-Boem|last4=Mui|first4=Diana|last5=Lin|first5=David|last6=Kaleq|first6=Ziyad Abdel|last7=Hakim|first7=Nagib|last8=Naeimi|first8=Helia|last9=Gardner|first9=Donald S.|last10=Mitra|first10=Subhasish|title=2010 IEEE International Test Conference |chapter=QED: Quick Error Detection tests for effective post-silicon validation |date=November 2010|pages=1–10|doi=10.1109/TEST.2010.5699215|isbn=978-1-4244-7206-2|s2cid=7909084}}</ref> and [[automatic theorem proving]].

In [[computational complexity theory|complexity theory]], the '''Boolean satisfiability problem''' ('''SAT''')

is a [[decision problem]], whose instance is a Boolean expression written using only AND, OR, NOT, variables, and parentheses.

The question is: given the expression, is there some assignment of ''TRUE'' and ''FALSE'' values to the variables that will

make the entire expression true? A formula of [[propositional logic]] is said to be ''satisfiable'' if [[logical value]]s can be assigned to its [[Variable (mathematics)|variables]] in a way that makes the formula true. The boolean satisfiability problem is [[NP-complete]]. The propositional satisfiability problem (PSAT), which decides whether a given [[propositional formula]] is satisfiable, is of central importance in various areas of [[computer science]], including [[theoretical computer science]], [[algorithmics]], [[artificial intelligence]], [[hardware design]], [[Electronic Design Automation|electronic design automation]], and [[hardware verification|verification]].

==Definitions==

The problem can be significantly restricted while still remaining [[NP-complete]]. By applying [[De Morgan's laws]], we can assume that NOT operators are only applied directly to variables, not expressions; we refer to either a variable or its negation as a ''literal''. For example, both ''x''₁ and not(''x''₂) are literals, the first a ''positive'' literal and the second a ''negative'' literal. If we OR together a group of literals, we get a ''clause'', such as (''x''₁ ''or'' not(''x''₂)). Finally, let us consider formulae that are a conjunction (AND) of clauses - this is the [[conjunctive normal form]] (CNF). Determining whether a formula in this form is satisfiable is still NP-complete, even if each clause is limited to at most three literals. This last problem is called 3SAT, 3CNFSAT, or 3-satisfiability.

A ''[[propositional logic]] formula'', also called ''Boolean expression'', is built from [[Variable (mathematics)|variables]], operators AND ([[Logical conjunction|conjunction]], also denoted by ∧), OR ([[logical disjunction|disjunction]], ∨), NOT ([[negation]], ¬), and parentheses. A formula is said to be ''satisfiable'' if it can be made TRUE by assigning appropriate [[logical value]]s (i.e. TRUE, FALSE) to its variables. The ''Boolean satisfiability problem'' (SAT) is, given a formula, to check whether it is satisfiable. This [[decision problem]] is of central importance in many areas of [[computer science]], including [[theoretical computer science]], [[computational complexity theory|complexity theory]],<ref>{{cite book | last = Karp | first = Richard M. | author-link = Richard Karp | chapter = Reducibility Among Combinatorial Problems | title = Complexity of Computer Computations | editor = Raymond E. Miller | editor2 = James W. Thatcher | publisher = Plenum | ___location = New York | pages = 85–103 | year = 1972 | chapter-url = http://www.cs.berkeley.edu/~luca/cs172/karp.pdf | isbn = 0-306-30707-3 | access-date = 2020-05-07 | archive-date = 2011-06-29 | archive-url = https://web.archive.org/web/20110629023717/http://www.cs.berkeley.edu/~luca/cs172/karp.pdf | url-status = dead }} Here: p.86</ref><ref>{{cite book | isbn=0-201-00029-6 |first1=Alfred V. |last1=Aho |first2=John E. |last2=Hopcroft |first3=Jeffrey D. |last3=Ullman | title=The Design and Analysis of Computer Algorithms | publisher=Addison-Wesley | year=1974 |page=403}}</ref> [[algorithmics]], [[cryptography]]<ref>{{Cite journal|last1=Massacci|first1=Fabio|last2=Marraro|first2=Laura|date=2000-02-01|title=Logical Cryptanalysis as a SAT Problem |journal=Journal of Automated Reasoning |volume=24|issue=1|pages=165–203|doi=10.1023/A:1006326723002|s2cid=3114247 }}</ref><ref>{{Cite book|last1=Mironov|first1=Ilya|last2=Zhang|first2=Lintao|title=Theory and Applications of Satisfiability Testing - SAT 2006 |chapter=Applications of SAT Solvers to Cryptanalysis of Hash Functions |date=2006|editor-last=Biere|editor-first=Armin|editor2-last=Gomes|editor2-first=Carla P.|chapter-url=https://link.springer.com/chapter/10.1007%2F11814948_13|series=Lecture Notes in Computer Science|volume=4121 |publisher=Springer|pages=102–115|doi=10.1007/11814948_13|isbn=978-3-540-37207-3}}</ref> and [[artificial intelligence]].<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| s2cid = 10190144 }}</ref>{{additional citation needed|date=May 2020}}

===Conjunctive normal form===

On the other hand, if we restrict each clause to at most two literals, the resulting problem, [[2SAT]], is [[NL-complete|'''NL'''-complete]]. Alternately, if every clause must be a [[Horn clause]], containing at most one positive literal, the resulting problem, [[Horn-satisfiability]], is [[P-complete|'''P'''-complete]].

A ''literal'' is either a variable (in which case it is called a ''positive literal'') or the negation of a variable (called a ''negative literal''). A ''clause'' is a disjunction of literals (or a single literal). A clause is called a ''[[Horn clause]]'' if it contains at most one positive literal. A formula is in ''[[conjunctive normal form]]'' (CNF) if it is a conjunction of clauses (or a single clause).

The [[Cook–Levin theorem]] proves that the Boolean satisfiability problem is [[NP-complete]],

and in fact, this was the first decision problem proved to be NP-complete.

However, beyond this theoretical significance, efficient and

scalable algorithms for SAT that were developed over the last decade have contributed to dramatic advances in our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints. Examples of such problems in [[Electronic Design Automation]] (EDA) include [[formal equivalence checking|combinational equivalence checking]], [[model checking]], [[formal verification]] of [[microprocessor|pipelined microprocessors]], [[automatic test pattern generation]], [[routing (electronic design automation)|routing]] of [[FPGA]]s, and so on. In fact, an SAT-solving engine is now considered to be an essential component in the EDA toolbox and all EDA vendors provide such a capability (usually behind the scenes.)

For example, {{math|size=100%|''x''₁}} is a positive literal, {{math|size=100%|¬''x''₂}} is a negative literal, and {{math|size=100%|''x''₁ ∨ ¬''x''₂}} is a clause. The formula {{math|size=100%|(''x''₁ ∨ ¬''x''₂) ∧ (¬''x''₁ ∨ ''x''₂ ∨ ''x''₃) ∧ ¬''x''₁}} is in conjunctive normal form; its first and third clauses are Horn clauses, but its second clause is not. The formula is satisfiable, by choosing ''x''₁&nbsp;=&nbsp;FALSE, ''x''₂&nbsp;=&nbsp;FALSE, and ''x''₃ arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ ''x''₃) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ ''x''₃) ∧ TRUE, and in turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formula ''a'' ∧ ¬''a'', consisting of two clauses of one literal, is unsatisfiable, since for ''a''=TRUE or ''a''=FALSE it evaluates to TRUE ∧ ¬TRUE (i.e., FALSE) or FALSE ∧ ¬FALSE (i.e., again FALSE), respectively.

==Complexity and restricted versions ==

=== NP-completeness ===

For some versions of the SAT problem,<!---need not list them in detail here---(viz. [[#Exactly-1 3-satisfiability|Exactly-1 3-satisfiability]], [[#XOR-satisfiability|XOR-satisfiability]], and, more general, [[#Schaefer's dichotomy theorem|Schaefer's dichotomy theorem]], discussed below),---> it is useful to define the notion of a ''generalized conjunctive normal form'' formula, viz. as a conjunction of arbitrarily many ''generalized clauses'', the latter being of the form {{math|''R''(''l''₁,...,''l''_''n'')}} for some [[Boolean function]] ''R'' and (ordinary) literals {{mvar|''l''_''i''}}. Different sets of allowed Boolean functions lead to different problem versions.<!---, see [[#Complexity and restricted versions|below]].---> As an example, ''R''(¬''x'',''a'',''b'') is a generalized clause, and ''R''(¬''x'',''a'',''b'') ∧ ''R''(''b'',''y'',''c'') ∧ ''R''(''c'',''d'',¬''z'') is a generalized conjunctive normal form. This formula is used [[#Exactly-1 3-satisfiability|below]], with ''R'' being the ternary operator that is TRUE just when exactly one of its arguments is.

SAT was the first known [[NP-complete]] problem, as proved by [[Stephen Cook]] in 1971 (see [[Cook's theorem]] for the proof). Until that time, the concept of an NP-complete problem did not even exist. The problem remains '''NP'''-complete even if all expressions are written in ''[[conjunctive normal form]]'' with 3 variables per clause (3-CNF), yielding the '''3SAT''' problem. This means the expression has the form:

<!---need not explain that already here---If ''R'' is the ternary operator that is TRUE just if exactly one of its arguments is, then a satisfying assignment for the latter formula can be found starting from every possible combination of truth values for ''x'', ''y'', ''z'', except ''x''&nbsp;=&nbsp;''y''&nbsp;=&nbsp;''z''&nbsp;=&nbsp;FALSE, and choosing the values of ''a'', ''b'', ''c'', ''d'' appropriately; cf. the left table under [[#Exactly-1 3-satisfiability|Exactly-1 3-satisfiability]] below.--->

:(''x''₁₁ OR ''x''₁₂ OR ''x''₁₃) AND

:(''x''₂₁ OR ''x''₂₂ OR ''x''₂₃) AND

:(''x''₃₁ OR ''x''₃₂ OR ''x''₃₃) AND ...

where each ''x'' is a variable or a negation of a variable, and each variable can appear multiple times in the expression.

Using the laws of [[Boolean algebra (structure)|Boolean algebra]], every propositional logic formula can be transformed into an equivalent conjunctive normal form, which may, however, be exponentially longer. For example, transforming the formula (''x''₁∧''y''₁) ∨ (''x''₂∧''y''₂) ∨ ... ∨ (''x''_''n''∧''y''_''n'') into conjunctive normal form yields

A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, if a graph has 17 valid 3-colorings, the SAT formula produced by the reduction will have 17 satisfying assignments.

{{block indent|{{math|(''x''₁&nbsp;∨&nbsp;''x''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''_''n'') ∧}}}}

{{block indent|{{math|(''y''₁&nbsp;∨&nbsp;''x''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''_''n'') ∧}}}}

{{block indent|{{math|(''x''₁&nbsp;∨&nbsp;''y''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''_''n'') ∧}}}}

{{block indent|{{math|(''y''₁&nbsp;∨&nbsp;''y''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''_''n'') ∧ ... ∧}}}}

{{block indent|{{math|(''x''₁&nbsp;∨&nbsp;''x''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''_''n'') ∧}}}}

{{block indent|{{math|(''y''₁&nbsp;∨&nbsp;''x''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''_''n'') ∧}}}}

{{block indent|{{math|(''x''₁&nbsp;∨&nbsp;''y''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''_''n'') ∧}}}}

{{block indent|{{math|(''y''₁&nbsp;∨&nbsp;''y''₂&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''_''n'')}};}}

while the former is a disjunction of ''n'' conjunctions of 2 variables, the latter consists of 2^''n'' clauses of ''n'' variables.

However, with use of the [[Tseytin transformation]], we may find an equisatisfiable conjunctive normal form formula with length linear in the size of the original propositional logic formula.

NP-completeness only refers to the run-time of the worst case instances. Many of the instances that occur in practical applications can be solved much more quickly. See [[#Runtime behavior|runtime behavior]] below.

==Complexity==

SAT is easier if the formulas are restricted to those in [[disjunctive normal form]], that is, they are disjunction (OR) of terms, where each term is a conjunction (AND) of literals (possibly negated variables). Such a formula is indeed satisfiable if and only if at least one of its terms is satisfiable, and a term is satisfiable if and only if it does not contain both ''x'' and NOT ''x'' for some variable ''x''. This can be checked in polynomial time.

{{Main|Cook–Levin theorem}}

===2-satisfiability===

{{main|2-satisfiability}}

SAT is also easier if the number of literals in a clause is limited to 2, in which case the problem is called 2SAT. This problem can also be solved in polynomial time, and in fact is complete for the class [[NL (complexity)|NL]]. Similarly, if we limit the number of literals per clause to 2 and change the AND operations to [[Exclusive or|XOR]] operations, the result is ''exclusive-or 2-satisfiability'', a problem complete for [[SL (complexity)|SL]] = [[L (complexity)|L]].

SAT was the first problem known to be [[NP-complete]], as proved by [[Stephen Cook]] at the [[University of Toronto]] in 1971<ref>{{Cite book | last1 = Cook | first1 = Stephen A. | title = Proceedings of the third annual ACM symposium on Theory of computing - STOC '71 | chapter = The complexity of theorem-proving procedures | author-link1=Stephen Cook| pages = 151–158 | year = 1971 | chapter-url=http://www.cs.toronto.edu/~sacook/homepage/1971.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.cs.toronto.edu/~sacook/homepage/1971.pdf |archive-date=2022-10-09 |url-status=live| doi = 10.1145/800157.805047| citeseerx = 10.1.1.406.395 | s2cid = 7573663 }}</ref> and independently by [[Leonid Levin]] at the [[Russian Academy of Sciences#The Academy of Sciences of the USSR|Russian Academy of Sciences]] in 1973.<ref>{{cite journal|last=Levin|first=Leonid|author-link=Leonid Levin|title = Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)|journal = Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii)|volume = 9|issue = 3|pages = 115–116|year = 1973}} [http://www.mathnet.ru/php/getFT.phtml?jrnid=ppi&paperid=914&volume=9&year=1973&issue=3&fpage=115&what=fullt&option_lang=eng (pdf)] {{in lang|ru}}, translated into English by {{cite journal|last=Trakhtenbrot|first=B. A.|title = A survey of Russian approaches to ''perebor'' (brute-force searches) algorithms|journal = Annals of the History of Computing |volume = 6|issue = 4|pages = 384–400|year = 1984|doi=10.1109/MAHC.1984.10036|s2cid=950581}}</ref> Until that time, the concept of an NP-complete problem did not even exist. The proof shows how every decision problem in the [[complexity class]] [[NP (complexity)|NP]] can be [[reduction (complexity)|reduced]] to the SAT problem for CNF{{efn|The SAT problem for ''arbitrary'' formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.}} formulas, sometimes called '''CNFSAT'''. A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, deciding whether a given [[Graph (discrete mathematics)|graph]] has a [[Graph coloring#Vertex coloring|3-coloring]] is another problem in NP; if a graph has 17 valid 3-colorings, then the SAT formula produced by the Cook–Levin reduction will have 17 satisfying assignments.

One of the most important restrictions of SAT is HORNSAT, where the formula is a conjunction of [[Horn clause]]s. This problem is solved by the polynomial-time [[Horn-satisfiability]] algorithm, and is in fact [[P-complete]]. It can be seen as [[P (complexity)|P's]] version of the Boolean satisfiability problem.

NP-completeness only refers to the run-time of the worst case instances. Many of the instances that occur in practical applications can be solved much more quickly. See [[#Algorithms for solving SAT|§Algorithms for solving SAT]] below.

Provided that the [[P = NP problem|complexity classes P and NP are not equal]], none of these restrictions are NP-complete, unlike SAT. The assumption that P and NP are not equal is not currently proven.

===3-satisfiability===

[[File:Sat reduced to Clique from Sipser.svg|thumb|upright=1.25|The 3-SAT instance {{math|(''x'' ∨ ''x'' ∨ ''y'') ∧ (¬''x'' ∨ ¬''y'' ∨ ¬''y'') ∧ (¬''x'' ∨ ''y'' ∨ ''y'')}} reduced to a [[clique problem]]. The green vertices form a 3-clique and correspond to the satisfying assignment ''x''=FALSE, ''y''=TRUE.]]

3-satisfiability is a special case of [[k-satisfiability|''k''-satisfiability]] (''k''-SAT) or simply satisfiability (SAT), when each clause contains exactly ''k'' = 3 literals. It was one of [[Karp's 21 NP-complete problems]].

Like the satisfiability problem for arbitrary formulas, determining the satisfiability of a formula in conjunctive normal form where each clause is limited to at most three literals is NP-complete also; this problem is called '''3-SAT''', '''3CNFSAT''', or '''3-satisfiability'''. To reduce the unrestricted SAT problem to 3-SAT, transform each clause {{math|''l''₁ ∨ ⋯ ∨ ''l''_''n''}} to a conjunction of {{math|''n'' - 2}} clauses

{{block indent|{{math|(''l''₁ ∨ ''l''₂ ∨ ''x''₂) ∧ }}}}

Here is an example, where ¬ indicates NOT:

: E ={{block indent|{{math|(''x''₁ or ¬''x''₂ or∨ ¬''xl''₃) and∨ (''x''₁₃) or∧ ''x''₂ or ''x''₄)}}}}

E has two clauses (denoted by parentheses), four literals{{block indent|{{math|(¬''x''₁₃, ''x''₂,∨ ''xl''₃₄, ∨ ''x''₄), and∧ ''k''=3⋯ (three∧ literals per clause).}}}}

{{block indent|{{math|(¬''x''_''n''−3 ∨ ''l''_''n''−2 ∨ ''x''_''n''−2) ∧ }}}}

{{block indent|{{math|(¬''x''_''n''−2 ∨ ''l''_''n''−1 ∨ ''l''_''n'')}}}}

where {{math|''x''₂,&thinsp;⋯&thinsp;,&thinsp;''x''_''n''−2}} are [[fresh variable]]s not occurring elsewhere. Although the two formulas are not [[logically equivalent]], they are [[equisatisfiable]]. The formula resulting from transforming all clauses is at most 3 times as long as its original; that is, the length growth is polynomial.{{sfnp|Aho|Hopcroft|Ullman|1974|loc=Theorem 10.4}}

To solve this instance of the decision problem we must determine whether there is a truth value (TRUE or FALSE) we can assign to each of the literals (''x''₁ through ''x''₄) such that the entire expression is TRUE. In this instance, there is such an assignment (''x''₁ = TRUE, ''x''₂ = TRUE, ''x''₃=TRUE, ''x''₄=TRUE), so the answer to this instance is YES. This is one of many possible assignments, with for instance, any set of assignments including ''x''₁ = TRUE being sufficient. If there were no such assignment(s), the answer would be NO.

3-SAT is one of [[Karp's 21 NP-complete problems]], and it is used as a starting point for proving that other problems are also [[NP-hard]].{{efn|i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.}} This is done by [[polynomial-time reduction]] from 3-SAT to the other problem. An example of a problem where this method has been used is the [[clique problem]]: given a CNF formula consisting of ''c'' clauses, the corresponding [[Graph (discrete mathematics)|graph]] consists of a vertex for each literal, and an edge between each two non-contradicting{{efn|i.e. such that one literal is not the negation of the other}} literals from different clauses; see the picture. The graph has a ''c''-clique if and only if the formula is satisfiable.{{sfnp|Aho|Hopcroft|Ullman|1974|loc=Theorem 10.5}}

Since k-SAT (the general case) reduces to 3-SAT, and 3-SAT can be proven to be [[NP-complete]], it can be used to prove that other problems are also NP-complete. This is done by showing how a solution to another problem could be used to solve 3-SAT. An example of a problem where this method has been used is "[[Clique problem|Clique]]". It's often easier to use reductions from 3-SAT than SAT to problems that researchers are attempting to prove NP-complete.

There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)^''n'' where ''n'' is the number of variables in the 3-SAT proposition, and succeeds with high probability to correctly decide 3-SAT.<ref name="Schoning.1999">{{cite book| last1=Schöning| first1=Uwe| title=40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039)| chapter=A probabilistic algorithm for k-SAT and constraint satisfaction problems| pages=410–414| date=Oct 1999| isbn=0-7695-0409-4| chapter-url=http://homepages.cwi.nl/~rdewolf/schoning99.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://homepages.cwi.nl/~rdewolf/schoning99.pdf |archive-date=2022-10-09 |url-status=live| doi=10.1109/SFFCS.1999.814612| s2cid=123177576}}</ref>

3-SAT can be further restricted to [[One-in-three 3SAT]], where we ask if ''exactly'' one of the variables in each clause is true, rather than ''at least'' one. One-in-three 3SAT remains NP-complete.

The [[exponential time hypothesis]] asserts that no algorithm can solve 3-SAT (or indeed ''k''-SAT for any {{Math|''k'' > 2}}) in {{math|exp([[Small o notation#Little-o notation|''o'']](''n''))}} time (that is, fundamentally faster than exponential in ''n'').

===Horn-satisfiability===

Selman, Mitchell, and Levesque (1996) give empirical data on the difficulty of randomly generated 3-SAT formulas, depending on their size parameters. Difficulty is measured in number recursive calls made by a [[DPLL algorithm]]. They identified a phase transition region from almost-certainly-satisfiable to almost-certainly-unsatisfiable formulas at the clauses-to-variables ratio at about 4.26.<ref>{{cite journal|first1=Bart |last1=Selman |first2=David |last2=Mitchell |first3=Hector |last3=Levesque | title=Generating Hard Satisfiability Problems| journal=Artificial Intelligence| year=1996| volume=81|issue=1–2 | pages=17–29| doi=10.1016/0004-3702(95)00045-3|citeseerx=10.1.1.37.7362 }}</ref>

{{main|Horn-satisfiability}}

3-satisfiability can be generalized to '''k-satisfiability''' ('''k-SAT''', also '''k-CNF-SAT'''), when formulas in CNF are considered with each clause containing up to ''k'' literals.{{citation needed|date=May 2020}} However, since for any ''k'' ≥ 3, this problem can neither be easier than 3-SAT nor harder than SAT, and the latter two are NP-complete, so must be k-SAT.

A clause is Horn if it contains at most one positive literal. Such clauses are of interest because they are able to express [[implication]] of one variable from a set of other variables. Indeed, one such clause <math>\neg x_1 \vee \cdots \vee \neg x_n \vee y</math> can be rewritten as <math>x_1 \wedge \cdots \wedge x_n \rightarrow y</math>, that is, if <math>x_1,\ldots,x_n</math> are all true, then <math>y</math> needs to be true as well.

Some authors restrict k-SAT to CNF formulas with '''exactly k literals'''.{{citation needed|date=May 2020}} This does not lead to a different complexity class either, as each clause {{math|''l''₁ ∨ ⋯ ∨ ''l''_''j''}} with ''j'' < ''k'' literals can be padded with fixed dummy variables to {{math|''l''₁ ∨ ⋯ ∨ ''l''_''j'' ∨ ''d''_''j''+1 ∨ ⋯ ∨ ''d''_''k''}}. After padding all clauses, 2^''k''–1 extra clauses{{efn|viz. all [[Canonical form (Boolean algebra)#Maxterms|maxterms]] that can be built with {{math|''d''₁,⋯,''d''_''k''}}, except {{math|''d''₁∨⋯∨''d''_''k''}}}} must be appended to ensure that only {{math|1=''d''₁ = ⋯ = ''d''_''k'' = FALSE}} can lead to a satisfying assignment. Since ''k'' does not depend on the formula length, the extra clauses lead to a constant increase in length. For the same reason, it does not matter whether '''duplicate literals''' are allowed in clauses, as in {{math|¬''x'' ∨ ¬''y'' ∨ ¬''y''}}.

The problem of deciding whether a set of Horn clauses is satisfiable is in P. This problem can indeed be solved by a single step of the [[Unit propagation]], which produces the single minimal (w.r.t. the set of literal assigned to true) model of the set of Horn clauses.

== Special instances of 3SAT ==

A generalization of the class of Horn formulae is that of renamable-Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.

=== Conjunctive normal form ===

===Schaefer's dichotomy theorem===

Conjunctive normal form (in particular with 3 literals per clause) is often considered the canonical representation for SAT formulas. As shown above, the general SAT problem reduces to 3-SAT, the problem of determining satisfiability for formulas in this form.

===Linear SAT===

{{main|Schaefer's dichotomy theorem}}

A 3-SAT formula is ''Linear SAT'' (''LSAT'') if each clause (viewed as a set of literals) intersects at most one other clause, and, moreover, if two clauses intersect, then they have exactly one literal in common. An LSAT formula can be depicted as a set of disjoint semi-closed intervals on a line. Deciding whether an LSAT formula is satisfiable is NP-complete.<ref>{{Cite journal|last1=Arkin|first1=Esther M.|last2=Banik|first2=Aritra|last3=Carmi|first3=Paz|last4=Citovsky|first4=Gui|last5=Katz|first5=Matthew J.|last6=Mitchell|first6=Joseph S. B.|last7=Simakov|first7=Marina|date=2018-12-11|title=Selecting and covering colored points|journal=Discrete Applied Mathematics|language=en|volume=250|pages=75–86|doi=10.1016/j.dam.2018.05.011|issn=0166-218X|doi-access=free}}</ref>

===2-satisfiability===

The restrictions above (CNF, 2CNF, 3CNF, Horn) bound the considered formulae to be conjunction of subformulae; each restriction states a specific form for all subformulae: for example, only binary clauses can be subformulae in 2CNF.

{{Main|2-satisfiability}}

SAT is easier if the number of literals in a clause is limited to at most 2, in which case the problem is called '''[[2-satisfiability|2-SAT]]'''. This problem can be solved in polynomial time, and in fact is [[NL-complete|complete]] for the complexity class [[NL (complexity)|NL]]. If additionally all OR operations in literals are changed to [[Exclusive or|XOR]] operations, then the result is called '''exclusive-or 2-satisfiability''', which is a problem complete for the complexity class [[SL (complexity)|SL]] = [[L (complexity)|L]].

Schaefer's dichotomy theorem states that, for any restriction to Boolean operators that can be used to form these subformulae, the corresponding satisfiability problem is in P or NP-complete. The membership in P of the satisfiability of 2CNF and Horn formulae are special cases of this theorem.

===Runtime behaviorHorn-satisfiability===

{{Main|Horn-satisfiability}}

The problem of deciding the satisfiability of a given conjunction of [[Horn clause]]s is called '''Horn-satisfiability''', or '''HORN-SAT'''. It can be solved in polynomial time by a single step of the [[unit propagation]] algorithm, which produces the single minimal model of the set of Horn clauses (w.r.t. the set of literals assigned to TRUE). Horn-satisfiability is [[P-complete]]. It can be seen as [[P (complexity)|P's]] version of the Boolean satisfiability problem. Also, deciding the truth of quantified Horn formulas can be done in polynomial time.<ref name="buningkarpinski">{{Cite journal | last1 = Buning | first1 = H.K. | last2 = Karpinski| first2 = Marek| last3=Flogel|first3=A.|year = 1995 | title = Resolution for Quantified Boolean Formulas | journal = Information and Computation | volume = 117 | issue = 1 | pages = 12–18 | publisher = Elsevier | doi= 10.1006/inco.1995.1025| doi-access = free }}</ref>

As mentioned briefly above, though the problem is NP-complete, many practical instances can be solved much more quickly. Many practical problems are actually "easy", so the SAT solver can easily find a solution, or prove that none exists, relatively quickly, even though the instance has thousands of variables and tens of thousands of constraints. Other much smaller problems exhibit run-times that are exponential in the problem size, and rapidly become impractical. Unfortunately, there is no reliable way to tell the difficulty of the problem without trying it. Therefore, almost all SAT solvers include time-outs, so they will terminate even if they cannot find a solution. Finally, different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. All of these behaviors can be seen in the SAT solving contests.<ref>{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|accessdate=2007-11-15}}</ref>

Horn clauses are of interest because they are able to express [[Entailment|implication]] of one variable from a set of other variables. Indeed, one such clause ¬''x''₁ ∨ ... ∨ ¬''x''_''n'' ∨ ''y'' can be rewritten as ''x''₁ ∧ ... ∧ ''x''_''n'' → ''y''; that is, if ''x''₁,...,''x''_''n'' are all TRUE, then ''y'' must be TRUE as well.

==Extensions of SAT==

A generalization of the class of Horn formulas is that of renameable-Horn formulae, which is the set of formulas that can be placed in Horn form by replacing some variables with their respective negation. For example, (''x''₁ ∨ ¬''x''₂) ∧ (¬''x''₁ ∨ ''x''₂ ∨ ''x''₃) ∧ ¬''x''₁ is not a Horn formula, but can be renamed to the Horn formula (''x''₁ ∨ ¬''x''₂) ∧ (¬''x''₁ ∨ ''x''₂ ∨ ¬''y''₃) ∧ ¬''x''₁ by introducing ''y''₃ as negation of ''x''₃. In contrast, no renaming of (''x''₁ ∨ ¬''x''₂ ∨ ¬''x''₃) ∧ (¬''x''₁ ∨ ''x''₂ ∨ ''x''₃) ∧ ¬''x''₁ leads to a Horn formula. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.

An extension that has gained significant popularity since 2003 is [[Satisfiability modulo theories]]

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.

== Not 3SAT problems ==

The satisfiability problem becomes more difficult (PSPACE-complete) if we allow ''[[quantifier]]s'' such as "for all" and "there exists" that bind the Boolean variables. An example of such an expression would be:

: <math>\forall x, \exists y,\exists z; (x \lor y \lor z) \land (\lnot x \lor \lnot y \lor \lnot z).</math>

SAT itself uses only <math>\exists</math> quantifiers. If we allow only <math>\forall</math> quantifiers, it becomes the [[Co-NP-complete]] [[Tautology (logic)|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.

=== Disjunctive normal form ===

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 (complexity)|PP]], a probabilistic class. The problem of how many variable assignments satisfy a formula, not a decision problem, is in [[Sharp-P|#P]]. UNIQUE-SAT or USAT 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, [[Valiant-Vazirani theorem|it has been shown]] that if there is a practical ([[BPP|randomized polynomial-time]]) algorithm to solve this problem, then all problems in [[NP (complexity class)|NP]] can be solved just as easily.

SAT is trivial if the formulas are restricted to those in '''[[disjunctive normal form]]''', that is, they are a disjunction of conjunctions of literals. Such a formula is indeed satisfiable if and only if at least one of its conjunctions is satisfiable, and a conjunction is satisfiable if and only if it does not contain both ''x'' and NOT ''x'' for some variable ''x''. This can be checked in linear time. Furthermore, if they are restricted to being in '''full disjunctive normal form''', in which every variable appears exactly once in every conjunction, they can be checked in constant time (each conjunction represents one satisfying assignment). But it can take exponential time and space to convert a general SAT problem to disjunctive normal form; to obtain an example, exchange "∧" and "∨" in the [[#Definitions|above]] exponential blow-up example for conjunctive normal forms.

===Exactly-1 3-satisfiability===

The [[maximum satisfiability problem]], an [[FNP (complexity)|FNP]] generalization of SAT, asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient [[approximation algorithm]]s, 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.

{{Main|1-in-3-SAT}}

Another NP-complete variant of the 3-satisfiability problem is the '''one-in-three 3-SAT''' (also known variously as '''1-in-3-SAT''' and '''exactly-1 3-SAT'''). Given a conjunctive normal form with three literals per clause, the problem is to determine whether there exists a truth assignment to the variables so that each clause has ''exactly'' one TRUE literal (and thus exactly two FALSE literals).

==Algorithms for solving SAT==

===Not-all-equal 3-satisfiability===

There are two classes of high-performance [[algorithms]] for solving instances of SAT in practice: modern variants of the [[DPLL algorithm]], such as [[Chaff algorithm|Chaff]], [[GRASP (SAT solver)|GRASP]] or [http://www.st.ewi.tudelft.nl/sat/march_dl.php march], and [[stochastic local search algorithm]]s, such as [[WalkSAT]].

{{main|Not-all-equal 3-satisfiability}}

Another variant is the '''not-all-equal 3-satisfiability''' problem (also called '''NAE3SAT'''). Given a conjunctive normal form with three literals per clause, the problem is to determine if an assignment to the variables exists such that in no clause all three literals have the same truth value. This problem is NP-complete, too, even if no negation symbols are admitted, by Schaefer's dichotomy theorem.<ref name="schaefer">{{Cite conference |last1=Schaefer |first1=Thomas J. |year=1978 |title=The complexity of satisfiability problems |url=http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf |pages=216–226 |citeseerx=10.1.1.393.8951 |doi=10.1145/800133.804350 |book-title=Proceedings of the 10th Annual ACM Symposium on Theory of Computing |place=San Diego, California}}</ref>

A DPLL SAT solver employs a systematic backtracking search procedure to explore the (exponentially-sized) space of variable assignments looking for satisfying assignments. The basic search procedure was proposed in two seminal papers in the early 60s (see references below) and is now commonly referred to as the [[Davis-Putnam-Logemann-Loveland algorithm]] (“DPLL” or “DLL”).

=== XOR-satisfiability ===

Modern SAT solvers (developed in the last ten years) come in two flavors: "conflict-driven" and "look-ahead". Conflict-driven solvers augment the basic DPLL search algorithm with efficient conflict analysis, clause learning, non-[[chronological backtracking]] (aka [[backjumping]]), as well as "two-watched-literals" unit propagation, adaptive branching, and random restarts. These "extras" to the basic systematic search have been empirically shown to be essential for handling the large SAT instances that arise in [[Electronic Design Automation]] (EDA). Look-ahead solvers have especially strengthened reductions (going beyond unit-clause propagation) and the heuristics, and they are generally stronger than conflict-driven solvers on hard instances (while conflict-driven solvers can be much better on large instances which have inside actually an easy instance).

{{Main|XOR-SAT}}

Another special case is the class of problems where each clause contains XOR (i.e. [[exclusive or]]) rather than (plain) OR operators. This is in [[P (complexity class)|P]], since an XOR-SAT formula can also be viewed as a system of linear equations mod 2, and can be solved in cubic time by [[Gaussian elimination]].<ref>{{citation|title=The Nature of Computation|first1=Cristopher|last1=Moore|author1-link=Cristopher Moore|first2=Stephan|last2=Mertens|publisher=Oxford University Press|year=2011|isbn=9780199233212|page=366|url=https://books.google.com/books?id=z4zMiZyAE1kC&pg=PA366}}.</ref>

Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and operations research, among others. Powerful solvers are readily available as [[free software]], and are remarkably{{Fact|date=October 2008}} easy to use. In particular, the conflict-driven [http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ MiniSAT], which was relatively successful at the [http://www.satcompetition.org/ 2005 SAT competition], only has about 600 lines of code. An example for look-ahead solvers is [http://www.st.ewi.tudelft.nl/sat/march_dl.php march_dl], which won a prize at the [http://www.satcompetition.org/ 2007 SAT competition].

== Schaefer's dichotomy theorem ==

[[Genetic algorithm]]s and other general-purpose [[stochastic local search method]]s are also being used to solve SAT problems, especially when there is no or limited knowledge of the specific structure of the problem instances to be solved. Certain types of large random satisfiable instances of SAT can be solved by [[survey propagation]] (SP). Particularly in [[hardware design]] and [[hardware verification|verification]] applications, satisfiability and other logical properties of a given propositional formula are sometimes decided based on a representation of the formula as a [[binary decision diagram]] (BDD).

{{Main|Schaefer's dichotomy theorem}}

The restrictions above (CNF, 2CNF, 3CNF, Horn, XOR-SAT) bound the considered formulae to be conjunctions of subformulas; each restriction states a specific form for all subformulas: for example, only binary clauses can be subformulas in 2CNF.

Schaefer's dichotomy theorem states that, for any restriction to Boolean functions that can be used to form these subformulas, the corresponding satisfiability problem is in P or NP-complete. The membership in P of the satisfiability of 2CNF, Horn, and XOR-SAT formulae are special cases of this theorem.<ref name="schaefer"/>

Propositional satisfiability has various generalisations, including satisfiability for [[quantified Boolean formula problem]], for [[first-order predicate calculus|first]]- and [[second-order logic]], [[constraint satisfaction problem]]s, [[0-1 integer programming]], and [[maximum satisfiability problem]].

The following table summarizes some common variants of SAT.

Many other decision problems, such as [[graph coloring]] problems, [[planning problem]]s, and [[Scheduling algorithm|scheduling problems]], can be easily encoded into SAT.

{| class="wikitable sortable"

|+

! Name

! Code

! 3SAT problem?

! Restrictions

! Requirements

! Class

|-

| ''3-satisfiability''

| <code>3SAT</code>

| {{Yes}}

| Each clause contains 3 literals.

| At least one literal must be true.

| NP-c

|-

| ''2-satisfiability''

| <code>2SAT</code>

| {{Yes}}

| Each clause contains 2 literals.

| At least one literal must be true.

| NL-c

|-

| ''Exactly-1 3-SAT''

| <code>1-in-3-SAT</code>

| {{No}}

| Each clause contains 3 literals.

| Exactly one literal must be true.

| NP-c

|-

| ''Exactly-1 Positive 3-SAT''

| <code>1-in-3-SAT+</code>

| {{No}}

| Each clause contains 3 positive literals.

| Exactly one literal must be true.

| NP-c

|-

| ''Not-all-equal 3-satisfiability''

| <code>NAE3SAT</code>

| {{No}}

| Each clause contains 3 literals.

| Either one or two literals must be true.

| NP-c

|-

| ''Not-all-equal positive 3-SAT''

| <code>NAE3SAT+</code>

| {{No}}

| Each clause contains 3 positive literals.

| Either one or two literals must be true.

| NP-c

|-

| [[Planar SAT|''Planar SAT'']]

| <code>PL-SAT</code>

| {{Yes}}

| The incidence graph (clause-variable graph) is [[Planar graph|planar]].

| At least one literal must be true.

| NP-c

|-

| ''Linear SAT''

| <code>LSAT</code>

| {{Yes}}

| Each clause contains 3 literals, intersects at most one other clause, and the intersection is exactly one literal.

| At least one literal must be true.

| NP-c

|-

| ''Horn satisfiability''

| <code>HORN-SAT</code>

| {{Yes}}

| Horn clauses (at most one positive literal).

| At least one literal must be true.

| P-c

|-

| ''Xor satisfiability''

| <code>XOR-SAT</code>

| {{No}}

| Each clause contains XOR operations rather than OR.

| The XOR of all literals must be true.

| P

|}

==SeeExtensions alsoof 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 function]]s,<ref name="Bryant.German.Velev.1999">R. E. Bryant, S. M. German, and M. N. Velev, [http://portal.acm.org/citation.cfm?id=709275 Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions], in Analytic Tableaux and Related Methods, pp.&nbsp;1–13, 1999.</ref> 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 if both "for all" ([[∀]]) and "there exists" ([[∃]]) [[Quantifier (logic)|quantifier]]s are allowed to bind the Boolean variables. An example of such an expression would be {{math|size=100%|∀''x'' ∀''y'' ∃''z'' (''x'' ∨ ''y'' ∨ ''z'') ∧ (¬''x'' ∨ ¬''y'' ∨ ¬''z'')}}; it is valid, since for all values of ''x'' and ''y'', an appropriate value of ''z'' can be found, viz. ''z''=TRUE if both ''x'' and ''y'' are FALSE, and ''z''=FALSE else. SAT itself (tacitly) uses only ∃ quantifiers. If only ∀ quantifiers are allowed instead, the so-called '''[[Tautology (logic)|tautology]] problem''' is obtained, which is [[co-NP-complete]]. If any number of both quantifiers are allowed, 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.

*[[Unsatisfiable core]]

Ordinary SAT asks if there is at least one variable assignment that makes the formula true. A variety of variants deal with the number of such assignments:

==References==

* '''MAJ-SAT''' asks if at least half of all assignments make the formula TRUE. It is known to be complete for [[PP (complexity)|PP]], a probabilistic class. Surprisingly, '''MAJ-kSAT''' is demonstrated to be in P for every finite integer k.<ref>{{Cite book |title=MAJORITY-3SAT (and Related Problems) in Polynomial Time |date=2022 |doi=10.1109/FOCS52979.2021.00103 |arxiv=2107.02748 |language=en-US |last1=Akmal |first1=Shyan |last2=Williams |first2=Ryan |pages=1033–1043 |isbn=978-1-6654-2055-6 }}</ref>

*M. Davis and H. Putnam, {{doi-inline|10.1145/321033.321034|A Computing Procedure for Quantification Theory}}, Journal of the Association for Computing Machinery, vol. 7, no., pp. 201–215, 1960.

* '''[[Sharp-SAT|#SAT]]''', the problem of counting how many variable assignments satisfy a formula, is a counting problem, not a decision problem, and is [[Sharp-P-complete|#P-complete]].

*M. Davis, G. Logemann, and D. Loveland, {{doi-inline|10.1145/368273.368557|A Machine Program for Theorem-Proving}}, Communications of the ACM, vol. 5, no. 7, pp. 394–397, 1962.

* '''UNIQUE SAT'''<ref>{{Cite journal|last1=Blass|first1=Andreas|last2=Gurevich|first2=Yuri|date=1982-10-01|title=On the unique satisfiability problem|journal=Information and Control|volume=55|issue=1|pages=80–88|doi=10.1016/S0019-9958(82)90439-9|issn=0019-9958|doi-access=free|hdl=2027.42/23842|hdl-access=free}}</ref> is the problem of determining whether a formula has exactly one assignment. It is complete for [[US (complexity)|US]],<ref>{{Cite web|url=https://complexityzoo.uwaterloo.ca/Complexity_Zoo:U#US|title=Complexity Zoo:U - Complexity Zoo|website=complexityzoo.uwaterloo.ca|access-date=2019-12-05|archive-date=2019-07-09|archive-url=https://web.archive.org/web/20190709142353/https://complexityzoo.uwaterloo.ca/Complexity_Zoo:U#US|url-status=dead}}</ref> the [[complexity class]] describing problems solvable by a non-deterministic polynomial time [[Turing machine]] that accepts when there is exactly one nondeterministic accepting path and rejects otherwise.

*S. A. Cook, {{doi-inline|10.1145/800157.805047|The Complexity of Theorem Proving Procedures}}, in Proc. 3rd Ann. ACM Symp. on Theory of Computing, pp. 151–158, Association for Computing Machinery, 1971.

*'''UNAMBIGUOUS-SAT''' is the name given to the satisfiability problem when the input formula is [[Promise problem|promised]] to have at most one satisfying assignment. The problem is also called '''USAT'''.<ref>{{Cite book |chapter-url=https://www.springer.com/gp/book/9781846282973 |chapter=Supplementary Lecture F: Unique Satisfiability |title=Theory of Computation |last=Kozen |first=Dexter C. |date=2006 |publisher=Springer |isbn=9781846282973 |series=Texts in Computer Science |page=180 |language=en}}</ref> A solving algorithm for UNAMBIGUOUS-SAT is allowed to exhibit any behavior, including endless looping, on a formula having several satisfying assignments. Although this problem seems easier, Valiant and Vazirani have [[Valiant–Vazirani theorem|shown]]<ref>{{Cite journal | last1 = Valiant | first1 = L. | last2 = Vazirani | first2 = V.| doi = 10.1016/0304-3975(86)90135-0 | title = NP is as easy as detecting unique solutions | url = http://www.cs.princeton.edu/courses/archive/fall05/cos528/handouts/NP_is_as.pdf| journal = Theoretical Computer Science | volume = 47 | pages = 85–93 | year = 1986 | doi-access = free }}</ref> that if there is a practical (i.e. [[Bounded-error probabilistic polynomial|randomized polynomial-time]]) algorithm to solve it, then all problems in [[NP (complexity class)|NP]] can be solved just as easily.

*{{cite book|author = [[Michael R. Garey]] and [[David S. Johnson]] | year = 1979 | title = [[List_of_important_publications_in_computer_science#Computers and Intractability: A Guide to the Theory of NP-Completeness|Computers and Intractability: A Guide to the Theory of NP-Completeness]] | publisher = W.H. Freeman | isbn = 0-7167-1045-5}} A9.1: LO1 &ndash; LO7, pp.259 &ndash; 260.

* '''MAX-SAT''', the [[maximum satisfiability problem]], is an [[FNP (complexity)|FNP]] generalization of SAT. It asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient [[approximation algorithm]]s, 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.

*J. P. Marques-Silva and K. A. Sakallah, {{doi-inline|10.1109/12.769433|GRASP: A Search Algorithm for Propositional Satisfiability}}, IEEE Transactions on Computers, vol. 48, no. 5, pp. 506–521, 1999.

*'''WMSAT''' is the problem of finding an assignment of minimum weight that satisfy a monotone Boolean formula (i.e. a formula without any negation). Weights of propositional variables are given in the input of the problem. The weight of an assignment is the sum of weights of true variables. That problem is NP-complete (see Th. 1 of <ref>{{Cite book|last1=Buldas|first1=Ahto|last2=Lenin|first2=Aleksandr|last3=Willemson|first3=Jan|last4=Charnamord|first4=Anton|title=Advances in Information and Computer Security |chapter=Simple Infeasibility Certificates for Attack Trees |date=2017|editor-last=Obana|editor-first=Satoshi|editor2-last=Chida|editor2-first=Koji|volume=10418|series=Lecture Notes in Computer Science|language=en|publisher=Springer International Publishing|pages=39–55|doi=10.1007/978-3-319-64200-0_3|isbn=9783319642000}}</ref>).

*J.-P. Marques-Silva and T. Glass, {{doi-inline|10.1109/DATE.1999.761110|Combinational Equivalence Checking Using Satisfiability and Recursive Learning}}, in Proc. Design, Automation and Test in Europe Conference, pp. 145–149, 1999.

*R. E. Bryant, S. M. German, and M. N. Velev, [http://portal.acm.org/citation.cfm?id=709275 Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions], in Analytic Tableaux and Related Methods, pp. 1–13, 1999.

*M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, {{doi-inline|10.1145/378239.379017|Chaff: engineering an efficient SAT solver}}, in Proc. 38th ACM/IEEE Design Automation Conference, pp. 530–535, Las Vegas, Nevada, 2001.

*E. Clarke, A. Biere, R. Raimi, and Y. Zhu, {{doi-inline|10.1023/A:1011276507260|Bounded Model Checking Using Satisfiability Solving}}, Formal Methods in System Design, vol. 19, no. 1, 2001.

*M. Perkowski and A. Mishchenko, "Logic Synthesis for Regular Layout using Satisfiability," in Proc. Intl Workshop on Boolean Problems, 2002.

*G.-J. Nam, K. A. Sakallah, and R. Rutenbar, {{doi-inline|10.1109/TCAD.2002.1004311|A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability}}, [[IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems]], vol. 21, no. 6, pp. 674–684, 2002.

*N. Een and N. Sörensson, {{doi-inline|10.1007/b95238|An Extensible SAT-solver}}, in Satisfiability Workshop, 2003.

*D. Babić, J. Bingham, and A. J. Hu, {{doi-inline|10.1109/TC.2006.175|B-Cubing: New Possibilities for Efficient SAT-Solving}}, IEEE Transactions on Computers 55(11):1315–1324, 2006.

*C. Rodríguez, M. Villagra and B. Barán, {{doi-inline|10.1109/BIMNICS.2007.4610083|Asynchronous team algorithms for Boolean Satisfiability}}, Bionetics2007, pp. 66-69, 2007.

<references/>

Other generalizations include satisfiability for [[first-order predicate calculus|first]]- and [[second-order logic]], [[constraint satisfaction problem]]s, [[0-1 integer programming]].

==External links==

More information on SAT:

* [http://users.ecs.soton.ac.uk/mqq06r/sat/ SAT and MAX-SAT for the Lay-researcher]

SAT Applications:

* [http://users.ecs.soton.ac.uk/mqq06r/winsat/ WinSAT]: A Windows based SAT application made particularly for researchers.

==Finding a satisfying assignment==

SAT Solvers:

While SAT is a [[decision problem]], the [[search problem]] of finding a satisfying assignment reduces to SAT. That is, each algorithm which correctly answers whether an instance of SAT is solvable can be used to find a satisfying assignment. First, the question is asked on the given formula Φ. If the answer is "no", the formula is unsatisfiable. Otherwise, the question is asked on the partly instantiated formula Φ[[substitution (logic)|{''x''₁=TRUE}]], that is, Φ with the first variable ''x''₁ replaced by TRUE, and simplified accordingly. If the answer is "yes", then ''x''₁=TRUE, otherwise ''x''₁=FALSE. Values of other variables can be found subsequently in the same way. In total, ''n''+1 runs of the algorithm are required, where ''n'' is the number of distinct variables in Φ.

* [http://www.princeton.edu/~chaff/ Chaff]

* [http://www.cs.ubc.ca/~babic/index_hypersat.htm HyperSAT]

* [http://www.cs.ubc.ca/~babic/index_spear.htm Spear]

* [http://minisat.se/ The MiniSAT Solver]

* [http://www.satlib.org/ubcsat/ UBCSAT]

* [http://www.sat4j.org/ Sat4j]

* [http://reasoning.cs.ucla.edu/rsat/home.html RSat]

* [http://dudka.cz/fss Fast SAT Solver] - simple but fast implementation of SAT solver based on [[Genetic algorithm]]

* [http://www.cs.nyu.edu/acsys/cvc3/ CVC3]

This property is used in several theorems in complexity theory:

Conferences/Publications:

* [http://wwwcs.uni-paderborn.de/cs/ag-klbue/en/workshops/sat-08/sat08-main.php SAT 2008: Eleventh International Conference on Theory and Applications of Satisfiability Testing ]

* [http://sat07.ecs.soton.ac.uk/ SAT 2007: Tenth International Conference on Theory and Applications of Satisfiability Testing ]

* [http://jsat.ewi.tudelft.nl Journal on Satisfiability, Boolean Modeling and Computation]

* [http://www.ictp.trieste.it/~zecchina/SP/ Survey Propagation]

* [[NP (complexity)|NP]] ⊆ [[P/poly]] ⇒ [[PH (complexity)|PH]] = [[Polynomial hierarchy#Definitions|Σ₂]] ([[Karp–Lipton theorem]])

Benchmarks:

* [[NP (complexity)|NP]] ⊆ [[BPP (complexity)|BPP]] ⇒ [[NP (complexity)|NP]] = [[RP (complexity)|RP]]

* [http://www.nlsde.buaa.edu.cn/~kexu/benchmarks/benchmarks.htm Forced Satisfiable SAT Benchmarks]

* [[P (complexity)|P]] = [[NP (complexity)|NP]] ⇒ [[FP (complexity)|FP]] = [[FNP (complexity)|FNP]]

* [http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/bmcbenchmarks.html IBM Formal Verification SAT Benchmarks]

* [http://www.satlib.org SATLIB]

* [http://www.cs.ubc.ca/~babic/index_benchmarks.htm Software Verification Benchmarks]

SAT==Algorithms for solving in general:SAT==

{{main|SAT solver}}

* http://www.satlive.org

* http://www.satisfiability.org

Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in the ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).<ref name="Codish.Ohrimenko.Stuckey.2007">{{citation |title=Principles and Practice of Constraint Programming – CP 2007|series=Lecture Notes in Computer Science|volume=4741|year=2007|pages=544–558|contribution=Propagation = Lazy Clause Generation|first1=Olga|last1=Ohrimenko |first2=Peter J.|last2=Stuckey|first3=Michael|last3=Codish|doi=10.1007/978-3-540-74970-7_39|isbn=978-3-540-74969-1 |quote=modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables |citeseerx=10.1.1.70.5471}}.</ref> Examples of such problems in [[electronic design automation]] (EDA) include [[formal equivalence checking]], [[model checking]], [[formal verification]] of [[microprocessor|pipelined microprocessors]],<ref name="Bryant.German.Velev.1999"/> [[automatic test pattern generation]], [[routing (electronic design automation)|routing]] of [[FPGA]]s,<ref>{{Cite journal |last1=Gi-Joon Nam |last2=Sakallah |first2=K. A. |last3=Rutenbar |first3=R. A. |title=A new FPGA detailed routing approach via search-based Boolean satisfiability |journal=IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |volume=21 |issue=6 |pages=674 |year=2002 |url=http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf |doi=10.1109/TCAD.2002.1004311 |bibcode=2002ITCAD..21..674N |access-date=2015-09-04 |archive-date=2016-03-15 |archive-url=https://web.archive.org/web/20160315003856/http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf |url-status=dead }}</ref> [[Automated planning and scheduling|planning]], and [[Scheduling algorithm|scheduling problems]], and so on. A SAT-solving engine is also considered to be an essential component in the [[electronic design automation]] toolbox.

----

Major techniques used by modern SAT solvers include the [[Davis–Putnam–Logemann–Loveland algorithm]] (or DPLL), [[conflict-driven clause learning]] (CDCL), and [[stochastic]] [[Local search (constraint satisfaction)|local search]] algorithms such as [[WalkSAT]]. Almost all SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution. Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. Recent{{When|date=June 2024}} attempts have been made to learn an instance's satisfiability using deep learning techniques.<ref>{{cite arXiv |last1=Selsam |first1=Daniel |last2=Lamm |first2=Matthew |last3=Bünz |first3=Benedikt |last4=Liang |first4=Percy |last5=de Moura |first5=Leonardo |last6=Dill |first6=David L. |title=Learning a SAT Solver from Single-Bit Supervision |eprint=1802.03685 |date=11 March 2019|class=cs.AI }}</ref>

''This article includes material from a column in the ACM [http://www.sigda.org SIGDA] [http://www.sigda.org/newsletter/index.html e-newsletter] by [http://www.eecs.umich.edu/~karem Prof. Karem Sakallah] <br>

Original text is available [http://www.sigda.org/newsletter/2006/eNews_061201.html here].''

SAT solvers are developed and compared in SAT-solving contests.<ref>{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|access-date=2007-11-15}}</ref> Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and [[operations research]], among others.

{{logic}}

==See also==

*[[Unsatisfiable core]]

*[[Satisfiability modulo theories]]

*[[Sharp-SAT|Counting SAT]]

*[[Planar SAT]]

*[[Karloff–Zwick algorithm]]

*[[Circuit satisfiability]]

==Notes==

{{notelist}}

== External links ==

{{commons category}}

* [http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php?lang=eng SAT Game]: try solving a Boolean satisfiability problem yourself

* [http://www.satcompetition.org/ The international SAT competition website]

* [http://www.satisfiability.org/ International Conference on Theory and Applications of Satisfiability Testing]

* {{usurped|1=[https://web.archive.org/web/20060219180520/http://jsat.ewi.tudelft.nl/ Journal on Satisfiability, Boolean Modeling and Computation]}}

* [http://www.satlive.org SAT Live, an aggregate website for research on the satisfiability problem]

* [http://www.maxsat.udl.cat/ Yearly evaluation of MaxSAT solvers]

==References==

{{Reflist|30em}}

==Sources==

* This article includes material from https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html by Prof. [[Karem A. Sakallah]].

==Further reading==

(by date of publication)

{{refbegin|colwidth=30em}}

* {{cite book|first1=Michael R. |last1=Garey |first2=David S. |last2=Johnson|author-link=Michael R. Garey |author2-link=David S. Johnson |year=1979 |title=Computers and Intractability: A Guide to the Theory of NP-Completeness |publisher=W. H. Freeman |isbn=0-7167-1045-5 |title-link=List of important publications in theoretical computer science#Computers and Intractability: A Guide to the Theory of NP-Completeness |pages=A9.1: LO1–LO7, pp.&nbsp;259–260}}

* {{Cite book |last1=Marques-Silva |first1=J. |last2=Glass |first2=T. |chapter=Combinational equivalence checking using satisfiability and recursive learning |title=Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078) |pages=145 |year=1999 |isbn=0-7695-0078-1 |doi=10.1109/DATE.1999.761110 |url=http://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf |archive-date=2022-10-09 |url-status=live}}

* {{Cite journal |last1=Clarke |first1=E. |last2=Biere |first2=A. |last3=Raimi |first3=R. |last4=Zhu |first4=Y. |journal=Formal Methods in System Design |volume=19 |pages=7–34 |year=2001 |title=Bounded Model Checking Using Satisfiability Solving |doi=10.1023/A:1011276507260 |s2cid=2484208}}

* {{Cite book | last1 = Giunchiglia | first1 = E. | last2 = Tacchella | first2 = A. | editor1-last = Giunchiglia | editor1-first = Enrico | editor2-first = Armando | title = Theory and Applications of Satisfiability Testing | series = Lecture Notes in Computer Science | volume = 2919 | year = 2004 | isbn = 978-3-540-20851-8 | doi = 10.1007/b95238 | s2cid = 31129008 | editor2-last = Tacchella}}

* {{Cite journal | last1 = Babic | first1 = D. | last2 = Bingham | first2 = J. | last3 = Hu | first3 = A. J. | title = B-Cubing: New Possibilities for Efficient SAT-Solving | journal = IEEE Transactions on Computers | volume = 55 | issue = 11 | pages = 1315 | year = 2006 | url = http://www.domagoj-babic.com/uploads/Pubs/TCOM06/tcom06.pdf| archive-url = https://web.archive.org/web/20161023223352/http://www.domagoj-babic.com/uploads/Pubs/TCOM06/tcom06.pdf| url-status = usurped| archive-date = October 23, 2016| doi = 10.1109/TC.2006.175| bibcode = 2006ITCmp..55.1315B | s2cid = 14819050 }}

* {{Cite book | last1 = Rodriguez | first1 = C. | last2 = Villagra | first2 = M. | last3 = Baran | first3 = B. | chapter = Asynchronous team algorithms for Boolean Satisfiability | title = 2007 2nd Bio-Inspired Models of Network, Information and Computing Systems | pages = 66–69 | year = 2007 | chapter-url = http://www.cc.pol.una.py/lcca/publicaciones/optimizacion/2007/Asynchronous%20Team%20Algorithms%20for%20Boolean%20Satisfiability.pdf| doi = 10.1109/BIMNICS.2007.4610083| s2cid = 15185219 }}

* {{cite book |editor1-first=Frank Van |editor1-last=Harmelen |editor2-first=Vladimir |editor2-last=Lifschitz |editor3-first=Bruce |editor3-last=Porter |title=Handbook of knowledge representation|year=2008|publisher=Elsevier|isbn=978-0-444-52211-5|pages=89–134|first1=Carla P. |last1=Gomes|author1-link=Carla Gomes |first2=Henry |last2=Kautz |first3=Ashish |last3=Sabharwal |first4=Bart |last4=Selman |chapter=Satisfiability Solvers|doi=10.1016/S1574-6526(07)03002-7|series=Foundations of Artificial Intelligence|volume=3}}

* {{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| pages = 2021–2035 | s2cid = 10190144 }}

* {{Cite book |first=Donald E. |last=Knuth |author-link=Donald Knuth|title=The Art of Computer Programming |volume=4B: Combinatorial Algorithms, Part 2 |pages=185–369 |chapter=Chapter 7.2.2.2: Satifiability|year=2022 |publisher=Addison-Wesley Professional |isbn=978-0-201-03806-4|title-link=The Art of Computer Programming }}

{{refend}}

{{Logic}}

{{DEFAULTSORT:Boolean Satisfiability Problem}}

[[Category:Boolean algebra]]

[[Category:Electronic design automation]]

[[Category:Formal methods]]

[[Category:Logic in computer science]]

[[Category:NP-complete problems]]

[[Category:Satisfiability problems]]

[[Category:Logic in computer science]]

[[Category:Formal methods]]

[[Category:Electronic design automation]]

[[Category:Boolean algebra]]

[[de:Erfüllbarkeitsproblem der Aussagenlogik]]

[[es:Problema de satisfacibilidad booleana]]

[[eo:Bulea plenumebloproblemo]]

[[fr:Problème SAT]]

[[ko:충족 가능성 문제]]

[[it:Soddisfacibilità booleana]]

[[he:בעיית הספיקות]]

[[ja:充足可能性問題]]

[[pl:Problem spełnialności]]

[[ru:Задача выполнимости булевых формул]]

[[sr:САТ проблем]]

[[th:ปัญหาความสอดคล้องแบบบูล]]

[[uk:Задача здійсненностіі бульових формул]]

[[zh:布尔可满足性问题]]