A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
计算机科学中的逻辑
2020-06-11 v2
摘要
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.
引用
@article{arxiv.cs/0605085,
title = {A Scalable Algorithm for Minimal Unsatisfiable Core Extraction},
author = {Nachum Dershowitz and Ziyad Hanna and Alexander Nadel},
journal= {arXiv preprint arXiv:cs/0605085},
year = {2020}
}