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