Editing 2-satisfiability (section)

==Problem representations==
[[File:Implication graph.svg|thumb|upright=1.35|The implication graph for the example 2-satisfiability instance shown in this section.]]
A 2-satisfiability problem may be described using a [[Boolean expression]] with a special restricted form. It is a [[Logical conjunction|conjunction]] (a Boolean ''and'' operation) of [[Clause (logic)|clauses]], where each clause is a [[disjunction]] (a Boolean ''or'' operation) of two variables or negated variables. The variables or their negations appearing in this formula are known as [[Literal (mathematical logic)|literals]].<ref name="cnf">{{citation|chapter=2. CNF Encodings|pages=75–98|first=Steven|last=Prestwich|title=Handbook of Satisfiability|volume=185|issue=Handbook of Satisfiability|series=Frontiers in Artificial Intelligence and Applications|publisher=IOS Press|editor1-first=Armin|editor1-last=Biere|editor2-first=Marijn|editor2-last=Heule|editor2-link=Marijn Heule|editor3-first=Hans|editor3-last=van Maaren|editor4-first=Toby|editor4-last=Walsh|chapter-url=https://books.google.com/books?id=YVSM3sxhBhcC&pg=PA75|year=2009|doi=10.3233/978-1-58603-929-5-75|isbn=978-1-58603-929-5|s2cid=31666330 }}.</ref> For example, the following formula is in conjunctive normal form, with seven variables, eleven clauses, and 22 literals:
<math display=block>
\begin{align}
&(x_0\lor x_2)\land(x_0\lor\lnot x_3)\land(x_1\lor\lnot x_3)\land(x_1\lor\lnot x_4)\land{} \\
&(x_2\lor\lnot x_4)\land{}(x_0\lor \lnot x_5)\land (x_1\lor\lnot x_5)\land (x_2\lor\lnot x_5)\land{} \\
&(x_3\lor x_6)\land (x_4\lor x_6)\land (x_5\lor x_6).
\end{align}
</math>

The 2-satisfiability problem is to find a [[truth assignment]] to these variables that makes the whole formula true. Such an assignment chooses whether to make each of the variables true or false, so that at least one literal in every clause becomes true. For the expression shown above, one possible satisfying assignment is the one that sets all seven of the variables to true. Every clause has at least one non-negated variable, so this assignment satisfies every clause. There are also 15 other ways of setting all the variables so that the formula becomes true. Therefore, the 2-satisfiability instance represented by this expression is satisfiable.

Formulas in this form are known as 2-CNF formulas. The "2" in this name stands for the number of literals per clause, and "CNF" stands for [[conjunctive normal form]], a type of Boolean expression in the form of a conjunction of disjunctions.<ref name="cnf"/> They are also called Krom formulas, after the work of [[University of California, Davis|UC Davis]] mathematician Melven R. Krom, whose 1967 paper was one of the earliest works on the 2-satisfiability problem.<ref name="Krom1967">{{citation
| last1 = Krom | first1 = Melven R.
| title = The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary
| journal = Zeitschrift für Mathematische Logik und Grundlagen der Mathematik
| volume = 13
| issue = 1–2
| pages = 15–20
| year = 1967
| doi = 10.1002/malq.19670130104
}}.</ref>

Each clause in a 2-CNF formula is [[logical equivalence|logically equivalent]] to an implication from one variable or negated variable to the other. For example, the second clause in the example may be written in any of three equivalent ways:
<math display=block>(x_0\lor\lnot x_3) \;\equiv\; (\lnot x_0\Rightarrow\lnot x_3) \;\equiv\; (x_3\Rightarrow x_0).</math>
Because of this equivalence between these different types of operation, a 2-satisfiability instance may also be written in [[implicative normal form]], in which we replace each ''or'' clause in the conjunctive normal form by the two implications to which it is equivalent.<ref>{{citation|title=Artificial Intelligence: A Modern Approach|page=282|series=Prentice Hall series in artificial intelligence|first1=Stuart Jonathan|last1=Russell|first2=Peter|last2=Norvig|publisher=Prentice Hall|year=2010|isbn=978-0-13-604259-4}}.</ref>

A third, more graphical way of describing a 2-satisfiability instance is as an [[implication graph]]. An implication graph is a [[directed graph]] in which there is one [[vertex (graph theory)|vertex]] per variable or negated variable, and an edge connecting one vertex to another whenever the corresponding variables are related by an implication in the implicative normal form of the instance. An implication graph must be a [[skew-symmetric graph]], meaning that it has a [[graph automorphism|symmetry]] that takes each variable to its negation and reverses the orientations of all of the edges.<ref name="APT79">{{citation
 | last1 = Aspvall | first1 = Bengt
 | last2 = Plass | first2 = Michael F.
 | author-link3 = Robert Tarjan | last3 = Tarjan | first3 = Robert E.
 | title = A linear-time algorithm for testing the truth of certain quantified boolean formulas
 | url = http://www.math.ucsd.edu/~sbuss/CourseWeb/Math268_2007WS/2SAT.pdf
 | journal = [[Information Processing Letters]]
 | volume = 8 | issue = 3 | pages = 121–123 | year = 1979
 | doi = 10.1016/0020-0190(79)90002-4}}.</ref>