Content deleted Content added
Line 17:
A clause is called '''[[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, {{math|size=100%|''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>}} is a clause, and {{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 a formula in conjunctive normal form, its 1st and 3rd clause are Horn clauses, but its 2nd clause is not. The formula is satisfiable, choosing ''x''<sub>1</sub> = FALSE, ''x''<sub>2</sub> = 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 and ''a''=FALSE it evaluates to TRUE ∧ ¬TRUE (i.e. to FALSE) and FALSE ∧ ¬FALSE (i.e. again to FALSE), respectively.
For some versions of the SAT problem,
Line 24:
<!---, 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 if exactly one of its arguments is.
<!---need not explain that alread yhere---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'' = ''y'' = ''z'' = 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
:{{math|(''x''<sub>1</sub>∨''x''<sub>2</sub>
:{{math|(''y''<sub>1</sub> ∨ ''x''<sub>2</sub>
:{{math|(''x''<sub>1</sub> ∨ ''y''<sub>2</sub>
:{{math|(''y''<sub>1</sub> ∨ ''y''<sub>2</sub>
:{{math|(''x''<sub>1</sub> ∨ ''x''<sub>2</sub>
:{{math|(''y''<sub>1</sub> ∨ ''x''<sub>2</sub>
:{{math|(''x''<sub>1</sub> ∨ ''y''<sub>2</sub>
:{{math|(''y''<sub>1</sub> ∨ ''y''<sub>2</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.
| |||