Editing 2-satisfiability (section)

==Complexity and extensions==

===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"/>

===The set of all solutions===
[[File:2SAT median graph.svg|thumb|upright=1.35|The [[median graph]] representing all solutions to the example 2-satisfiability instance whose implication graph is shown above.]]
The set of all solutions to a 2-satisfiability instance has the structure of a [[median graph]], in which an edge corresponds to the operation of flipping the values of a set of variables that are all constrained to be equal or unequal to each other. In particular, by following edges in this way one can get from any solution to any other solution. Conversely, any median graph can be represented as the set of solutions to a 2-satisfiability instance in this way. The median of any three solutions is formed by setting each variable to the value it holds in the [[majority function|majority]] of the three solutions. This median always forms another solution to the instance.<ref>{{citation
 | last1 = Bandelt | first1 = Hans-Jürgen
 | last2 = Chepoi | first2 = Victor
 | contribution = Metric graph theory and geometry: a survey
 | doi = 10.1090/conm/453/08795
 | mr = 2405677
 | pages = 49–86
 | publisher = American Mathematical Society | location = Providence, RI
 | series = Contemporary Mathematics
 | title = Surveys on discrete and computational geometry
 | volume = 453
 | year = 2008| isbn = 978-0-8218-4239-3
 }}. {{citation
 | first1 = F. R. K. | last1 = Chung | author-link1 = Fan Chung
 | first2 = R. L. | last2 = Graham | author-link2 = Ronald Graham
 | first3 = M. E. | last3 = Saks
 | title = A dynamic location problem for graphs
 | url = http://www.math.ucsd.edu/~fan/mypaps/fanpap/101location.pdf
 | journal = [[Combinatorica]] | volume = 9 | year = 1989 | pages = 111–132
 | doi = 10.1007/BF02124674
 | issue = 2| s2cid = 5419897 }}. {{citation
 | last = Feder | first = T.
 | title = Stable Networks and Product Graphs
 | series = Memoirs of the American Mathematical Society
 | volume = 555 | year = 1995}}.</ref>

