Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
A Novel SAT-Based Approach to Model Based Diagnosis
Authors: A. Metodi, R. Stern, M. Kalech, M. Codish
JAIR 2014 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental evidence indicates that our approach is superior to all published algorithms for minimal cardinality MBD. In particular, we can determine, for the ๏ฌrst time, minimal cardinality diagnoses for the entire standard ISCAS-85 and 74XXX benchmarks. Our results open the way to improve the state-of-the-art on a range of similar MBD problems. |
| Researcher Affiliation | Academia | Amit Metodi EMAIL Department of Computer Science, Ben Gurion University of the Negev, Beer-Sheva, Israel Roni Stern EMAIL Meir Kalech EMAIL Department of Information Systems Engineering, Ben Gurion University of the Negev, Beer-Sheva, Israel Michael Codish EMAIL Department of Computer Science, Ben Gurion University of the Negev, Beer-Sheva, Israel |
| Pseudocode | Yes | Algorithm 1 partitioning a system into sections Algorithm 2 dominators (component c, section S, system C) Algorithm 3 Find a diagnosis (and upper bound | | on min. card.) |
| Open Source Code | Yes | The entire set of our tools, range of benchmarks, as well as a more detailed report of the results can be found online (Metodi, 2012a; Metodi, Stern, Kalech, & Codish, 2012b). Metodi, A. (2012a). SCryptodiagnoser: A SAT based MBD solver. http://amit.metodi. me/research/mbdsolver. Metodi, A. (2012b). SCryptominisat. http://amit.metodi.me/research/scrypto. Metodi, A., Stern, R., Kalech, M., & Codish, M. (2012b). Compiling model-based diagnosis to Boolean satisfaction: Detailed experimental results and prototype implementation. http: //www.cs.bgu.ac.il/ mcodish/Papers/Pages/aaai-2012.html. |
| Open Datasets | Yes | We evaluated our SAT-based approach using two standard benchmarks: ISCAS-85 (Brglez, Bryan, & Kozminski, 1989) and 74XXX. These are the standard benchmarks in the MBD literature, used extensively from the time they were made available until today (Feldman & van Gemund, 2006; Feldman et al., 2010a; Siddiqi & Huang, 2007, 2011; Stern, Kalech, Feldman, & Provan, 2012; Nica, Pill, Quaritsch, & Wotawa, 2013). |
| Dataset Splits | No | The paper uses predefined 'observation sets' (Feldman, DXC-09, Siddiqi) as test cases for diagnostic problems, but these do not represent traditional training/validation/test dataset splits typically described in machine learning contexts for model training. |
| Hardware Specification | Yes | All experiments were run on an Intel Core 2 Duo (E8400 3.00GHz CPU, 4GB memory) under Linux (Ubuntu lucid, kernel 2.6.32-24-generic) unless stated otherwise. |
| Software Dependencies | Yes | Our decision to model the relation between a component c and its health variable Hc by introducing an additional xor gate...the underlying SAT solver that we apply, Crypto Mini Sat (Soos, 2010), offers direct support for xor clauses...The ๏ฌnite domain constraint compiler, BEE (Metodi & Codish, 2012), which we apply... Soos, M. (2010). Cryptominisat, v2.5.1. http://www.msoos.org/cryptominisat2. |
| Experiment Setup | No | The paper describes the overall process and components of the SAT-based approach, including constraint modeling and solution phases, but it does not specify concrete numerical hyperparameters or system-level training settings typically found in experimental setups for machine learning models. |