Subsumption-driven clause learning with DPLL+restarts

Olivier Bailleux

We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approac…