Proceedings

Efficient Model Based Diagnosis with Maximum Satisfiability

João P. Marques Silva, Mikolás Janota, Alexey Ignatiev, António Morgado

Download BibTeX Cite

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 1966-1971.

Abstract

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.

João P. Marques Silva, Mikolás Janota, Alexey Ignatiev, and Antonio Morgado. 2015. Efficient Model Based Diagnosis with Maximum Satisfiability. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15. IJCAI, 1966–1971. https://ijcai.org/proceedings/2015/279
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards