A Model-Based Diagnosis Method for Integrating Cardinality Constraints and Enqueueing at Once

Qing Yang; Ouyang Dantong; Zhou Huisi; Zhang Liming

doi:10.7544/issn1000-1239.202330546

Journal of Computer Research and Development > 2025 > 62(2): 408-417. > DOI: 10.7544/issn1000-1239.202330546 CSTR: 32373.14.issn1000-1239.202330546

Qing Yang, Ouyang Dantong, Zhou Huisi, Zhang Liming. A Model-Based Diagnosis Method for Integrating Cardinality Constraints and Enqueueing at Once[J]. Journal of Computer Research and Development, 2025, 62(2): 408-417. DOI: 10.7544/issn1000-1239.202330546

Citation:

PDF (1851 KB)

A Model-Based Diagnosis Method for Integrating Cardinality Constraints and Enqueueing at Once

College of Computer Science and Technology, Jilin University, Changchun 130012
Key Laboratory of Symbol Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012

Funds: This work was supported by the National Natural Science Foundation of China (62076108, 61872159) and the Project of Education Department of Jilin Province (JJKH20211106, JJKH20211103KJ).

More Information

Author Bio:
Qing Yang: born in 2000. Master candidate. His main research interest includes model-based diagnosis

Ouyang Dantong: born in 1968. PhD, professor, PhD supervisor. Senior member of CCF. Her main research interests include the model-based diagnosis, SAT problem, and model checking

Zhou Huisi: born in 1995. PhD. Her main research interests include MaxSAT, model-based diagnosis

Zhang Liming: born in 1980. PhD, senior engineer. Senior member of CCF. His main research interests include model-based diagnosis and SAT problem
Received Date: June 23, 2023
Revised Date: December 06, 2023
Available Online: April 27, 2024

Graphical Abstract

Abstract

Abstract

Model-based diagnosis (MBD) finds a growing number of uses in different settings. It includes software fault localization, debugging of spread sheets, Web services, and hardware designs, and 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. Since computing diagnosis is computationally challenging, some MBD algorithms by compacting the model are presented successively, such as dominated-based compacted model with multiple observations (D-CMMO) approach. In this paper, we propose one new diagnosis model, namely, cardinality-constrained compacted (CCM) model, to solve the problem in which a considerable amount of time is needed when multiple observations are given and more than one fault is injected. CCM uses two methods to optimize the process of solving MBD. Firstly, we propose to utilize relationship of faulty system-outs and faulty components to limit the scope of target solution. Secondly, the performance of the MaxSAT (maximum satisfiability) solver is effectively improved by enqueueing all assumptions at once. Furthermore, experiment evaluations on ISCAS85 and ITC99 benchmarks show that compared with D-CMMO, the latest encoding algorithms for MBD, the above two optimization methods effectively reduce the scope of MBD problem, reduce the difficulty of searching for the target solution by the MaxSAT solver, and thus return diagnostic solution in a shorter time. On average, the solving efficiency of CCM method is improved by 64.5% and 92.8% compared with D-CMMO method respectively.

FullText(HTML)

References (38)

References

