 Implication graphs were originally used for analyzing complex Boolean expressions.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 formula_1 can be rewritten as the pair formula_2.