Student or educator? Sign up with your school email and get 6 months of Pro free.
CoChat
Sign Up
Cited by 15

The DOI matches its Crossref record.

Model-Based Diagnosis with Multiple Observations

Ignatiev, Alexey, Morgado, Antonio, Weissenbacher, Georg, Marques-Silva, Joao·2019·Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
DOI 10.24963/ijcai.2019/155
Open this paper in CoChat — free account

Abstract

Existing automated testing frameworks require multiple observations to be jointly diagnosed with the purpose of identifying common fault locations. This is the case for example with continuous integration tools. This paper shows that existing solutions fail to compute the set of minimal diagnoses, and as a result run times can increase by orders of magnitude. The paper proposes not only solutions to correct existing algorithms, but also conditions for improving their run times. Nevertheless, the diagnosis of multiple observations raises a number of important computational challenges, which even the corrected algorithms are often unable to cope with. As a result, the paper devises a novel algorithm for diagnosing multiple observations, which is shown to enable significant performance improvements in practice.

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.24963/ijcai.2019/155

Cites

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

No references could be resolved yet.

Research works printed but not linked: 40

  1. L. Ardissono, L. Console, A. Goy, G. Petrone, C. Picardi, M. Segnan, and D. T. Dupré. Co- operative model-based diagnosis of web services. In DX, pages 125-130, 2005.
  2. M. F. Arif, C. Mencía, and J. Marques- Silva. Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. In SAT, pages 324-342, 2015.
  3. G. Audemard, J. Lagniez, and L. Si- mon. Improving Glucose for incremental SAT solving with assumptions: Application to MUS extraction. In SAT, pages 309-317, 2013.
  4. J. Bailey and P. J. Stuckey. Dis- covery of minimal unsatisfiable subsets of constraints us- ing hitting set dualization. In PADL, pages 174-186, 2005.
  5. E. Birnbaum and E. L. Lozinskii. Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell., 15(1):25-46, 2003.
  6. 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.
  7. K. Chandrasekaran, R. M. Karp, E. Moreno-Centeno, and S. Vempala. Algorithms for implicit hitting set problems. In SODA, pages 614- 629, 2011.
  8. J. Davies and F. Bacchus. Solv- ing MAXSAT by solving a sequence of simpler SAT in- stances. In CP, pages 225-239, 2011.
  9. J. de Kleer and B. C. Williams. Diagnosing multiple faults. Artif. Intell., 32(1):97-130, 1987.
  10. J. de Kleer. An improved approach for gen- erating max-fault min-cardinality diagnoses. In DX, pages 247-252, 2008.
  11. A. Feldman, G. M. Provan, and A. J. C. van Gemund. Solving strong-fault diagnostic mod- els by model relaxation. In IJCAI, pages 785-790, 2009.
  12. Feldman et al., 2010a] A. Feldman, G. Provan, J. de Kleer, S. Robert, and A. van Gemund. Solving model-based di- agnosis problems with Max-SAT solvers and vice versa. In DX, pages 185-192, 2010.
  13. É. Grégoire, Y. Izza, and J. Lagniez. Boosting MCSes enumeration. In IJCAI, pages 1309- 1315, 2018.
  14. Huang and Darwiche, 2005] J. Huang and A. Darwiche. On compiling system models for faster and more scalable di- agnosis. In AAAI, pages 300-306, 2005.
  15. A. Ignatiev, A. Previti, M. H. Liffiton, and J. Marques-Silva. Smallest MUS extraction with min- imal hitting set dualization. In CP, pages 173-182, 2015.
  16. Ignatiev et al., 2016a] A. Ignatiev, A. Morgado, and J. Marques-Silva. Propositional abduction with implicit hitting sets. In ECAI, pages 1327-1335, 2016.
  17. Ignatiev et al., 2016b] A. Ignatiev, A. Previti, and J. Marques-Silva. On finding minimum satisfying assignments. In CP, pages 287-297, 2016.
  18. A. Ignatiev, A. Morgado, and J. Marques-Silva. Model based diagnosis of multi- ple observations with implicit hitting sets. CoRR, abs/1707.01972, 2017. · arXiv
  19. A. Ignatiev, A. Morgado, and J. Marques-Silva. PySAT: A Python toolkit for pro- totyping with SAT oracles. In SAT, pages 428-437, 2018.
  20. D. Jannach and T. Schmitz. Model-based diagnosis of spreadsheet programs: a constraint-based debugging approach. Autom. Softw. Eng., 23(1):105-144, 2016.
  21. M. Jose and R. Majumdar. Cause clue clauses: error localization using maximum sat- isfiability. In PLDI, pages 437-446, 2011.
  22. S. Lamraoui and S. Naka- jima. A formula-based approach for automatic fault lo- calization of imperative programs. In ICFEM, pages 251- 266, 2014.
  23. S. Lamraoui and S. Naka- jima. A formula-based approach for automatic fault local- ization of multi-fault programs. JIP, 24(1):88-98, 2016.
  24. M. H. Liffiton and K. A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1):1-33, 2008.
  25. M. H. Liffiton, A. Previti, A. Malik, and J. Marques-Silva. Fast, flexible MUS enumeration. Constraints, 21(2):223-250, 2016.
  26. Marques-Silva et al., 2015] J. Marques-Silva, M. Janota, A. Ignatiev, and A. Morgado. Efficient model based diag- nosis with maximum satisfiability. In IJCAI, pages 1966- 1972, 2015.
  27. C. Mencía, A. Previti, and J. Marques- Silva. Literal-based MCS extraction. In IJCAI, pages 1973-1979, 2015.
  28. A. Morgado, C. Dodaro, and J. Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In CP, pages 564-573, 2014.
  29. Nica et al., 2013] I. Nica, I. Pill, T. Quaritsch, and F. Wotawa. The route to success -a performance com- parison of diagnosis algorithms. In IJCAI, 2013.
  30. Pietersma and van Gemund, 2006] J. Pietersma and A. J. C. van Gemund. Temporal versus spatial observability in model-based diagnosis. In ICSMC, pages 5325-5331, 2006.
  31. A. Previti, A. Ignatiev, A. Morgado, and J. Marques-Silva. Prime compilation of non-clausal for- mulae. In IJCAI, pages 1980-1988, 2015.
  32. A. Previti, C. Mencía, M. Järvisalo, and J. Marques-Silva. Premise set caching for enumerating minimal correction subsets. In AAAI, pages 6633-6640, 2018.
  33. R. Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987.
  34. S. Safarpour, H. Mangassarian, A. G. Veneris, M. H. Liffiton, and K. A. Sakallah. Im- proved design debugging using maximum satisfiability. In FMCAD, pages 13-19, 2007.
  35. P. Saikko, J. Berg, and M. Järvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In SAT, pages 539-546, 2016.
  36. S. Schlobach, Z. Huang, R. Cornet, and F. van Harmelen. Debugging incoherent terminolo- gies. J. Autom. Reasoning, 39(3):317-349, 2007.
  37. S. A. Siddiqi. Computing minimum- cardinality diagnoses by model relaxation. In IJCAI, pages 1087-1092, 2011.
  38. R. T. Stern, M. Kalech, A. Feldman, and G. M. Provan. Exploring the duality in conflict-directed model-based diagnosis. In AAAI, 2012.
  39. P. J. Stuckey, M. Sulzmann, and J. Wazny. Interactive type debugging in Haskell. In Haskell, pages 72-83, 2003.
  40. E. Torlak, F. S. Chang, and D. Jackson. Finding minimal unsatisfiable cores of declarative specifi- cations. In FM, pages 326-341, 2008.

Cited by

Metadata

Authors
Ignatiev, A., Morgado, A., Weissenbacher, G., & Marques-Silva, J.
Affiliations
  • Faculty of Science, University of Lisbon, Portugal
  • TU Wien, Vienna, Austria
Venue
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Publisher
International Joint Conferences on Artificial Intelligence Organization
Published
2019-08
Pages
1108-1115
DOI
10.24963/ijcai.2019/155
Cited by
15
References
0

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review

Data sources

Bibliographic data: Semantic Scholar, OpenAlex, Crossref.

Contains information from the Semantic Scholar Academic Graph Datasets, made available under the ODC Attribution License (ODC-BY 1.0).

Semantic Scholar’s data is described in: Kinney, R., et al. (2023). The Semantic Scholar Open Data Platform. arXiv:2301.10140.