Towards efficient MUS extraction

DOI10.3233/AIC-2012-0523zbMath1248.68450OpenAlexW1879512746MaRDI QIDQ3164969

Anton Belov, Inês Lynce, João P. 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

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

Related Items (19)

Quantified maximum satisfiability ⋮ On Tackling Explanation Redundancy in Decision Trees ⋮ 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 ⋮ Propositional SAT Solving ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Understanding the complexity of axiom pinpointing in lightweight description logics ⋮ FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets ⋮ On getting rid of the preprocessing minimization step in MUC-finding algorithms ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Accelerating predicate abstraction by minimum unsatisfiable cores extraction ⋮ An Automata View to Goal-Directed Methods ⋮ MCS Extraction with Sublinear Oracle Queries ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ SAT-based rigorous explanations for decision lists

This page was built for publication: Towards efficient MUS extraction