Efficient Model Based Diagnosis with Maximum Satisfiability
Authors: Joao Marques-Silva, Mikoláš Janota, Alexey Ignatiev, Antonio Morgado
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art. |
| Researcher Affiliation | Academia | Joao Marques-Silva INESC-ID, IST, Portugal UCD CASL, Ireland jpms@tecnico.ulisboa.pt Mikol aˇs Janota INESC-ID, IST Lisbon, Portugal mikolas.janota@gmail.com Alexey Ignatiev INESC-ID, IST Lisbon, Portugal aign@sat.inesc-id.pt Antonio Morgado INESC-ID, IST Lisbon, Portugal ajrmorgado@gmail.com |
| Pseudocode | Yes | Algorithm 1: MBD to Max SAT compilation |
| Open Source Code | No | The paper does not provide an explicit statement about the release of its own source code or a link to a repository for the methodology described. |
| Open Datasets | Yes | Most recent papers on approaches for MBD have focused on the ISCAS85 [Brglez and Fujiwara, 1985] problem instances. ... This section proposes the use of the more challenging ITC99 benchmark suite [Corno et al., 2000]. |
| Dataset Splits | No | The paper does not explicitly provide training/test/validation dataset splits. It mentions using ISCAS85 and ITC99 benchmark suites but does not detail the splits used for training, validation, or testing. |
| Hardware Specification | Yes | The experiments were performed on a cluster of Linux servers, each with two Intel Xeon 2.60GHz processors and 64 GByte of physical memory. |
| Software Dependencies | No | The paper mentions software like 'Crypto Mini Sat [Soos et al., 2009]' and 'Glucose [Audemard and Simon, 2009]' (both based on Mini SAT) but does not provide specific version numbers for these or any other ancillary software. |
| Experiment Setup | Yes | For all experiments, the time limit was set to 600s and the memory limit to 4GByte. The experiments focus on the run time for computing one minimal cardinality diagnosis for each scenario. As a result, the preprocessing time of scrypto is not accounted for. Similarly, to guarantee that the Max SAT encoding time is negligible, the number of iterations of Algorithm 1 is limited to 2. |