Faster Extraction of High-Level Minimal Unsatisfiable Cores

DOI10.1007/978-3-642-21581-0_15MaRDI QIDQ3007682zbMATH OpenOpenAlexFDO

Authors Vadim Ryvchin, Ofer Strichman

Publication date 17 June 2011

Published in Theory and Applications of Satisfiability Testing - SAT 2011 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-21581-0_15

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Accelerated deletion-based extraction of minimal unsatisfiable cores
• Accelerating predicate abstraction by minimum unsatisfiable cores extraction
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Verification, Model Checking, and Abstract Interpretation
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• An approach for extracting a small unsatisfiable core

Cites work

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Algorithms for computing minimal unsatisfiable subsets of constraints
• An approach for extracting a small unsatisfiable core
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• Finding Guaranteed MUSes Fast
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Temporal induction by incremental SAT solving
• The complexity of facets resolved
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems

Cited in

(21)

• An approach for extracting a small unsatisfiable core
• Accelerating predicate abstraction by minimum unsatisfiable cores extraction
• Speeding up assumption-based SAT
• Quantified maximum satisfiability
• 2QBF: challenges and solutions
• Computing small unsatisfiable cores in satisfiability modulo theories
• Speeding up MUS extraction with preprocessing and chunking
• Hints revealed
• 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
• Debugging design errors by using unsatisfiable cores
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• Anytime answer set optimization via unsatisfiable core shrinking
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• A fast counterexample minimization algorithm with refutation analysis and incremental SAT
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• Verification, Model Checking, and Abstract Interpretation
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets
• Efficient generation of small interpolants in CNF
• On getting rid of the preprocessing minimization step in MUC-finding algorithms

Describes a project that uses

Uses Software

• MiniSat
• AMUSE

This page was built for publication: Faster Extraction of High-Level Minimal Unsatisfiable Cores

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