A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

Abstract We propose a new algorithm for minimal unsatisfiable core extraction, based on a deeper exploration of resolution-refutation properties. We provide experimental results on formal verification benchmarks confirming that our algorithm finds smaller cores than suboptimal algorithms; and that it runs faster than those algorithms that guarantee minimality of the core. (A more complete version of this paper may be found at arXiv. org/pdf/cs. LO/0605085.)

Authors

• Nachum Dershowitz
• Ziyad Hanna
• Alexander Nadel

Keywords

No keywords are indexed for this paper.