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

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.

Answer 2

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