Editing Boolean satisfiability problem (section)

==Definitions==
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===

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

For example, {{math|size=100%|''x''<sub>1</sub>}} is a positive literal, {{math|size=100%|¬''x''<sub>2</sub>}} is a negative literal, and {{math|size=100%|''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>}} is a clause. The formula {{math|size=100%|(''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>) ∧ (¬''x''<sub>1</sub> ∨ ''x''<sub>2</sub> ∨ ''x''<sub>3</sub>) ∧ ¬''x''<sub>1</sub>}} 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''<sub>1</sub>&nbsp;=&nbsp;FALSE, ''x''<sub>2</sub>&nbsp;=&nbsp;FALSE, and ''x''<sub>3</sub> arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ ''x''<sub>3</sub>) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ ''x''<sub>3</sub>) ∧ 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.

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''<sub>1</sub>,...,''l''<sub>''n''</sub>)}} for some [[Boolean function]] ''R'' and (ordinary) literals {{mvar|''l''<sub>''i''</sub>}}. 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.
<!---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.--->

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''<sub>1</sub>∧''y''<sub>1</sub>) ∨ (''x''<sub>2</sub>∧''y''<sub>2</sub>) ∨ ... ∨ (''x''<sub>''n''</sub>∧''y''<sub>''n''</sub>) into conjunctive normal form yields
{{block indent|{{math|(''x''<sub>1</sub>&nbsp;∨&nbsp;''x''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''<sub>''n''</sub>) ∧}}}}
{{block indent|{{math|(''y''<sub>1</sub>&nbsp;∨&nbsp;''x''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''<sub>''n''</sub>) ∧}}}}
{{block indent|{{math|(''x''<sub>1</sub>&nbsp;∨&nbsp;''y''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''<sub>''n''</sub>) ∧}}}}
{{block indent|{{math|(''y''<sub>1</sub>&nbsp;∨&nbsp;''y''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''<sub>''n''</sub>) ∧ ... ∧}}}}
{{block indent|{{math|(''x''<sub>1</sub>&nbsp;∨&nbsp;''x''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''<sub>''n''</sub>) ∧}}}}
{{block indent|{{math|(''y''<sub>1</sub>&nbsp;∨&nbsp;''x''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''<sub>''n''</sub>) ∧}}}}
{{block indent|{{math|(''x''<sub>1</sub>&nbsp;∨&nbsp;''y''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''<sub>''n''</sub>) ∧}}}}
{{block indent|{{math|(''y''<sub>1</sub>&nbsp;∨&nbsp;''y''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''<sub>''n''</sub>)}};}}
while the former is a disjunction of ''n'' conjunctions of 2 variables, the latter consists of 2<sup>''n''</sup> 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.