Skip to main navigation Skip to search Skip to main content

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

  • Mark Liffiton
  • , Maher Mneimneh
  • , Inês Lynce
  • , Zaher Andraus
  • , João Marques-Silva
  • , Karem Sakallah

Research output: Journal ArticleArticlepeer-review

Original languageEnglish
Pages (from-to)415-442
Number of pages28
JournalConstraints
Volume14
Issue number4
DOIs
StatePublished - Dec 2009
Externally publishedYes

ASJC Scopus Subject Areas

  • Software
  • Discrete Mathematics and Combinatorics
  • Computational Theory and Mathematics
  • Artificial Intelligence

Keywords

  • Boolean satisfiability
  • Infeasibility
  • Minimal unsatisfiable subformula
  • MUS
  • SAT
  • Smallest minimal unsatisfiable subformula
  • SMUS

Cite this