Editing Boolean satisfiability problem (section)

===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.]]
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''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''n''</sub>}} to a conjunction of {{math|''n'' - 2}} clauses

{{block indent|{{math|(''l''<sub>1</sub> ∨ ''l''<sub>2</sub> ∨ ''x''<sub>2</sub>) ∧ }}}}
{{block indent|{{math|(¬''x''<sub>2</sub> ∨ ''l''<sub>3</sub> ∨ ''x''<sub>3</sub>) ∧ }}}}
{{block indent|{{math|(¬''x''<sub>3</sub> ∨ ''l''<sub>4</sub> ∨ ''x''<sub>4</sub>) ∧ ⋯ ∧ }}}}
{{block indent|{{math|(¬''x''<sub>''n''−3</sub> ∨ ''l''<sub>''n''−2</sub> ∨ ''x''<sub>''n''−2</sub>) ∧ }}}}
{{block indent|{{math|(¬''x''<sub>''n''−2</sub> ∨ ''l''<sub>''n''−1</sub> ∨ ''l''<sub>''n''</sub>)}}}}

where {{math|''x''<sub>2</sub>,&thinsp;⋯&thinsp;,&thinsp;''x''<sub>''n''−2</sub>}} 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}}

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}}

There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)<sup>''n''</sup> 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>

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'').

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>

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.

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''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''j''</sub>}} with ''j'' < ''k'' literals can be padded with fixed dummy variables to {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''j''</sub> ∨ ''d''<sub>''j''+1</sub> ∨ ⋯ ∨ ''d''<sub>''k''</sub>}}. After padding all clauses, 2<sup>''k''</sup>–1 extra clauses{{efn|viz. all [[Canonical form (Boolean algebra)#Maxterms|maxterms]] that can be built with {{math|''d''<sub>1</sub>,⋯,''d''<sub>''k''</sub>}}, except {{math|''d''<sub>1</sub>∨⋯∨''d''<sub>''k''</sub>}}}} must be appended to ensure that only {{math|1=''d''<sub>1</sub> = ⋯ = ''d''<sub>''k''</sub> = 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''}}.