Towards efficient MUS extraction

DOI10.3233/AIC-2012-0523MaRDI QIDQ3164969zbMATH OpenOpenAlexFDO

Authors Anton Belov, Inês Lynce, Joao Marques-Silva

Publication date 25 October 2012

Published in AI Communications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/aic-2012-0523

zbMATH Keywords

Boolean satisfiabilityminimally unsatisfiable subformula

Mathematics Subject Classification ID

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

Recommendations

• On improving MUS extraction algorithms
• MUSer2: an efficient MUS extractor
• Theory and Applications of Satisfiability Testing
• Efficient combination of decision procedures for MUS computation
• MUS Extraction Using Clausal Proofs

Cited in

(41)

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• Using local search to find MSSes and MUSes
• Finding all minimal safe inductive sets
• Minimal sets on propositional formulae. Problems and reductions
• Understanding the complexity of axiom pinpointing in lightweight description logics
• On exact selection of minimally unsatisfiable subformulae
• Accelerating predicate abstraction by minimum unsatisfiable cores extraction
• SAT-based rigorous explanations for decision lists
• On computing the union of MUSes
• Local-search extraction of mUSes
• Quantified maximum satisfiability
• MCS Extraction with Sublinear Oracle Queries
• Efficient reasoning for inconsistent Horn formulae
• On efficient computation of variable MUSes
• On improving MUS extraction algorithms
• Propositional SAT solving
• On computing preferred MUSes and MCSes
• MUSer2: an efficient MUS extractor
• Speeding up MUS extraction with preprocessing and chunking
• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
• SAT-Based Formula Simplification
• Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
• A new approach to partial MUS enumeration
• SAT-Based Horn Least Upper Bounds
• Efficient combination of decision procedures for MUS computation
• Algorithms for computing minimal equivalent subformulas
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• On Tackling Explanation Redundancy in Decision Trees
• MUPS identification based on discrimination rules
• Formula preprocessing in MUS extraction
• Parallel MUS extraction
• Factoring Out Assumptions to Speed Up MUS Extraction
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• An automata view to goal-directed methods
• FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets
• Anytime approximate formal feature attribution
• Explanations of unsatisfiability beyond minimal subsets
• Counting minimal unsatisfiable subsets
• On getting rid of the preprocessing minimization step in MUC-finding algorithms

This page was built for publication: Towards efficient MUS extraction

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