A 2-satisfiability instance in conjunctive normal form can be transformed into an implication graph by replacing each of its disjunctions by a pair of implications. For example, the statement can be rewritten as the pair . An instance is satisfiable if and only if no literal and its negation belong to the same strongly connected component of its implication graph; this characterization can be used to solve 2-satisfiability instances in linear time.[1]
In CDCL SAT-solvers, unit propagation can be naturally associated with an implication graph that captures all possible ways of deriving all implied literals from decision literals,[2] which is then used for clause learning.
References
^Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979). "A linear-time algorithm for testing the truth of certain quantified boolean formulas". Information Processing Letters. 8 (3): 121–123. doi:10.1016/0020-0190(79)90002-4.
^Paul Beame; Henry Kautz; Ashish Sabharwal (2003). Understanding the Power of Clause Learning (PDF). IJCAI. pp. 1194–1201.