Counting minimal unsatisfiable subsets

DOI10.1007/978-3-030-81688-9_15MaRDI QIDQ832272zbMATH OpenOpenAlexFDO

Authors Jaroslav Bendík, Kuldeep S. Meel

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81688-9_15

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• Approximate counting of minimal unsatisfiable subsets
• Finding Guaranteed MUSes Fast
• Fast, flexible MUS enumeration
• Towards efficient MUS extraction
• Theory and Applications of Satisfiability Testing

Cites work

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A theory of diagnosis from first principles
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Approximate counting of minimal unsatisfiable subsets
• BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
• Computing maximal autarkies with few and simple oracle queries
• Diagnosing multiple faults
• Fast, flexible MUS enumeration
• Finding a collection of MUSes incrementally
• Formulas free from inconsistency: an atom-centric characterization in Priest's minimally inconsistent LP
• Inconsistency measurement based on variables in minimal unsatisfiable subsets
• Investigations on autark assignments
• MUS Extraction Using Clausal Proofs
• MUSer2: an efficient MUS extractor
• Measuring the blame of each formula for inconsistent prioritized knowledge bases
• On computing minimal independent support and its applications to sampling and counting
• On computing the union of MUSes
• On the evaluation of inconsistency measures
• On the query complexity of selecting minimal sets for monotone predicates
• Quantified maximum satisfiability
• Recursive online enumeration of all minimal unsatisfiable subsets
• Redundancy in logic. I: CNF propositional formulae
• Solving satisfiability in less than \(2^ n\) steps
• Subtractive reductions and complete problems for counting complexity classes
• The Complexity of Enumeration and Reliability Problems
• The complexity of selecting maximal solutions
• Tunable online MUS/MSS enumeration

Cited in

(7)

• Calculating the minimal number of homogeneous objects to represent a plurality in a heterogeneous system of objects
• ASP and subset minimality: enumeration, cautious reasoning and MUSes
• Approximate counting of minimal unsatisfiable subsets
• Hashing-based approximate counting of minimal unsatisfiable subsets
• Minimal enumerations of subsets of a finite set and the middle level problem
• Boolean abstractions for realizability modulo theories
• Computing MUS-based inconsistency measures

Describes a project that uses

Uses Software

• GANAK
• BEACON
• sharpSAT
• MUSer2
• AMUSE
• CEGAR

This page was built for publication: Counting minimal unsatisfiable subsets

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