3.1 Unit Propagation and Decision Levels

All clause learning algorithms discussed in this paper are based on unit propagation, which is the process of repeatedly applying the unit clause rule followed by formula simplification until no clause with exactly one unassigned literal remains. In this context, it is convenient to work with residual formulas at different stages of DPLL. Let $\rho$ be the partial assignment at some stage of DPLL on formula F. The residual formula at this stage is obtained by applying unit propagation to the simplified formula F|_$\rho$.

When using unit propagation, variables assigned values through the actual branching process are called decision variables and those assigned values as a result of unit propagation are called implied variables. Decision and implied literals are analogously defined. Upon backtracking, the last decision variable no longer remains a decision variable and might instead become an implied variable depending on the clauses learned so far. The decision level of a decision variable x is one more than the number of current decision variables at the time of branching on x. The decision level of an implied variable is the maximum of the decision levels of decision variables used to imply it. The decision level at any step of the underlying DPLL procedure is the maximum of the decision levels of all current decision variables. Thus, for instance, if the clause learning algorithm starts off by branching on x, the decision level of x is 1 and the algorithm at this stage is at decision level 1.

A clause learning algorithm stops and declares the given formula to be unsatisfiable whenever unit propagation leads to a conflict at decision level zero, i.e. when no variable is currently branched upon. This condition will be referred to in this paper as a conflict at decision level zero.