Efficient Model Based Diagnosis with Maximum Satisfiability

The research group Formal Methods in Systems Engineering hosted a talk by Alexey Ignatiev on August 14, 2015.

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. The talk will briefly describe a work on this topic done at INESC-ID Lisboa, which 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. Experimental results obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art.