logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 11: 112101(2018) https://doi.org/10.1007/s11432-017-9273-5

Efficient zonal diagnosis with maximum satisfiability

More info
  • ReceivedJul 11, 2017
  • AcceptedSep 27, 2017
  • PublishedMay 18, 2018

Abstract

Model-based diagnosis (MBD) has been widely acknowledged as an effective diagnosis paradigm. However, for large scale circuits, it is difficult to find all cardinality-minimal diagnoses within a reasonable time. This paper proposes a novel method that takes a significant step in this direction. The idea is to divide a circuit into zones and compute the cardinality-minimal diagnoses by finding subset-minimal diagnoses with cardinality-minimal via a maximum satisfiability (MaxSAT) solver on an abstracted circuit that is composed of these zones instead of all components. We also propose a new propagate-extend method for extending the seed-TLDs to obtain all cardinality-minimal diagnoses efficiently. We implement our method with a state-of-the-art core-guided MaxSAT solver, and present evidence that it significantly improves the diagnosis efficiency on ISCAS-85 circuits. Our method outperforms SATbD, which was recently shown to outperform most complete MBD approaches using satisfiability (SAT).


References

[1] Console L, Dressler O. Model-based diagnosis in the real world: lessons learned and challenges remaining. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence, Stockholm, 1999. 1393--1400. Google Scholar

[2] Xu K, Li W. Many hard examples in exact phase transitions. Theory Comput Sci, 2006, 355: 291-302 CrossRef Google Scholar

[3] Wang Y Y, Ouyang D T, Zhang L M. A novel local search for unicost set covering problem using hyperedge configuration checking and weight diversity. Sci China Inf Sci, 2017, 60: 062103 CrossRef Google Scholar

[4] Gao J, Wang J N, Yin M H. Experimental analyses on phase transitions in compiling satisfiability problems. Sci China Inf Sci, 2015, 58: 032104 CrossRef Google Scholar

[5] Geng X N, Ouyang D T, Zhang Y G. Model-based diagnosis of incomplete discrete-event system with rough set theory. Sci China Inf Sci, 2017, 60: 012205 CrossRef Google Scholar

[6] Wang X Y, Jiang S J, Gao P F. Cost-effective testing based fault localization with distance based test-suite reduction. Sci China Inf Sci, 2017, 60: 092112 CrossRef Google Scholar

[7] Zhou J P, Yin M H, Li X T. Phase transitions of expspace-complete problems: a further step. Int J Found Comput Sci, 2012, 23: 173-184 CrossRef Google Scholar

[8] de Kleer J, Mackworth A K, Reiter R. Characterizing diagnoses and systems. Artif Intel, 1992, 56: 197-222 CrossRef Google Scholar

[9] De K J. US Patent, 9563525, 2017-02-07. Google Scholar

[10] Jannach D, Schmitz T, Shchekotykhin K. Parallelized hitting set computation for model-based diagnosis. In: Proceedings of the 29th AAAI Conference on Artificial Intelligence, Austin, 2015. 1503--1510. Google Scholar

[11] Williams B C, Ragno R J. Conflict-directed A* and its role in model-based embedded systems. Discrete Appl Math, 2007, 155: 1562-1595 CrossRef Google Scholar

[12] Feldman A, Provan G, de Kleer J, et al. Solving model-based diagnosis problems with max-sat solvers and vice versa. In: Proceedings of the 21th International Workshop on Principles of Diagnosis, Portland, 2010. 185--192. Google Scholar

[13] Metodi A, Stern R, Kalech M, et al. Compiling model-based diagnosis to boolean satisfaction. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. 793--799. Google Scholar

[14] Metodi A, Stern R, Kalech M. A Novel SAT-Based Approach to Model Based Diagnosis. jair, 2014, 51: 377-411 CrossRef Google Scholar

[15] Zhang J, Ma F F, Zhang Z Q. Faulty interaction identification via constraint solving and optimization. In: Proceedings of the 15th Theory and Applications of Satisfiability Testing, Trento, 2012. 186--199. Google Scholar