[1]	Reiter R. A theory of diagnosis from first principles[J]. Artificial Intelligence, 1987, 32(1): 57−95 doi: 10.1016/0004-3702(87)90062-2
[2]	Friedrich G, Gottlob G, Nejdl W. Hypothesis classification, abductive diagnosis and therapy[C]//Proc of the Expert Systems in Engineering Principles and Applications. Berlin: Springer, 1990: 69–78
[3]	Feldman A, Pill I, Wotawa F, et al. Efficient model-based diagnosis of sequential circuits[C]//Proc of the 34th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2020: 2814–2821
[4]	Struss P, Price C. Model-based systems in the automotive industry[J]. AI Magazine, 2004, 24(4): 17−34
[5]	Ardissono L, Console L, Goy A, et al. Cooperative model-based diagnosis of web services[C]//Proc of the 16th Int Workshop on Principles of Diagnosis. Paris: CEUR-WS, 2005: 125–130
[6]	Jannach D, Schmitz T. Model-based diagnosis of spreadsheet programs: A constraint-based debugging approach[J]. Automated Software Engineering, 2016, 23(1): 105−144 doi: 10.1007/s10515-014-0141-7
[7]	Jose M, Majumdar R. Cause clue clauses: Error localization using maximum satisfiability[J]. ACM SIGPLAN Notices, 2011, 46(6): 437−446 doi: 10.1145/1993316.1993550
[8]	Feldman A, Provan G M, Van Gemund A J C. Computing minimal diagnoses by greedy stochastic search[C]//Proc of the 23rd AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2008: 911–918
[9]	Siddiqi S A, Huang Jinbo. Hierarchical diagnosis of multiple faults[C]//Proc of the 20th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2007: 581–586
[10]	Jannach D, Schmitz T, Shchekotykhin K M. Parallelized hitting set computation for model-based diagnosis[C]//Proc of the 29th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2015: 1503–1510
[11]	Ansótegui C, Bonet M L, Levy J. SAT-based MaxSAT algorithms[J]. Artificial Intelligence, 2013, 196(1): 77−105
[12]	Feldman A, Provan G, de Kleer J. Solving model-based diagnosis problems with Max-SAT solvers and vice versa[C]//Proc of the 21st Int Workshop on Principles of Diagnosis. New York: PHM Society, 2010: 185–192
[13]	Stern R T, Kalech M, Feldman A. Exploring the duality in conflict-directed model-based diagnosis[C]//Proc of the 26th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2012: 828–834
[14]	Ignatiev A, Morgado A, Weissenbacher G, et al. Model-based diagnosis with multiple observations[C]//Proc of the 28th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2019: 1108–1115
[15]	Lamraoui S, Nakajima S. A formula-based approach for automatic fault localization of imperative programs[C]//Proc of the 16th Int Conf on Formal Engineering Methods. Berlin: Springer, 2014: 251–266
[16]	Lamraoui S, Nakajima S. A formula-based approach for automatic fault localization of multi-fault programs[J]. Journal of Information Processing, 2016, 24(1): 88−98 doi: 10.2197/ipsjjip.24.88
[17]	Narodytska N, Bacchus F. Maximum satisfiability using core-guided MaxSAT resolution[C]//Proc of the 28th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2014: 2717–2723
[18]	Cai Shaowei, Lei Zhendong. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability[J]. Artificial Intelligence, 2020, 287: 103354−103354 doi: 10.1016/j.artint.2020.103354
[19]	Marques-Silva J, Heras F, Janota M, et al. On computing minimal correction subsets[C]//Proc of the 23rd Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2013: 615–622
[20]	Previti A, Mencía C, Järvisalo M, et al. Premise set caching for enumerating minimal correction subsets[C]//Proc of the 32nd AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2018: 6633–6640
[21]	Zhou Huisi, Ouyang Dantong, Zhang Liming, et al. Model-based diagnosis with improved implicit hitting set dualization. Forthcoming[J]. Applied Intelligence, 2022, 52(2): 2111−2118 doi: 10.1007/s10489-021-02408-0
[22]	Kalech M, Stern R, Lazebnik E. Minimal cardinality diagnosis in problems with multiple observations[J]. Diagnostics, 2021, 11(5): 780−780 doi: 10.3390/diagnostics11050780
[23]	Gu Jun, Purdom P W, Franco J, et al. Algorithms for the Satisfiability Problem[M]//Handbook of Combinatorial Optimization. Berlin: Springer, 1999: 379–572
[24]	Zhou Huisi, Ouyang Dantong, Zhao Xiangfu, et al. Two compacted models for efficient model-based diagnosis[C]//Proc of the 34th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2022: 3885−3893
[25]	Metodi A, Stern R, Kalech M, et al. A novel SAT-based approach to model based diagnosis[J]. Journal of Artificial Intelligence, 2014, 51(1): 377−411
[26]	Marques-Silva J , Mikoláš J, Ignatiev A , et al. Efficient model based diagnosis with maximum satisfiability[C]//Proc of the 24th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2015: 1966−1972
[27]	Amit M, Roni S, Meir K, et al. Compiling model-based diagnosis to Boolean satisfaction[C]//Proc of the 26th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2012: 793−799
[28]	Thomas L, Robert E T. A fast algorithm for finding dominators in a flowgraph[J]. ACM Transactions Programming Languages and Systems, 1979, 1(1): 121−141 doi: 10.1145/357062.357071
[29]	刘梦,欧阳丹彤,刘伯文,等. 结合问题特征的分组式诊断方法[J] 电子学报,2018,46(3):589−594 Liu Meng, Ouyang Dantong, Liu Bowen, et al. Grouped diagnosis approach using the feature of problem[J]. Acta Electronica Sinica, 2018, 46(3): 589−594 (in Chinese)
[30]	欧阳丹彤,刘伯文,刘梦,等. 结合电路结构基于分块的诊断方法[J] 电子学报,2018,46(7):1571−1577 Ouyang Dantong, Liu Bowen, Liu Meng, et al. A block-based diagnostic method combing with the circuit structure[J]. Acta Electronica Sinica, 2018, 46(7): 1571−1577 (in Chinese)
[31]	周慧思,欧阳丹彤,田鑫亮,等. 基于模型诊断的一种新编码方法[J] 计算机研究与发展,2023,60(1):95−102 Zhou Huisi, Ouyang Dantong, Tian Xinliang, et al. A novel encoding for model based diagnosis[J]. Journal of Computer Research and Development, 2023, 60(1): 95−102 (in Chinese)
[32]	Siddiqi S A, Huang Jinbo. Sequential diagnosis by abstraction[J]. Journal of Artificial Intelligence Research, 2011, 41: 329−365 doi: 10.1613/jair.3296
[33]	Eèn N, Sörensson N. Temporal induction by incremental SAT solving[J]. Electronic Notes in Theoretical Computer Science, 2003, 89(4): 543−560 doi: 10.1016/S1571-0661(05)82542-3
[34]	Eèn N, Sörensson N. An extensible SAT-solver[C]//Proc of the 6th Theory and Applications of Satisfiability Testing. Berlin: Springer, 2004: 502−518
[35]	Audemard G, Lagniez J M, Simon L. Improving Glucose for incremental SAT solving with assumptions: Application to MUS extraction[C]//Proc of the 16th Theory and Applications of Satisfiability Testing. Berlin: Springer, 2013: 309–317
[36]	Ogawa T, Liu Yangyang, Hasegawa R, et al. Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers[C]//Proc of the 25th IEEE Int Conf on Tools with Artificial Intelligence. Piscataway, NJ: IEEE, 2013: 9−17
[37]	Brglzz F, Fujtwara H. A neutral netlist of 10 combinational benchmark circuits and a target translator in FORTRAN[J/OL]. IEEE International Symposium on Circuits and Systems. 1985[2023-03-20].https://www.researchgate.net/publication/239562831_A_neutral_netlist_of_10_combinational_circuits_and_a_target_translator_in_fortran
[38]	Siddiqi S A. Computing minimum-cardinality diagnoses by model relaxation[C]//Proc of the 22nd Int Joint Conf on Artificial Intelligence. Palo Alto, CA : AAAI, 2011: 1087–1092

