A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

DOI10.1007/11814948_5MaRDI QIDQ5756585zbMATH OpenOpenAlexFDO

Authors Nachum Dershowitz, Ziyad Hanna, 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)

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.

Recommendations

• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• An approach for extracting a small unsatisfiable core
• Algorithms for computing minimal unsatisfiable subsets of constraints
• On improving MUS extraction algorithms

Cited in

(25)

• An approach for extracting a small unsatisfiable core
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• Accelerating predicate abstraction by minimum unsatisfiable cores extraction
• MCS Extraction with Sublinear Oracle Queries
• Computing small unsatisfiable cores in satisfiability modulo theories
• On improving MUS extraction algorithms
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Propositional SAT solving
• Speeding up MUS extraction with preprocessing and chunking
• Mining backbone literals in incremental SAT. A new kind of incremental data
• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
• Finding Guaranteed MUSes Fast
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Explaining counterexamples using causality
• Anytime answer set optimization via unsatisfiable core shrinking
• Algorithms for computing minimal equivalent subformulas
• Resolution proof transformation for compression and interpolation
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• Integrating topological proofs with model checking to instrument iterative design
• Detecting Inconsistencies in Large Biological Networks with Answer Set Programming
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• Verification, Model Checking, and Abstract Interpretation
• Efficiently explaining CSPs with unsatisfiable subset optimization
• Conflict-free electric vehicle routing problem: an improved compositional algorithm

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756585)