Subsumption-driven clause learning with DPLL+restarts

Complete SAT solvers make deductions until they find a model or produce the empty clause. In DPLL and CDCL solvers, these deductions are produced using assumptions generally called decisions. In DPLL solvers [DLL62], the knowledge accumulated since the beginning of the search is represented by the phases of decision literals. Each new conflict induced by decisions increases the amount of information being accumulated. This amount of information can be interpreted as a proportion of search space already explored that is known not to contain a model.