Model-Based Diagnosis with Multiple Observations
Authors: Alexey Ignatiev, Antonio Morgado, Georg Weissenbacher, Joao Marques-Silva
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | This section evaluates three approaches to MBD with multiple failing observations: the Diag Combine approach of [Lamraoui and Nakajima, 2014; Lamraoui and Nakajima, 2016], its improved version implementing the ideas of Section 3.2, and, finally, the approach based on hitting set dualization (see Section 4). The experiments were performed in Ubuntu Linux on an Intel Xeon E5-2630 2.60GHz processor with 64GByte of memory. The time and memory limits for each individual instance were 1800s and 10GByte, respectively. |
| Researcher Affiliation | Academia | 1 Faculty of Science, University of Lisbon, Portugal 2 TU Wien, Vienna, Austria 3 ISDCT SB RAS, Irkutsk, Russia |
| Pseudocode | Yes | Algorithm 1: Enumeration of minimal diagnoses |
| Open Source Code | Yes | The implementation of the considered approaches as well as all the benchmarks used are available online at https://github.com/alexeyignatiev/mbd-mobs. |
| Open Datasets | Yes | The test instances build on the ISCAS85 benchmark suite [Brglez and Fujiwara, 1985]. |
| Dataset Splits | No | The paper describes how "100 unique observations" were generated for each faulty circuit and states "The number of benchmark instances generated in this non-exhaustive way is 144." However, it does not specify any explicit train/validation/test dataset splits (e.g., percentages or sample counts) for its experiments. |
| Hardware Specification | Yes | The experiments were performed in Ubuntu Linux on an Intel Xeon E5-2630 2.60GHz processor with 64GByte of memory. |
| Software Dependencies | Yes | The consistency checks are done using the Glucose 3 SAT solver [Audemard et al., 2013]. [...] Both tools make use of the LBX algorithm [Menc ıa et al., 2015] for doing exhaustive enumeration of the individual diagnoses for each failing observation. [...] enumeration of cardinality-minimal hitting sets is achieved with the use OLLITI/RC2 [Morgado et al., 2014; Ignatiev et al., 2018], the best performing Max SAT algorithm from the Max SAT Evaluation 2018. [...] implemented in C++ and consists of two interacting parts. [...] it was written on top of the Py SAT toolkit [Ignatiev et al., 2018] |
| Experiment Setup | Yes | The time and memory limits for each individual instance were 1800s and 10GByte, respectively. [...] HSD is configured to compute cardinality-minimal diagnoses although enumeration of subset-minimal solutions is also supported. [...] A faulty system with its 100 observations was discarded if it had more than 100 minimal aggregated diagnoses, eliminating some faulty systems from the experiment. We emphasize that this filtering was done after the observation generation phase. |