A Scalable Algorithm for Minimal Unsatisfiable Core Extraction | Zendy

Nachum Dershowitz | Zendy; Ziyad Hanna | Zendy; Alexander Nadel | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

Author(s) -

Nachum Dershowitz,

Ziyad Hanna,

Alexander Nadel

Publication year - 2006

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-37206-7

DOI - 10.1007/11814948_5

Subject(s) - computer science , scalability , core (optical fiber) , resolution (logic) , algorithm , multi core processor , theoretical computer science , parallel computing , artificial intelligence , database , telecommunications

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.)

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research