Recently, various MBD methods have been developed, each focusing on different models. Evidence suggests that compiling MBD to MaxSAT offers significant performance improvements over earlier approaches. However, these algorithms rarely consider the problem of encoding reduction. Moreover, they remain time-consuming, particularly when applied to large-scale single observation or multi-observation problems.
To solve the problems, a research team led by Jihong Ouyang published their new research on “DVRE: Dominator-based Variables Reduction of Encoding for Model-Based Diagnosis” on 15 July 2025 in Frontiers of Computer Science co-published by Higher Education Press and Springer Nature.
In this research, they propose an efficient encoding method to solve this problem. The method makes several significant contributions. First, our strategy significantly reduces the size of the encoding required for constructing MaxSAT formulations in the offline phase, without the need for additional observations. Second, this strategy significantly decreases the number of clauses and variables through system observations, even when dealing with components that have uncertain output values. Last, our algorithm is applicable to both single and multiple observation diagnosis problems, without sacrificing the completeness of the solution set. Experimental results on ISCAS-85 benchmarks show that our algorithm outperforms the state-of-the-art algorithms on both single and multiple observation problems.
DOI
10.1007/s11704-024-40894-w