Algorithms for computing minimal unsatisfiable subsets of constraints

DOI10.1007/s10817-007-9084-zzbMath1154.68510OpenAlexW2020169768MaRDI QIDQ2471741

Publication date: 18 February 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-007-9084-z

zbMATH Keywords

Constraint satisfaction CAMUS Minimal unsatifiable subset

Mathematics Subject Classification ID

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

Related Items

On computing minimal independent support and its applications to sampling and counting, Fast, flexible MUS enumeration, Quantified maximum satisfiability, Integrating Topological Proofs with Model Checking to Instrument Iterative Design, Analysing sanity of requirements for avionics systems, On Tackling Explanation Redundancy in Decision Trees, Counting minimal unsatisfiable subsets, PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF, 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, Propositional SAT Solving, Measuring inconsistency with constraints for propositional knowledge bases, A max-term counting based knowledge inconsistency checking strategy and inconsistency measure calculation of fuzzy knowledge based systems, Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis, Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form, Solving satisfiability problems with preferences, Minimal sets on propositional formulae. Problems and reductions, Understanding the complexity of axiom pinpointing in lightweight description logics, Strategyproof social choice when preferences and outcomes may contain ties, Human-centred feasibility restoration in practice, Responsibility for inconsistency, Model enumeration in propositional circumscription via unsatisfiable core analysis, Finding Guaranteed MUSes Fast, ASP and subset minimality: enumeration, cautious reasoning and MUSes, FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets, Shield synthesis, Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases, Algorithms for computing minimal equivalent subformulas, Accelerating predicate abstraction by minimum unsatisfiable cores extraction, On Improving MUS Extraction Algorithms, Faster Extraction of High-Level Minimal Unsatisfiable Cores, Enhancing unsatisfiable cores for LTL with information on temporal relevance, On semidefinite least squares and minimal unsatisfiability, Debugging unsatisfiable constraint models, Does This Set of Clauses Overlap with at Least One MUS?, On the measure of conflicts: an argumentation-based framework, Omission-Based Abstraction for Answer Set Programs, Abstraction for non-ground answer set programs, MCS Extraction with Sublinear Oracle Queries, BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies, Generalizing Core-Guided Max-SAT, Dealing Automatically with Exceptions by Introducing Specificity in ASP, Strong inconsistency, A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas, Methods for solving reasoning problems in abstract argumentation -- a survey, Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores, On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving, Iterative and core-guided maxsat solving: a survey and assessment, On the query complexity of selecting minimal sets for monotone predicates, SAT-based rigorous explanations for decision lists

Uses Software

Cites Work