A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

TL;DR

This paper introduces a scalable algorithm for extracting minimal unsatisfiable cores using resolution-refutation properties, demonstrating improved efficiency and smaller core sizes in formal verification benchmarks.

Contribution

The paper presents a novel, scalable algorithm for minimal unsatisfiable core extraction that outperforms existing methods in size and speed.

Findings

Finds smaller cores than suboptimal algorithms

Runs faster than algorithms guaranteeing minimality

Effective on formal verification benchmarks

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.