A Novel SAT-Based Approach to Model Based Diagnosis
Abstract
This paper introduces a novel encoding of Model Based Diagnosis (MBD) to Boolean Satisfaction (SAT) focusing on minimal cardinality diagnosis. The encoding is based on a combination of sophisticated MBD preprocessing algorithms and the application of a SAT compiler which optimizes the encoding to provide more succinct CNF representations than obtained with previous works. Experimental evidence indicates that our approach is superior to all published algorithms for minimal cardinality MBD. In particular, we can determine, for the first 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.
Cite
Text
Metodi et al. "A Novel SAT-Based Approach to Model Based Diagnosis." Journal of Artificial Intelligence Research, 2014. doi:10.1613/JAIR.4503Markdown
[Metodi et al. "A Novel SAT-Based Approach to Model Based Diagnosis." Journal of Artificial Intelligence Research, 2014.](https://mlanthology.org/jair/2014/metodi2014jair-novel/) doi:10.1613/JAIR.4503BibTeX
@article{metodi2014jair-novel,
title = {{A Novel SAT-Based Approach to Model Based Diagnosis}},
author = {Metodi, Amit and Stern, Roni and Kalech, Meir and Codish, Michael},
journal = {Journal of Artificial Intelligence Research},
year = {2014},
pages = {377-411},
doi = {10.1613/JAIR.4503},
volume = {51},
url = {https://mlanthology.org/jair/2014/metodi2014jair-novel/}
}