Editing 2-satisfiability (section)

===NL-completeness===
A nondeterministic algorithm for determining whether a 2-satisfiability instance is ''not'' satisfiable, using only a [[logarithm]]ic amount of writable memory, is easy to describe: simply choose (nondeterministically) a variable ''v'' and search (nondeterministically) for a chain of implications leading from ''v'' to its negation and then back to ''v''. If such a chain is found, the instance cannot be satisfiable. By the [[Immerman–Szelepcsényi theorem]], it is also possible in nondeterministic logspace to verify that a satisfiable 2-satisfiability instance is satisfiable.

2-satisfiability is [[NL-complete]],<ref>{{citation
 | last = Papadimitriou | first = Christos H.
 | author-link = Christos Papadimitriou
 | title = Computational Complexity
 | pages = chapter 4.2
 | publisher = Addison-Wesley
 | year = 1994
 | isbn = 978-0-201-53082-7}}., Thm. 16.3.</ref> meaning that it is one of the "hardest" or "most expressive" problems in the [[complexity class]] '''[[NL (complexity)|NL]]''' of problems solvable nondeterministically in logarithmic space. Completeness here means that a deterministic Turing machine using only logarithmic space can transform any other problem in '''NL''' into an equivalent 2-satisfiability problem.  Analogously to similar results for the more well-known complexity class ''[[NP (complexity)|NP]]'', this transformation together with the Immerman–Szelepcsényi theorem allow any problem in NL to be represented as a [[second order logic]] formula with a single existentially quantified predicate with clauses limited to length 2. Such formulae are known as SO-Krom.<ref name="ck04">{{citation
 | last1 = Cook | first1 = Stephen | author1-link = Stephen Cook
 | last2 = Kolokolova | first2 = Antonina
 | doi = 10.1109/LICS.2004.1319634
 | title = 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
 | pages = 398–407
 | contribution = A Second-Order Theory for NL
 | year = 2004| isbn = 978-0-7695-2192-3 | s2cid = 9936442 }}.</ref>  Similarly, the [[implicative normal form]] can be expressed in [[first order logic]] with the addition of an operator for [[transitive closure]].<ref name="ck04"/>