[16] Darwiche A. Decomposable negation normal form. J ACM, 2001, 48: 608-647 CrossRef Google Scholar

[17] Siddiqi S, Huang J B. Hierarchical diagnosis of multiple faults. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, 2007. 581--586. Google Scholar

[18] Stern R, Kalech M, Feldman A, et al. Exploring the duality in conflict-directed model-based diagnosis. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. 828--834. Google Scholar

[19] Smith A, Veneris A, Ali M F. Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans Comput-Aided Design, 2005, 24: 1606-1621 CrossRef Google Scholar

[20] Mangassarian H, Veneris A, Safarpour S, et al. A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In: Proceedings of the 26th International Conference on Computer-Aided Design, San Jose, 2007. 240--245. Google Scholar

[21] Suelflow A, Fey G, Bloem R, et al. Using unsatisfiable cores to debug multiple design errors. In: Proceedings of the 18th ACM Great Lakes Symposium on VLSI, Orlando, 2008. 77--82. Google Scholar

[22] Safarpour S, Veneris A. Abstraction and refinement techniques in automated design debugging. In: Proceedings of the 10th Design, Automation and Test in Europe Conference and Exhibition, Nice, 2007. 1182--1187. Google Scholar

[23] Gao J, Li R Z, Yin M H. A randomized diversification strategy for solving satisfiability problem with long clauses. Sci China Inf Sci, 2017, 60: 092109 CrossRef Google Scholar

[24] Liu J, Xu K. A novel weighting scheme for random k-SAT. Sci China Inf Sci, 2016, 59: 092101 CrossRef Google Scholar

[25] Safarpour S, Mangassarian H, Veneris A, et al. Improved design debugging using maximum satisfiability. In: Proceedings of the 7th Formal Methods in Computer Aided Design, Austin, 2007. 13--19. Google Scholar

[26] Kutsuna T, Sato S, Chujo N. Diagnosing automotive control systems using abstract model-based diagnosis. In: Proceedings of the 20th International Workshop on Principles of Diagnosis, Stockholm, 2009. 99--105. Google Scholar

[27] Chen Y B, Safarpour S, Veneris A, et al. Spatial and temporal design debug using partial MaxSAT. In: Proceedings of the 19th ACM Great Lakes Symposium on VLSI, Boston Area, 2009. 345--350. Google Scholar

[28] Cai S W, Luo C, Thornton J, et al. Tailoring local search for partial MaxSAT. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence, Quebec, 2014. 2623--2629. Google Scholar

[29] Marques-Silva J, Janota M, Ignatiev A, et al. Efficient model based diagnosis with maximum satisfiability. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence, Buenos Aires, 2015. 1966--1972. Google Scholar

[30] Kirkland T, Mercer M. A topological search algorithm for ATPG. In: Proceedings of the 24th ACM/IEEE Design Automation Conference, Miami Beach, 1987. 502--508. Google Scholar

[31] Huang J B, Darwiche A. On compiling system models for faster and more scalable diagnosis. In: Proceedings of the 20th National Conference on Artificial Intelligence, London, 2005. 300--306. Google Scholar

[32] Reiter R. A theory of diagnosis from first principles. Artif Intel, 1987, 32: 57-95 CrossRef Google Scholar

[33] de Kleer J, Williams B C. Diagnosing multiple faults. Artif Intel, 1987, 32: 97-130 CrossRef Google Scholar

[34] Siddiqi S. Computing minimum-cardinality diagnoses by model relaxation. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, Barcelona, 2011. 1087--1092. Google Scholar

[35] Martins R, Joshi S, Manquinho V, et al. Incremental cardinality constraints for MaxSAT. In: Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, Lyon, 2014. 531--548. Google Scholar

[36] Nica I, Pill I, Quaritsch T, et al. The route to success-a performance comparison of diagnosis algorithms. In: Proceedings of the 22th International Joint Conference on Artificial Intelligence, Beijing, 2013. 1039--1045. Google Scholar

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1