Algorithm Summary

Step $1$: Build the implication graph. For each clause "a OR b", add edges NOT a → b and NOT b → a. You end up with $2n$ nodes and $2m$ edges. Step $2$: Compute SCCs using Kosaraju or Tarjan. Step $3$: Check satisfiability by verifying that no variable x shares an SCC with NOT x.

If any do, return unsatisfiable. Step $4$: Construct assignment. For each variable, set x to true if SCC(x) > SCC(NOT x) in topological order, otherwise set x to false. Output this assignment.