Efficient model based diagnosis with maximum satisfiability
João P. Marques-Silva, Mikoláš Janota, Alexey Ignatiev, António Morgado · 2015
Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spread-sheets, 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 moti-vates further improvements to existing approaches. This paper proposes a novel encoding of MBD into maximum satisfiability (MaxSAT). The new encod-ing builds on recent work on using Propositional Satisfiability (SAT) for MBD, but identifies a num-ber 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 re-sults obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art. 1