Local-search extraction of mUSes

DOI10.1007/s10601-007-9019-7zbMath1211.90307OpenAlexW2073776354WikidataQ126254226 ScholiaQ126254226MaRDI QIDQ2385174

Éric Grégoire, Cédric Piette, Bertrand Mazure

Publication date: 11 October 2007

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-007-9019-7

zbMATH Keywords

local searchSATminimally unsatisfiable subformulas

Mathematics Subject Classification ID

Approximation methods and heuristics in mathematical programming (90C59) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (10)

THE LANDSCAPE OF INCONSISTENCY: A PERSPECTIVE ⋮ A FRAMEWORK FOR HANDLING LOGICAL INCONSISTENCIES IN THE FUSION OF BOOLEAN KNOWLEDGE BASES ⋮ Finding Guaranteed MUSes Fast ⋮ MUST: Provide a Finer-Grained Explanation of Unsatisfiability ⋮ Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases ⋮ Resolution proof transformation for compression and interpolation ⋮ On Improving MUS Extraction Algorithms ⋮ Does This Set of Clauses Overlap with at Least One MUS? ⋮ An approach for extracting a small unsatisfiable core ⋮ A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

Uses Software

• MUP
• AMUSE

Cites Work

• The complexity of facets resolved
• On the complexity of propositional knowledge base revision, updates, and counterfactuals
• Boosting complete techniques thanks to local search methods
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• On exact selection of minimally unsatisfiable subformulae
• On subclasses of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
• Unnamed Item
• Unnamed Item

This page was built for publication: Local-search extraction of mUSes