More Web Proxy on the site http://driver.im/

Article

Efficient model based diagnosis with maximum satisfiability

Authors:

Joao Marques-Silva,

Mikoláš Janota,

Alexey Ignatiev,

Antonio MorgadoAuthors Info & Claims

IJCAI'15: Proceedings of the 24th International Conference on Artificial Intelligence

Pages 1966 - 1972

Published: 25 July 2015 Publication History

Abstract

Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spreadsheets, web services, and hardware designs, but also the analysis of biological systems, among many others. Motivated by these different uses, there have been significant improvements made to MBD algorithms in recent years. Nevertheless, the analysis of larger and more complex systems motivates further improvements to existing approaches. This paper proposes a novel encoding of MBD into maximum satisfiability (MaxSAT). The new encoding builds on recent work on using Propositional Satisfiability (SAT) for MBD, but identifies a number of key optimizations that are very effective in practice. The paper also proposes a new set of challenging MBD instances, which can be used for evaluating new MBD approaches. Experimental results obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art.

References

[1]

Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77-105, 2013.

Digital Library

[2]

Carlos Ansótegui, Yuri Malitsky, and Meinolf Sellmann. Maxsat by improved instance-specific algorithm configuration. In AAAI, pages 2594-2600, 2014.

[3]

Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In IJCAI, pages 399-404, 2009.

Digital Library

[4]

Andreas Bauer. Simplifying diagnosis using LSAT: A propositional approach to reasoning from first principles. In CPAIOR, pages 49-63, 2005.

Digital Library

[5]

Roberto J. Bayardo Jr. and Joseph Daniel Pehoushek. Counting models using connected components. In AAAI/IAAI, pages 157-162, 2000.

Digital Library

[6]

Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability. IOS Press, 2009.

Digital Library

[7]

F. Brglez and H. Fujiwara. A neutral list of 10 combinational benchmark circuits and a target translator in FORTRAN. In ISCAS, pages 695-698, Jun. 1985.

[8]

Fulvio Corno, Matteo Sonza Reorda, and Giovanni Squillero. RT-level ITC'99 benchmarks and first ATPG results. IEEE Design & Test of Computers, 17(3):44-53, 2000.

Digital Library

[9]

Adnan Darwiche. Model-based diagnosis using structured system descriptions. J. Artif. Intell. Res. (JAIR), 8:165-222, 1998.

Digital Library

[10]

Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608-647, 2001.

Digital Library

[11]

Johan de Kleer and Brian C. Williams. Diagnosing multiple faults. Artif. Intell., 32(1):97-130, 1987.

Digital Library

[12]

Johan de Kleer, Alan K. Mackworth, and Raymond Reiter. Characterizing diagnoses and systems. Artif. Intell., 56(2-3):197-222, 1992.

Digital Library

[13]

Johan de Kleer. Minimum cardinality candidate generation. In DX, pages 397-402, 2009.

[14]

A. Feldman, G. Provan, J. de Kleer, S. Robert, and A. van Gemund. Solving model-based diagnosis problems with Max-SAT solvers and vice versa. In DX, pages 185-192, 2010.

[15]

Birgit Hofer, André Riboira, Franz Wotawa, Rui Abreu, and Elisabeth Getzner. On the empirical evaluation of fault localization techniques for spreadsheets. In FASE, pages 68-82, 2013.

Digital Library

[16]

Mikolás Janota, Inês Lynce, and Joao Marques-Silva. Algorithms for computing backbones of propositional formulae. AI Commun., 28(2):161-177, 2015.

[17]

Manu Jose and Rupak Majumdar. Cause clue clauses: error localization using maximum satisfiability. In PLDI, pages 437-446, 2011.

Digital Library

[18]

Thomas Lengauer and Robert Endre Tarjan. A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst., 1(1):121-141, 1979.

Digital Library

[19]

Ruben Martins, Saurabh Joshi, Vasco M. Manquinho, and Inês Lynce. Incremental cardinality constraints for MaxSAT. In CP, pages 531-548, 2014.

[20]

Amit Metodi and Michael Codish. Compiling finite domain constraints to SAT with BEE. TPLP, 12(4-5):465-483, 2012.

Digital Library

[21]

Amit Metodi, Roni Stern, Meir Kalech, and Michael Codish. Compiling model-based diagnosis to Boolean satisfaction. In AAAI, 2012.

[22]

Amit Metodi, R. Stern, Meir Kalech, and Michael Codish. A novel sat-based approach to model based diagnosis. J. Artif. Intell. Res. (JAIR), 51:377-411, 2014.

Digital Library

[23]

Rémi Monasson, Riccardo Zecchina, Scott Kirkpatrick, Bart Selman, and Lidror Troyansk. Determining computational complexity from characteristic 'phase transitions'. Nature, 400:133-137, July 1999.

[24]

António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and Joao Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 18(4):478-534, 2013.

Digital Library

[25]

Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided maxsat resolution. In AAAI, pages 2717-2723, 2014.

Digital Library

[26]

Iulia Nica and Franz Wotawa. ConDiag - computing minimal diagnoses using a constraint solver. In DX, pages 185-192, 2012.

[27]

