Editing 2-satisfiability (section)

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