Local-search extraction of mUSes

DOI10.1007/S10601-007-9019-7MaRDI QIDQ2385174zbMATH OpenOpenAlexWikidataFDO

Authors E. Grégoire, Bertrand Mazure, Cedric Piette

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

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

Recommendations

• Using local search to find MSSes and MUSes
• Towards efficient MUS extraction
• Finding a collection of MUSes incrementally
• On improving MUS extraction algorithms
• MUSer2: an efficient MUS extractor
• On computing the union of MUSes
• Mechanisms for local search
• Maxima units search (MUS) algorithm: methodology and applications
• Local search algorithms for the composite retrieval problem

Cites work

• scientific article; zbMATH DE number 1943828 (Why is no real title available?)
• A machine program for theorem-proving
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• Boosting complete techniques thanks to local search methods
• Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
• Checking depth-limited consistency and inconsistency in knowledge-based systems
• On exact selection of minimally unsatisfiable subformulae
• On subclasses of minimal unsatisfiable formulas
• On the complexity of propositional knowledge base revision, updates, and counterfactuals
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• The complexity of facets resolved
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(13)

• Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases
• Resolution proof transformation for compression and interpolation
• Finding Guaranteed MUSes Fast
• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A framework for handling logical inconsistencies in the fusion of Boolean knowledge bases
• Approximate counting of minimal unsatisfiable subsets
• Efficient combination of decision procedures for MUS computation
• Does This Set of Clauses Overlap with at Least One MUS?
• An approach for extracting a small unsatisfiable core
• Using local search to find MSSes and MUSes
• THE LANDSCAPE OF INCONSISTENCY: A PERSPECTIVE
• On improving MUS extraction algorithms
• MUST: Provide a Finer-Grained Explanation of Unsatisfiability

Describes a project that uses

Uses Software

• AMUSE
• MUP

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

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