Unsatisfiable core

From Wikipedia, the free encyclopedia

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[1].

An unsatisfiable core is called a minimal unsatisfiable core, if it becomes satisfiable if any one of its clauses is removed. This is a local minimum, and there are several practical methods of computing them.[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[1].

[edit] References

  1. ^ a b L. Zhang and S. Malik, Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formulas
  2. ^ N. Dershowitz, Z. Hanna, and A. Nadel, A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
\lnot(p\land\lnot p)  This logic-related article is a stub. You can help by expanding it.