Counting minimal unsatisfiable subsets

DOI10.1007/978-3-030-81688-9_15zbMath1493.68259OpenAlexW3184610995MaRDI QIDQ832272

Jaroslav Bendík, Kuldeep S. Meel

Publication date: 25 March 2022

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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the query complexity of selecting minimal sets for monotone predicates
• On computing minimal independent support and its applications to sampling and counting
• Fast, flexible MUS enumeration
• Quantified maximum satisfiability
• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• Solving satisfiability in less than \(2^ n\) steps
• Diagnosing multiple faults
• A theory of diagnosis from first principles
• Investigations on autark assignments
• The complexity of selecting maximal solutions
• On computing the union of MUSes
• Approximate counting of minimal unsatisfiable subsets
• Redundancy in logic. I: CNF propositional formulae
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Subtractive reductions and complete problems for counting complexity classes
• Finding a Collection of MUSes Incrementally
• BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies
• Measuring the blame of each formula for inconsistent prioritized knowledge bases
• Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency
• MUS Extraction Using Clausal Proofs
• Computing Maximal Autarkies with Few and Simple Oracle Queries
• The Complexity of Enumeration and Reliability Problems
• Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores
• Formulas Free From Inconsistency: An Atom-Centric Characterization in Priest's Minimally Inconsistent LP
• Recursive online enumeration of all minimal unsatisfiable subsets