Clause learning (see e.g.,Marques-Silva and Sakallah, 1996) can be thought of as an extension of the DPLL procedure that caches causes of assignment failures in the form of learned clauses. It proceeds by following the normal branching process of DPLL until there is a ``conflict'' after unit propagation. If this conflict occurs when no variable is currently branched upon, the formula is declared unsatisfiable. Otherwise, the ``conflict graph'' is analyzed and the ``cause'' of the conflict is learned in the form of a ``conflict clause.'' The procedure now backtracks and continues as in ordinary DPLL, treating the learned clause just like initial ones. A clause is said to be known at a stage if it is either an initial clause or has previously been learned.
The learning process is expected to save us from redoing the same computation when we later have an assignment that causes conflict due in part to the same reason. Variations of such conflict-driven learning include different ways of choosing the clause to learn (different learning schemes) and possibly allowing multiple clauses to be learned from a single conflict (Zhang et al., 2001). In the last decade, many algorithms based on this idea have been proposed and demonstrated to be empirically successful on large problems that could not be handled using other methodologies (Moskewicz et al., 2001, Bayardo Jr., 1997, Zhang, 1997, Marques-Silva and Sakallah, 1996). We leave a more detailed discussion of the concepts involved in clause learning as well as its formulation as a proof system CL to Section 3.