Alexey Ignatiev

Date: 10:15, Friday, August 14, 2015
Speaker: Alexey Ignatiev
Venue: TU Wien

Time: 10:15, Day: Friday

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.

Posted in RiSE Seminar