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

Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spread sheets, 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. 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 Model (CCM), 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 returned diagnostic solution in a shorter time. On average, the solving efficiency of CCM method is improved by 64.5% and 92.8% compared to D-CMMO method respectively.