A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

DOI10.1007/s10601-008-9058-8zbMath1181.90291OpenAlexW1966998067MaRDI QIDQ1037642

Maher Mneimneh, Zaher Andraus, Inês Lynce, Mark H. Liffiton, João P. Marques-Silva, Karem A. Sakallah

Publication date: 16 November 2009

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-008-9058-8

zbMATH Keywords

MUSBoolean satisfiabilityinfeasibilitySMUS

Mathematics Subject Classification ID

Integer programming (90C10) Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57)

Related Items (12)

On computing minimal independent support and its applications to sampling and counting ⋮ Quantified maximum satisfiability ⋮ Counting minimal unsatisfiable subsets ⋮ SAT-Based Formula Simplification ⋮ Computing smallest MUSes of quantified Boolean formulas ⋮ Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases ⋮ Accelerating predicate abstraction by minimum unsatisfiable cores extraction ⋮ Faster Extraction of High-Level Minimal Unsatisfiable Cores ⋮ On semidefinite least squares and minimal unsatisfiability ⋮ Unnamed Item ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ SAT-based rigorous explanations for decision lists

Uses Software

• MiniSat
• CEGAR
• MUP
• AMUSE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• The complexity of facets resolved
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On subclasses of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Local-search extraction of mUSes
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Consistent subsets of inconsistent systems: structure and behaviour
• Theory and Applications of Satisfiability Testing
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas