The problem
In two satisfiability you must assign true or false to many variables so that a list of constraints holds. Each constraint is a clause with two literals joined by or, such as x or not y. The question is whether any assignment satisfies all clauses at once.
Clauses as implications
A clause a or b is equivalent to two implications: if a is false then b must be true, and if b is false then a must be true. Build an implication graph whose nodes are the literals and whose edges are these forced consequences.
Reading the answer
A variable is contradictory when a literal and its negation are forced into the same group of mutually implying nodes, that is the same strongly connected component.
- If a variable and its negation share a component, the formula is unsatisfiable.
- Otherwise an assignment exists, and you can read it off from the component order.
This reduces a logic question to finding strongly connected components, which is a linear time graph routine.
Key idea
Turn each two literal clause into implications, then a variable sharing a component with its negation means no solution exists.