A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
type: Item
instance of: scholarly article
title: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
zbMATH Open document ID: 1181.90291
author: Maher Mneimneh
author: Inês Lynce
author: Zaher Andraus
author: Mark H. Liffiton
author: Joao Marques-Silva
author: Karem A. Sakallah
published in: Constraints
publication date: 2009-11-16T00:00:00Z
Mathematics Subject Classification ID: 90C57
Mathematics Subject Classification ID: 90C10
zbMATH DE Number: 5633630
zbMATH Keywords: Boolean satisfiability
zbMATH Keywords: infeasibility
zbMATH Keywords: MUS
zbMATH Keywords: SMUS
describes a project that uses: MiniSat
describes a project that uses: CEGAR
describes a project that uses: MUP
describes a project that uses: AMUSE
MaRDI profile type: Publication
full work available at URL: s10601-008-9058-8
OpenAlex ID: W1966998067
cites work: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
cites work: Consistent subsets of inconsistent systems: structure and behaviour
cites work: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
cites work: On subclasses of minimal unsatisfiable formulas
cites work: Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
cites work: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
cites work: Theory and Applications of Satisfiability Testing
cites work: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
cites work: Local-search extraction of mUSes
cites work: Q4888830
cites work: Q4326390
cites work: Algorithms for computing minimal unsatisfiable subsets of constraints
cites work: The complexity of facets resolved
cites work: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
DOI: 10.1007/S10601-008-9058-8
description: scientific article; zbMATH DE number 5633630