Unsatisfiable core
In mathematical logic, given an unsatisfiable Boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula.
Many SAT solvers can produce a resolution graph which proves the unsatisfiability of the original problem. This can be analyzed to produce a smaller unsatisfiable core.
An unsatisfiable core is called a minimal unsatisfiable core, if every proper subset (allowing removal of any arbitrary clause or clauses) of it is satisfiable. Thus, such a core is a local minimum, though not necessarily a global one. There are several practical methods of computing minimal unsatisfiable cores.[1][2]
A minimum unsatisfiable core contains the smallest number of the original clauses required to still be unsatisfiable. No practical algorithms for computing the minimum core are known. Algorithms for Computing Minimal Unsatisfiable Subsets. Notice the terminology: whereas minimal unsatisfiable core was a local problem with an easy solution, the minimum unsatisfiable core is a global problem with no known easy solution.
References
- ↑ N. Dershowitz, Z. Hanna, and A. Nadel, A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- ↑ Stefan Szeider, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable