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 d...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.展开更多
基金supported by the National Natural Science Foundation of China(Grant Nos.62076108 and 62006094)the Scientific and Technological Developing Scheme of Jilin Province,China(Grant No.20190701031GH)the Key Project of the Education Department of Jilin Province,China(Grant No.JJKH20231175KJ).
文摘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.
