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.L0/0605085.) © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Dershowitz, N., Hanna, Z., & Nadel, A. (2006). A scalable algorithm for minimal unsatisfiable core extraction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4121 LNCS, pp. 36–41). Springer Verlag. https://doi.org/10.1007/11814948_5
Mendeley helps you to discover research relevant for your work.