Efficient Model Based Diagnosis with maximum satisfiability

Joao Marques-Silva, Mikoláš Janota, Alexey Ignatiev, Antonio Morgado

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

32 Citations (Scopus)


Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spreadsheets, web services, and hardware designs, but also the analysis of biological systems, among many others. Motivated by these different uses, there have been significant improvements made to MBD algorithms in recent years. Nevertheless, the analysis of larger and more complex systems motivates further improvements to existing approaches. This paper proposes a novel encoding of MBD into maximum satisfiability (MaxSAT). The new encoding builds on recent work on using Propositional Satisfiability (SAT) for MBD, but identifies a number of key optimizations that are very effective in practice. The paper also proposes a new set of challenging MBD instances, which can be used for evaluating new MBD approaches. Experimental results obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art.

Original languageEnglish
Title of host publicationProceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence
EditorsQiang Yang, Michael Wooldridge
Place of PublicationPalo Alto CA USA
PublisherAssociation for the Advancement of Artificial Intelligence (AAAI)
Number of pages7
ISBN (Electronic)9781577357384
Publication statusPublished - 2015
Externally publishedYes
EventInternational Joint Conference on Artificial Intelligence 2015 - Buenos Aires, Argentina
Duration: 25 Jul 20151 Aug 2015
Conference number: 24th


ConferenceInternational Joint Conference on Artificial Intelligence 2015
Abbreviated titleIJCAI 2015
CityBuenos Aires
Internet address

Cite this