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)

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

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)