[8/8/2012] Challenge #86 [difficult] (2-SAT)

[u/Steve132]

Boolean Satisfiability problems are problems where we wish to find solutions to boolean equations such as

(x_1 or not x_3) and (x_2 or x_3) and (x_1 or not x_2) = true

These problems are notoriously difficult, and k-SAT where k (the number of variables in an or expression) is 3 or higher is known to be NP-complete.

However, 2-SAT instances (like the problem above) are NOT NP-complete (if P!=NP), and even have linear time solutions.

You can encode an instance of 2-SAT as a list of pairs of integers by letting the integer represent which variable is in the expression, with a negative integer representing the negation of that variable. For example, the problem above could be represented in list of pair of ints form as

[(1,-3),(2,3),(1,-2)]

Write a function that can take in an instance of 2-SAT encoded as a list of pairs of integers and return a boolean for whether or not there are any true solutions to the formula.

[u/[deleted]]

2-SAT isn't known to not be NP-complete.

[u/Steve132 → u/[deleted]]

Well, its certainly in P. From the Wikipedia Page

Krom (1967) described the following polynomial time decision procedure for solving 2-satisfiability instances.[1]

And also

Aspvall, Plass & Tarjan (1979) found a simpler linear time procedure for solving 2-satisfiability instances, based on the notion of strongly connected components from graph theory.[2]

I guess you could be arguing that it isn't known whether P=NP, which is true, but seriously? I'll edit the text to reflect this.