Faster Extraction of High-Level Minimal Unsatisfiable Cores

DOI10.1007/978-3-642-21581-0_15zbMath1331.68211OpenAlexW144339668MaRDI QIDQ3007682

Ofer Strichman, Vadim Ryvchin

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

Related Items (11)

Quantified maximum satisfiability ⋮ Speeding up MUS Extraction with Preprocessing and Chunking ⋮ Hints Revealed ⋮ Mining Backbone Literals in Incremental SAT ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets ⋮ On getting rid of the preprocessing minimization step in MUC-finding algorithms ⋮ Accelerating predicate abstraction by minimum unsatisfiable cores extraction ⋮ Efficient generation of small interpolants in CNF ⋮ 2QBF: Challenges and Solutions ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores

Uses Software

• MiniSat
• AMUSE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An approach for extracting a small unsatisfiable core
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• The complexity of facets resolved
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Finding Guaranteed MUSes Fast
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Computer Aided Verification

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