3.4 Implication Graph and Conflicts

Unit propagation can be naturally associated with an implication graph that captures all possible ways of deriving all implied literals from decision literals.

Definition 6   The implication graph G at a given stage of DPLL is a directed acyclic graph with edges labeled with sets of clauses. It is constructed as follows:

1. Create a node for each decision literal, labeled with that literal. These will be the indegree zero source nodes of G.

2. While there exists a known clause C = (l₁ $\vee$...l_k $\vee$ l ) such that $\neg$l₁,...,$\neg$l_k label nodes in G,
   1. Add a node labeled l if not already present in G.

   2. Add edges (l_i, l ), 1$\le$i$\le$k, if not already present.

   3. Add C to the label set of these edges. These edges are thought of as grouped together and associated with clause C.

3. Add to G a special node $\Lambda$. For any variable x which occurs both positively and negatively in G, add directed edges from x and $\neg$x to $\Lambda$.

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 $\neg$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 $\Lambda$.

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.

Definition 7   A conflict graph H is any subgraph of an implication graph with the following properties:

1. H contains $\Lambda$ and exactly one conflict variable.
2. All nodes in H have a path to $\Lambda$.
3. Every node l in H other than $\Lambda$ either corresponds to a decision literal or has precisely the nodes $\neg$l₁,$\neg$l₂,...,$\neg$l_k as predecessors where (l₁ $\vee$ l₂ $\vee$...$\vee$ l_k $\vee$ l ) is a known clause.

Figure 2: A conflict graph along with various learning schemes

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.