DVRE: dominator-based variables reduction of encoding for model-based diagnosis

Compiling Model-Based Diagnosis to maximum satisfiability (MaxSAT) is currently a popular method because it can directly calculate the diagnosis. Although the method based on dominator component encoding can reduce the difficulty of the problem, with the increase of the system size, the complexity of the solution is also increasing. In this paper, we 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.