Compiling Model-Based Diagnosis to Boolean Satisfaction
Abstract
This paper introduces an 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 SAT compilation techniques which together provide concise CNF formula. 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 benchmark. Our results open the way to improve the state-of-the-art on a range of similar MBD problems.
Cite
Text
Metodi et al. "Compiling Model-Based Diagnosis to Boolean Satisfaction." AAAI Conference on Artificial Intelligence, 2012. doi:10.1609/AAAI.V26I1.8222Markdown
[Metodi et al. "Compiling Model-Based Diagnosis to Boolean Satisfaction." AAAI Conference on Artificial Intelligence, 2012.](https://mlanthology.org/aaai/2012/metodi2012aaai-compiling/) doi:10.1609/AAAI.V26I1.8222BibTeX
@inproceedings{metodi2012aaai-compiling,
title = {{Compiling Model-Based Diagnosis to Boolean Satisfaction}},
author = {Metodi, Amit and Stern, Roni and Kalech, Meir and Codish, Michael},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2012},
pages = {793-799},
doi = {10.1609/AAAI.V26I1.8222},
url = {https://mlanthology.org/aaai/2012/metodi2012aaai-compiling/}
}