Iulia Nica, Ingo Pill, Thomas Quaritsch, and Franz Wotawa. The route to success - a performance comparison of diagnosis algorithms. In IJCAI, 2013.

Digital Library

[28]

Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987.

Digital Library

[29]

Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, and Karem A. Sakallah. Improved design debugging using maximum satisfiability. In FMCAD, pages 13-19, 2007.

Digital Library

[30]

Sajjad Ahmed Siddiqi and Jinbo Huang. Hierarchical diagnosis of multiple faults. In IJCAI, pages 581-586, 2007.

Digital Library

[31]

Sajjad Ahmed Siddiqi. Computing minimum-cardinality diagnoses by model relaxation. In IJCAI, pages 1087-1092, 2011.

Digital Library

[32]

John K. Slaney and Toby Walsh. Backbones in optimization and approximation. In IJCAI, pages 254-259, 2001.

Digital Library

[33]

Alexander Smith, Andreas G. Veneris, Moayad Fahim Ali, and Anastasios Viglas. Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems, 24(10):1606-1621, 2005.

Digital Library

[34]

Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In SAT, pages 244-257, 2009.

Digital Library

[35]

Roni Tzvi Stern, Meir Kalech, Alexander Feldman, and Gregory M. Provan. Exploring the duality in conflict-directed model-based diagnosis. In AAAI, 2012.

Digital Library

[36]

Brian C. Williams and Robert J. Ragno. Conflict-directed A* and its role in model-based embedded systems. Discrete Applied Mathematics, 155(12):1562-1595, 2007.

Digital Library

Cited By

Ouyang JHuang SChi JZhang L(2025)DVRE: dominator-based variables reduction of encoding for model-based diagnosisFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-024-40894-w19:7Online publication date: 1-Jul-2025
https://dl.acm.org/doi/10.1007/s11704-024-40894-w
Zheng GNguyen TBrida SRegis GFrias MAguirre NBagheri H(2021)flackProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00065(637-648)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00065
Ignatiev AMorgado AWeissenbacher GMarques-Silva J(2019)Model-based diagnosis with multiple observationsProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367032.3367190(1108-1115)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367032.3367190
Show More Cited By

Recommendations

Model-based diagnosis of hybrid systems using satisfiability modulo theory
AAAI'19/IAAI'19/EAAI'19: Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence

Currently, detecting and isolating faults in hybrid systems is often done manually with the help of human operators. In this paper we present a novel model-based diagnosis approach for automatically diagnosing hybrid systems. The approach has two parts: ...
Parallel model-based diagnosis on multi-core computers

Model-Based Diagnosis (MBD) is a principled and domain-independent way of analyzing why a system under examination is not behaving as expected. Given an abstract description (model) of the system's components and their behavior when functioning normally,...
Model-aided diagnosis: an inexpensive combination of model-based and case-based condition assessment

Online condition monitoring and diagnosis are being utilized more and more for increasing the reliability and availability of technical systems and to reduce their maintenance costs. Today's model-based diagnosis (MBD) tools are able to detect and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

IJCAI'15: Proceedings of the 24th International Conference on Artificial Intelligence

July 2015

4429 pages

ISBN:9781577357384

Editors:
Qiang Yang
Hong Kong University of Science and Technology
,
Michael Wooldridge
University of Oxford

Sponsors

The International Joint Conferences on Artificial Intelligence, Inc. (IJCAI)

Publisher

AAAI Press

Publication History

Published: 25 July 2015

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ouyang JHuang SChi JZhang L(2025)DVRE: dominator-based variables reduction of encoding for model-based diagnosisFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-024-40894-w19:7Online publication date: 1-Jul-2025
https://dl.acm.org/doi/10.1007/s11704-024-40894-w
Zheng GNguyen TBrida SRegis GFrias MAguirre NBagheri H(2021)flackProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00065(637-648)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00065
Ignatiev AMorgado AWeissenbacher GMarques-Silva J(2019)Model-based diagnosis with multiple observationsProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367032.3367190(1108-1115)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367032.3367190
Grégoire ÉIzza YLagniez J(2018)Boosting MCSes enumerationProceedings of the 27th International Joint Conference on Artificial Intelligence10.5555/3304415.3304601(1309-1315)Online publication date: 13-Jul-2018
https://dl.acm.org/doi/10.5555/3304415.3304601
Liu MOuyang DZhang L(2018)A novel approach for improving quality of health state with difference degree in circuit diagnosisApplied Intelligence10.1007/s10489-018-1214-248:11(4371-4381)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.1007/s10489-018-1214-2
Shchekotykhin KSchmitz TJannach D(2016)Efficient sequential model-based fault-localization with partial diagnosesProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence10.5555/3060621.3060795(1251-1257)Online publication date: 9-Jul-2016
https://dl.acm.org/doi/10.5555/3060621.3060795
Berg JSaikko PJärvisalo M(2016)Subsumed label elimination for maximum satisfiabilityProceedings of the Twenty-second European Conference on Artificial Intelligence10.3233/978-1-61499-672-9-630(630-638)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.3233/978-1-61499-672-9-630

View Options

View options

Figures

Tables

Media

View Table of Conten