A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

Nachum Dershowitz, Ziyad Hanna, Alexander Nadel

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 v…