I'm taking Coursera's Advanced Algorithms and Complexity course as part of the Data-Structures and Algorithms Specialization.
In a lecture, I was introduced to a way of determining the satisfiability of a 2-SAT formula, and finding a satisfying assignment, by translating the formula into an implication graph.
I struggled to understand why the resulting graph is constructed the way it is, and how boolean implication is used to ensure that correspondence between graph and SAT truthiness.
Making the following truth table helped me understand:
If a clause (x, y) is provided in the 2-SAT formula, then we need to enforce that at least one of x or y is true. Otherwise, the clause should evaluate to false and the assignment resulting in our current situation is not one that satisfies the 2-SAT formula provided.
In the image, in the 'x' and 'y' columns on the left contain all the combinations of values that are possible for x and y. The first combination (0,0) is the case we want to make sure always yields false.
In the right 2 columns are two "clauses" created from the combinations of values for x and y. In the left clause, we negate x; in the second, we negate y and swap the positions of x and y within the clause.
According to an implication truth table (above), (1,0) yields false, while any other combination yields true.
Given the way we've constructed the clauses in the 2 right columns, the only time these clauses will be false will be when x and y are 0. This is exactly what we want.
When we create a directed graph from the 2-SAT clauses provided, we represent each of the 2 clauses we create as a directed edge. The first edge goes from the negation of the variable x, to the variable y, and the second one goes from the negation of the variable y is assigned to the variable x.
When examining an edge to verify implication truth-ness, in the case where the current vertex involves negation, we take the negative of whatever value is assigned to the variable corresponding to that vertex.
I think that covers it. I hope this helps others. It took me several attempts to understand, but the struggle to write my thoughts out each time allowed me to make incremental progress towards illumination.