Practical algorithms for unsatisfiability proof and core generation in SAT solvers

Abstract

Since Zhang and Malik's work in 2003 [19], it is well-known that modern DPLL-based SAT solvers with learning can be instrumented to write a trace on disk from which, if the input is unsatisfiable, a resolution proof can be extracted (and checked), an