Jump to content

Unsatisfiable core

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by DBeyer (talk | contribs) at 20:59, 12 October 2007. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Given an unsatisfiable boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called unsatisfiable core of the original formula.

See also

References

  • L. Zhang and S. Malik. Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formulas. [1]
  • N. Dershowitz, Z. Hanna, and A. Nadel. A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. [2]
Retrieved from "https://en.wikipedia.org/w/index.php?title=Unsatisfiable_core&oldid=164131451"