Efficient Model Based Diagnosis with Maximum Satisfiability

Alexey Ignatiev

FC, University of Lisbon


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 our recent work on this topic, 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.

Tuesday, May 31 2016