Algorithm for 2-Satisfiability problem

Question

Can anyone explain the algorithm for 2-satisfiability problem or provide me the links for the same? I could not find good links to understand it.

Answer 1

You can solve it with greedy approach. Or using Graph theory, here is link with explains solution with graph tehory: http://www.cs.tau.ac.il/~safra/Complexity/2SAT.ppt

Answer 2

Here is the Wikipedia page on the subject, which describes a polynomial time algorithm. (The brute force algorithm of just trying all the different truth assignments is exponential time.) Maybe a bit of further explanation will help.

The expression "if P then Q" is only false when P is true and Q is false. So the expression has the same truth table values as "Q or not P". It is also equivalent to its contrapositive, "if not Q then not P", and that in turn is equivalent to "not P or Q" (the same as the other one).

So the algorithm involves replacing every expression of the form "A or B", with the two expressions, "if not A then B" and "if not B then A". (Putting it another way, A and B can't both be false.)

Next, construct a graph representing these implications. Create nodes for each "A" and "not A", and add links for each of the implications obtained above.

The last step is to make sure that none of the variables is equivalent to its own negation. That is, for each variable A (or not A), follow the links to discover all the nodes that can be reached from it, taking care to detect loops.

If one of the variables, A, can reach "not A", and "not A" can also reach A, then the original expression is not satisfiable. (It is a paradox.) If none of the variables do this, then it is satisfiable.

(It's okay if A implies "not A", but not the other way around. That just means that A must be negated to satisfy the expression.)

Answer 3

If you have n variables and m clauses:

Create a graph with 2n vertices: intuitively, each vertex resembles a true or not true literal for each variable. For each clause (a v b), where a and b are literals, create an edge from !a to b and from !b to a. These edges mean that if a is not true, then b must be true and vica-versa.

Once this digraph is created, go through the graph and see if there is a cycle that contains both a and !a for some variable a. If there is, then the 2SAT is not satisfiable (because a implies !a and vica-versa). Otherwise, it is satisfiable, and this can even give you a satisfying assumption (pick some literal a so that a doesn't imply !a, force all implications from there, repeat). You can do this part with any of your standard graph algorithms, ala Breadth-First Search , Floyd-Warshall, or any algorithm like these, depending on how sensitive you are to the time complexity of your algorithm.