Algorithms for computing minimal unsatisfiable subsets of constraints
From MaRDI portal
Publication:2471741
DOI10.1007/S10817-007-9084-ZzbMATH Open1154.68510OpenAlexW2020169768MaRDI QIDQ2471741FDOQ2471741
Authors: Karem A. Sakallah, Mark H. Liffiton 
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
Recommendations
Cites Work
- Theory and Applications of Satisfiability Testing
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Consistent subsets of inconsistent systems: structure and behaviour
- Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- A GRASP algorithm to solve the unicost set covering problem
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
- Title not available (Why is that?)
- An Efficient Algorithm for the Transversal Hypergraph Generation
- An efficient implementation of a quasi-polynomial algorithm for generating hypergraph transversals
- Title not available (Why is that?)
Cited In (72)
- Certified SAT solving with GPU accelerated inprocessing
- Abstraction for non-ground answer set programs
- ASP and subset minimality: enumeration, cautious reasoning and MUSes
- Finding boundary elements in ordered sets with application to safety and requirements analysis
- Human-centred feasibility restoration in practice
- Omission-based abstraction for answer set programs
- Hashing-based approximate counting of minimal unsatisfiable subsets
- Efficiently explaining CSPs with unsatisfiable subset optimization
- On using incremental encodings in unsatisfiability-based MaxSAT solving
- Impossibility theorems involving weakenings of expansion consistency and resoluteness in voting
- Towards an automatic proof of the bakery algorithm
- Accelerating parameter synthesis using semi-algebraic constraints
- Computing MUS-based inconsistency measures
- On the query complexity of selecting minimal sets for monotone predicates
- SAT-Based Formula Simplification
- On computing minimal independent support and its applications to sampling and counting
- Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases
- Counting minimal unsatisfiable subsets
- Model enumeration in propositional circumscription via unsatisfiable core analysis
- Recursive online enumeration of all minimal unsatisfiable subsets
- Solving satisfiability problems with preferences
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Fast, flexible MUS enumeration
- Quantified maximum satisfiability
- Finding Guaranteed MUSes Fast
- Algorithms for computing minimal equivalent subformulas
- Analysing sanity of requirements for avionics systems
- Debugging unsatisfiable constraint models
- A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
- Shield synthesis
- BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
- Propositional SAT solving
- Accelerated deletion-based extraction of minimal unsatisfiable cores
- Minimal sets on propositional formulae. Problems and reductions
- Binary constraint satisfaction problems defined by excluded topological minors
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- On Tackling Explanation Redundancy in Decision Trees
- Does This Set of Clauses Overlap with at Least One MUS?
- Measuring inconsistency with constraints for propositional knowledge bases
- Enumerating infeasibility: finding multiple MUSes quickly
- A new approach to partial MUS enumeration
- Tunable online MUS/MSS enumeration
- Responsibility for inconsistency
- A max-term counting based knowledge inconsistency checking strategy and inconsistency measure calculation of fuzzy knowledge based systems
- On the measure of conflicts: an argumentation-based framework
- Iterative and core-guided maxsat solving: a survey and assessment
- Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
- On getting rid of the preprocessing minimization step in MUC-finding algorithms
- Enumerating prime implicants of propositional formulae in conjunctive normal form
- Approximating minimal unsatisfiable subformulae by means of adaptive core search
- Understanding the complexity of axiom pinpointing in lightweight description logics
- Integrating topological proofs with model checking to instrument iterative design
- SAT-based rigorous explanations for decision lists
- FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets
- Speeding up MUS extraction with preprocessing and chunking
- Faster Extraction of High-Level Minimal Unsatisfiable Cores
- On improving MUS extraction algorithms
- Strategyproof social choice when preferences and outcomes may contain ties
- Generalizing Core-Guided Max-SAT
- Algorithms for Computing Minimal Conflicts
- On the minimum consistent subset problem
- Dealing Automatically with Exceptions by Introducing Specificity in ASP
- MCS Extraction with Sublinear Oracle Queries
- PBLib -- a library for encoding pseudo-Boolean constraints into CNF
- On semidefinite least squares and minimal unsatisfiability
- Accelerating predicate abstraction by minimum unsatisfiable cores extraction
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- Methods for solving reasoning problems in abstract argumentation -- a survey
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
- Restoring CSP satisfiability with MaxSAT
- Strong inconsistency
- Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
Uses Software
This page was built for publication: Algorithms for computing minimal unsatisfiable subsets of constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2471741)