{{harvtxt|Feder|1994}} describes an algorithm for efficiently listing all solutions to a given 2-satisfiability instance, and for solving several related problems.<ref>{{citation|first=Tomás|last=Feder|title=Network flow and 2-satisfiability|journal=[[Algorithmica]]|volume=11|issue=3|year=1994|pages=291–319|doi=10.1007/BF01240738|s2cid=34194118}}.</ref>
There also exist algorithms for finding two satisfying assignments that have the maximal [[Hamming distance]] from each other.<ref>{{citation|first1=Ola|last1=Angelsmark|first2=Johan|last2=Thapper|contribution=Algorithms for the maximum Hamming distance problem|title=Recent Advances in Constraints|publisher=Springer-Verlag|series=Lecture Notes in Computer Science|volume=3419|year=2005|pages=[https://archive.org/details/recentadvancesin0000join/page/128 128–141]|doi=10.1007/11402763_10|isbn=978-3-540-25176-7|url=https://archive.org/details/recentadvancesin0000join/page/128}}.</ref>

===Counting the number of satisfying assignments===
'''#2SAT''' is the problem of counting the number of satisfying assignments to a given 2-CNF formula. This [[Counting problem (complexity)|counting problem]] is [[Sharp-P-complete|#P-complete]],<ref>{{citation
 | last1 = Valiant | first1 = Leslie G. | author-link = Leslie Valiant
 | year = 1979
 | title = The complexity of enumeration and reliability problems
 | journal = [[SIAM Journal on Computing]]
 | volume=8
 | pages= 410–421
 | doi = 10.1137/0208032
 | issue = 3}}</ref> which implies that it is not solvable in [[polynomial time]] unless [[P versus NP problem|P&nbsp;=&nbsp;NP]]. Moreover, there is no [[Polynomial-time approximation scheme|fully polynomial randomized approximation scheme]] for #2SAT unless [[NP (complexity)|NP]] = [[RP (complexity)|RP]] and this even holds when the input is restricted to monotone 2-CNF formulas, i.e., 2-CNF formulas in which each [[Literal (mathematical logic)|literal]] is a positive occurrence of a variable.<ref>{{citation
 | last1 = Welsh | first1 = Dominic | author1-link = Dominic Welsh
 | last2 = Gale | first2 = Amy
 | year = 2001
 | contribution = The complexity of counting problems
 | title = Aspects of complexity: minicourses in algorithmics, complexity and computational algebra: mathematics workshop, Kaikoura, January 7–15, 2000
 | pages = 115ff}}, Theorem 57.</ref>

The fastest known algorithm for computing the exact number of satisfying assignments to a 2SAT formula runs in time <math>O(1.2377^n)</math>.<ref>{{citation|first1=Vilhelm|last1=Dahllöf|first2=Peter|last2=Jonsson|first3=Magnus|last3=Wahlström|title=Counting models for 2SAT and 3SAT formulae|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=332|issue=1–3|year=2005|pages=265–291|doi=10.1016/j.tcs.2004.10.037}}</ref>
<ref>{{citation|first1=Martin|last1=Fürer|first2=Shiva Prasad|last2=Kasiviswanathan|contribution=Algorithms for counting 2-SAT solutions and colorings with applications|title=Algorithmic Aspects in Information and Management|publisher=Springer-Verlag|series=Lecture Notes in Computer Science|volume=4508|year=2007|pages=47–57|doi=10.1007/978-3-540-72870-2_5|isbn=978-3-540-72868-9|citeseerx=10.1.1.634.4498}}.</ref>
<ref>{{citation|first1=Magnus|last1=Wahlström|contribution=A tighter bound for counting max-weight solutions to 2sat instances|title=International Workshop on Parameterized and Exact Computation|volume=5018|year=2008|pages=202–213|doi=10.1007/978-3-540-79723-4_19|series=Lecture Notes in Computer Science|isbn=978-3-540-79722-7|citeseerx=10.1.1.129.9232}}</ref>

===Random 2-satisfiability instances===

One can form a 2-satisfiability instance at random, for a given number ''n'' of variables and ''m'' of clauses, by choosing each clause uniformly at random from the set of all possible two-variable clauses. When ''m'' is small relative to ''n'', such an instance will likely be satisfiable, but larger values of ''m'' have smaller probabilities of being satisfiable. More precisely, if ''m''/''n'' is fixed as a constant α ≠ 1, the probability of satisfiability tends to a [[Limit of a sequence|limit]] as ''n'' goes to infinity: if α&nbsp;&lt;&nbsp;1, the limit is one, while if α&nbsp;&gt;&nbsp;1, the limit is zero. Thus, the problem exhibits a [[phase transition]] at α&nbsp;=&nbsp;1.<ref>{{citation|first1=Béla|last1=Bollobás|author1-link=Béla Bollobás|first2=Christian|last2=Borgs|first3=Jennifer T.|last3=Chayes|author3-link=Jennifer Tour Chayes|first4=Jeong Han|last4=Kim|first5=David B.|last5=Wilson|title=The scaling window of the 2-SAT transition|journal=Random Structures and Algorithms|volume=18|issue=3|pages=201–256|year=2001|doi=10.1002/rsa.1006|arxiv=math/9909031|s2cid=9954684}}; {{citation|first1=V.|last1=Chvátal|author-link1=Václav Chvátal|first2=B.|last2=Reed|title=Proceedings., 33rd Annual Symposium on Foundations of Computer Science |author2-link=Bruce Reed (mathematician)|contribution=Mick gets some (the odds are on his side)|year=1992|pages=620–627|doi=10.1109/SFCS.1992.267789|isbn=978-0-8186-2900-6|s2cid=5575389}}; {{citation|first=A.|last=Goerdt|title=A threshold for unsatisfiability|journal=[[Journal of Computer and System Sciences]]|volume=53|year=1996|pages=469–486|doi=10.1006/jcss.1996.0081|issue=3|doi-access=free}}.</ref>

===Maximum-2-satisfiability ===<!-- MAX-2-SAT redirects here -->
In the maximum-2-satisfiability problem ('''MAX-2-SAT'''), the input is a formula in [[conjunctive normal form]] with two [[Literal (mathematical logic)|literals]] per clause, and the task is to determine the maximum number of clauses that can be simultaneously satisfied by an assignment. Like the more general [[maximum satisfiability problem]], MAX-2-SAT is [[NP-hard]]. The proof is by reduction from [[Boolean satisfiability problem|3SAT]].<ref>{{citation|year=1976|author1=M. R. Garey|author2=D. S. Johnson|author3=L. J. Stockmeyer|title=Some simplified NP-complete graph problems|journal=Theoretical Computer Science|language=en|volume=1|issue=3|pages=237–267|doi=10.1016/0304-3975(76)90059-1|issn=0304-3975}}; see pp. 4–6</ref>

By formulating MAX-2-SAT as a problem of finding a [[Cut (graph theory)|cut]] (that is, a partition of the vertices into two subsets) maximizing the number of edges that have one endpoint in the first subset and one endpoint in the second, in a graph related to the implication graph, and applying [[semidefinite programming]] methods to this cut problem, it is possible to find in polynomial time an approximate solution that satisfies at least 0.940... times the optimal number of clauses.<ref>{{citation|first1=Michael|last1=Lewin|first2=Dror|last2=Livnar|first3=Uri|last3=Zwick|author3-link=Uri Zwick|contribution=Improved Rounding Techniques for the MAX 2-SAT and MAX DI-CUT Problems|title=Proceedings of the 9th International IPCO Conference on Integer Programming and Combinatorial Optimization|year=2002|pages=67–82|isbn=978-3-540-43676-8|publisher=Springer-Verlag}}</ref> A ''balanced'' MAX 2-SAT instance is an instance of MAX 2-SAT where every variable appears positively and negatively with equal weight. For this problem, Austrin has improved the approximation ratio to <math>\min \left\{(3 - \cos \theta)^{-1} (2 + (2/\pi)\theta) \,:\, \pi/2 \leq \theta \leq \pi \right\} = 0.943...</math>.<ref>{{citation
 | last = Austrin | first = Per
 | contribution = Balanced Max 2-sat Might Not Be the Hardest
 | doi = 10.1145/1250790.1250818
 | isbn = 978-1-59593-631-8
 | location = New York, NY, USA
 | pages = 189–197
 | publisher = ACM
 | title = Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing (STOC '07)
 | year = 2007| s2cid = 2353625
 }}.</ref>

If the [[unique games conjecture]] is true, then it is impossible to approximate MAX 2-SAT, balanced or not, with an [[approximation ratio|approximation constant]] better than 0.943... in polynomial time.<ref>{{citation|first1=Subhash|last1=Khot|author1-link=Subhash Khot|first2=Guy|last2=Kindler|first3=Elchanan|last3=Mossel|first4=Ryan|last4=O'Donnell| author4-link = Ryan O'Donnell (computer scientist)|contribution=Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs?|title=FOCS '04: Proceedings of the 45th Annual IEEE Symposium on Foundations of Computer Science|year=2004|pages=146–154|doi=10.1109/FOCS.2004.49|isbn=978-0-7695-2228-9|publisher=IEEE|citeseerx=10.1.1.126.2295|s2cid=2090495}}</ref> Under the weaker assumption that [[P versus NP problem|P&nbsp;≠&nbsp;NP]], the problem is only known to be inapproximable within a constant better than 21/22 = 0.95454...<ref>{{citation|first=Johan|last=Håstad|author-link=Johan Håstad|title=Some optimal inapproximability results|journal=[[Journal of the ACM]]|volume=48|issue=4|year=2001|pages=798–859|doi=10.1145/502090.502098|citeseerx=10.1.1.638.2808|s2cid=5120748}}.</ref>

Various authors have also explored exponential worst-case time bounds for exact solution of MAX-2-SAT instances.<ref>{{citation|first1=N.|last1=Bansal|first2=V.|last2=Raman|contribution=Upper bounds for MaxSat: further improved|editor1-first=A.|editor1-last=Aggarwal|editor2-first=C.|editor2-last=Pandu Rangan|title=Proc. 10th Conf. Algorithms and Computation, ISAAC'99|series=Lecture Notes in Computer Science|volume=1741|publisher=Springer-Verlag|year=1999|pages=247–258}}; {{citation|first1=Jens|last1=Gramm|first2=Edward A.|last2=Hirsch|first3=Rolf|last3=Niedermeier|first4=Peter|last4=Rossmanith|author3-link=Rolf Niedermeier|title=Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT|journal=[[Discrete Applied Mathematics]]|volume=130|issue=2|year=2003|pages=139–155|doi=10.1016/S0166-218X(02)00402-X}}; {{citation|first1=Arist|last1=Kojevnikov|first2=Alexander S.|last2=Kulikov|contribution=A new approach to proving upper bounds for MAX-2-SAT|title=Proc. 17th ACM-SIAM Symp. Discrete Algorithms|year=2006|pages=11–17|doi=10.1145/1109557.1109559|isbn=978-0-89871-605-4|s2cid=10194873}}</ref>

===Weighted-2-satisfiability===
In the weighted 2-satisfiability problem ('''W2SAT'''), the input is an <math>n</math>-variable 2SAT instance and an integer {{math|''k''}}, and the problem is to decide whether there exists a satisfying assignment in which exactly {{math|''k''}} of the variables are true.<ref name=fg06/>

The W2SAT problem includes as a special case the [[vertex cover problem]], of finding a set of {{mvar|k}} vertices that together touch all the edges of a given undirected graph. For any given instance of the vertex cover problem, one can construct an equivalent W2SAT problem with a variable for each vertex of a graph. Each edge {{math|''uv''}} of the graph may be represented by a 2SAT clause {{math|''u'' ∨ ''v''}} that can be satisfied only by including either {{mvar|u}} or {{mvar|v}} among the true variables of the solution. Then the satisfying instances of the resulting 2SAT formula encode solutions to the vertex cover problem, and there is a satisfying assignment with  {{math|''k''}} true variables if and only if there is a vertex cover with {{math|''k''}} vertices. Therefore, like vertex cover, W2SAT is [[NP-complete]].

Moreover, in [[parameterized complexity]] W2SAT provides a natural [[W(1)|W[1]-complete]] problem,<ref name=fg06>{{Citation
 | last1 = Flum | first1 = Jörg
 | last2 = Grohe | first2 = Martin | author2-link = Martin Grohe
 | doi = 10.1007/3-540-29953-X
 | pages = 69–70
 | title = Parameterized Complexity Theory | year = 2006 | publisher = Springer
 | isbn = 978-3-540-29952-3 }}</ref> which implies that W2SAT is not [[fixed-parameter tractable]] unless  this holds for all problems in [[W(1)|W[1]]]. That is, it is unlikely that there exists an algorithm for W2SAT whose running time takes the form {{math|''f''(''k'')·''n''<sup>''O''(1)</sup>}}. Even more strongly, W2SAT cannot be solved in time {{math|''n''<sup>''o''(''k'')</sup>}} unless the [[exponential time hypothesis]] fails.<ref>{{citation
  |first1=Jianer | last1=Chen
  |first2=Xiuzhen | last2=Huang
  |first3=Iyad A. | last3=Kanj
  |first4=Ge | last4=Xia
  |title=Strong computational lower bounds via parameterized complexity
  |journal=[[Journal of Computer and System Sciences]]
  |volume=72
  |year=2006
  |pages=1346–1367
  |doi=10.1016/j.jcss.2006.04.007
  |issue=8|doi-access=free
  }}</ref>

===Quantified Boolean formulae===
As well as finding the first polynomial-time algorithm for 2-satisfiability, {{harvtxt|Krom|1967}} also formulated the problem of evaluating [[True quantified Boolean formula|fully quantified Boolean formulae]] in which the formula being quantified is a 2-CNF formula. The 2-satisfiability problem is the special case of this quantified 2-CNF problem, in which all quantifiers are [[existential quantifier|existential]]. Krom also developed an effective decision procedure for these formulae. {{harvtxt|Aspvall|Plass|Tarjan|1979}} showed that it can be solved in linear time, by an extension of their technique of strongly connected components and topological ordering.<ref name="Krom1967"/><ref name="APT79"/>

===Many-valued logics===
The 2-satisfiability problem can also be asked for propositional [[many-valued logic]]s. The algorithms are not usually linear, and for some logics the problem is even NP-complete. See {{harvs|last=Hähnle|year=2001|year2=2003|txt}} for surveys.<ref>{{citation|editor1-first=Dov M.|editor1-last=Gabbay|editor2-first=Franz|editor2-last=Günthner|title=Handbook of Philosophical Logic|year=2001|publisher=Springer|isbn=978-94-017-0452-6|pages=297–395|chapter=Advanced many-valued logics|first=Reiner|last=Hähnle|volume=2|doi=10.1007/978-94-017-0452-6_5}} (see in particular [https://books.google.com/books?id=_ol81ow-1s4C&pg=PA373 p.&nbsp;373]); {{citation|editor1-first=Melvin|editor1-last=Fitting|editor2-first=Ewa|editor2-last=Orlowska|editor2-link= Ewa Orłowska |title=Beyond two: theory and applications of multiple-valued logic|year=2003|publisher=Springer|isbn=978-3-7908-1541-2|first=Reiner|last=Hähnle|chapter=Complexity of Many-valued Logics|doi=10.1007/978-3-7908-1769-0_9|series=Studies in Fuzziness and Soft Computing|volume=114|pages=211–233}}</ref>