On exact selection of minimally unsatisfiable subformulae

DOI10.1007/s10472-005-0418-4zbMath1099.68105OpenAlexW2073487961MaRDI QIDQ1777390

Renato Bruni

Publication date: 13 May 2005

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-005-0418-4

zbMATH Keywords

satisfiabilityinfeasibility analysisunsatisfiabilityMUS selection

Mathematics Subject Classification ID

Related Items (6)

Local-search extraction of mUSes ⋮ Extending Removed Sets Revision to partially preordered belief bases ⋮ On Improving MUS Extraction Algorithms ⋮ On semidefinite least squares and minimal unsatisfiability ⋮ Dealing Automatically with Exceptions by Introducing Specificity in ASP ⋮ Using local search to find MSSes and MUSes

Uses Software

• Leibniz

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nested satisfiability
• On finding solutions for extended Horn formulas
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Polynomial-time inference of all valid implications for Horn and related formulae
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• The complexity of read-once resolution
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• A short note on some tractable cases of the satisfiability problem.
• A perspective on certain polynomial-time solvable classes of satisfiability
• The arborescence-realization problem
• Detecting IIS in infeasible linear programmes using techniques from goal programming
• Fast Heuristics for the Maximum Feasible Subsystem Problem
• A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Recognizing disguised NR(1) instances of the satisfiability problem
• Identifying Minimally Infeasible Subsystems of Inequalities
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Renaming a Set of Clauses as a Horn Set
• Extended Horn sets in propositional logic
• A class of logic problems solvable by linear programming
• Analyzing Infeasible Mixed-Integer and Integer Linear Programs

This page was built for publication: On exact selection of minimally unsatisfiable subformulae