Editing Boolean satisfiability problem (section)

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