A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

DOI10.1007/11814948_5zbMath1187.68538arXivcs/0605085OpenAlexW1630321466MaRDI QIDQ5756585

Ziyad Hanna, Nachum Dershowitz, Alexander Nadel

Publication date: 4 September 2007

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/cs/0605085

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (15)

Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ Speeding up MUS Extraction with Preprocessing and Chunking ⋮ Mining Backbone Literals in Incremental SAT ⋮ Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ Propositional SAT Solving ⋮ Finding Guaranteed MUSes Fast ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Explaining counterexamples using causality ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Resolution proof transformation for compression and interpolation ⋮ On Improving MUS Extraction Algorithms ⋮ Faster Extraction of High-Level Minimal Unsatisfiable Cores ⋮ An approach for extracting a small unsatisfiable core ⋮ Detecting Inconsistencies in Large Biological Networks with Answer Set Programming ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores

Uses Software

• MiniSat
• Zchaff2004
• Chaff
• BerkMin
• MUP
• AMUSE
• Velev SAT Benchmarks

This page was built for publication: A Scalable Algorithm for Minimal Unsatisfiable Core Extraction