Practical algorithms for unsatisfiability proof and core generation in SAT solvers
Roberto Asín‐Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell · AI Communications · 2010
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