Unit propagation can be naturally associated with an implication graph that captures all possible ways of deriving all implied literals from decision literals.
Since all node labels in G are distinct, we identify nodes with the literals labeling them. Any variable x occurring both positively and negatively in G is a conflict variable, and x as well as x are conflict literals. G contains a conflict if it has at least one conflict variable. DPLL at a given stage has a conflict if the implication graph at that stage contains a conflict. A conflict can equivalently be thought of as occurring when the residual formula contains the empty clause .
By definition, an implication graph may not contain a conflict at all, or it may contain many conflict variables and several ways of deriving any single literal. To better understand and analyze a conflict when it occurs, we work with a subgraph of an implication graph, called the conflict graph (see Figure 2), that captures only one among possibly many ways of reaching a conflict from the decision variables using unit propagation.
While an implication graph may or may not contain conflicts, a conflict graph always contains exactly one. The choice of the conflict graph is part of the strategy of the solver. A typical strategy will maintain one subgraph of an implication graph that has properties 2 and 3 from Definition 7, but not property 1. This can be thought of as a unique inference subgraph of the implication graph. When a conflict is reached, this unique inference subgraph is extended to satisfy property 1 as well, resulting in a conflict graph, which is then used to analyze the conflict.