[1]	Xie Wenbing, Guan Ruixue, Zhang Yiming, Li Jiamei, Wang Jun. Efficient Optimization of Erasure Coding for Storage Library[J]. Journal of Computer Research and Development. DOI: 10.7544/issn1000-1239.202440091
[2]	Yan Zhiyuan, Xie Biwei, Bao Yungang. HVMS: A Hybrid Vectorization-Optimized Mechanism of SpMV[J]. Journal of Computer Research and Development, 2024, 61(12): 2969-2984. DOI: 10.7544/issn1000-1239.202330204
[3]	Wang Chuang, Ding Yan, Huang Chenlin, Song Liantao. Bitsliced Optimization of SM4 Algorithm with the SIMD Instruction Set[J]. Journal of Computer Research and Development, 2024, 61(8): 2097-2109. DOI: 10.7544/issn1000-1239.202220531
[4]	Shen Jie, Long Biao, Jiang Hao, Huang Chun. Implementation and Optimization of Vector Trigonometric Functions on Phytium Processors[J]. Journal of Computer Research and Development, 2020, 57(12): 2610-2620. DOI: 10.7544/issn1000-1239.2020.20190721
[5]	Yan Hongfei, Zhang Xudong, Shan Dongdong, Mao Xianling, Zhao Xin. SIMD-Based Inverted Index Compression Algorithms[J]. Journal of Computer Research and Development, 2015, 52(5): 995-1004. DOI: 10.7544/issn1000-1239.2015.20131548
[6]	Zhao Long, Han Wenbao, and Yang Hongzhi. Research on ECC Attacking Algorithm Based on SIMD Instructions[J]. Journal of Computer Research and Development, 2012, 49(7): 1553-1559.
[7]	He Yi, Ren Ju, Wen Mei, Yang Qianming, Wu Nan, Zhang Chunyuan, and Guo Min. Research on FPGA-Based Paging-Simulation Model for SIMD Architecture[J]. Journal of Computer Research and Development, 2011, 48(1): 9-18.
[8]	Huang Shuangqu, Xiang Bo, Bao Dan, Chen Yun, and Zeng Xiaoyang. VLSI Implementation of Multi-Standard LDPC Decoder Based on SIMD Architecture[J]. Journal of Computer Research and Development, 2010, 47(7): 1313-1320.
[9]	Li Zhaopeng, Chen Yiyun, Ge Lin, and Hua Baojian. A Formal Certifying Framework for Assembly Programs[J]. Journal of Computer Research and Development, 2008, 45(5): 825-833.
[10]	Lin Jiao, Chen Wenguang, Li Qiang, Zheng Weimin, Zhang Yimin. A New Data Clustering Algorithm for Parallel Whole-Genome Shotgun Sequence Assembly[J]. Journal of Computer Research and Development, 2006, 43(8): 1323-1329.