Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores
Alexander Nadel, Vadim Ryvchin, Ofer Strichman · Journal on Satisfiability Boolean Modeling and Computation · 2014
Various technologies are based on the capability to find small unsatisfiable cores given an unsatisfiable CNF formula, i.e., a subset of the clauses that are unsatisfiable regardless of the rest of the formula. If that subset is irreducible, it is ca