Research On Diagnostic Problems With PMS Algorithm Combined With Structure Characteristics

Model-Based Diagnosis(MBD)is an important research direction in artificial intelligence field.At first,model-based diagnosis is mainly used in the static diagnosis for electric circuit.In recent years,dynamic diagnosis is gradually applied in the field of large scale software validation,aircraft safety validation and network communication validation.Hence,diagnosis problem has become the focus of both theoretical research and technique application.At current stage,Max SAT(Maximum Satisfiability)solver is one of the mainstream methods to solve model-based diagnosis problem.Max SAT problem is the optimization design of SAT problem.Currently,Max SAT solver is composed of complete solver and incomplete solver,where complete solver and calculate a optimal solution in effective time and incomplete solver get an approximate optimal solution in certain time.Weighted Max SAT and(unweighted)PMS(Partial Maximum Satisfiability)problem are two significant generalizations of Max SAT,in which PMS makes model-based diagnosis problem more convenient by being classified as hard clauses and soft clauses,is well applied in network router scheduling problem,fault detection problem,time table scheduling,combinatorial auction and PGA routing problem.Currently,diagnosis problem is encoded as PMS problem and become Max SAT contest instance.Based on the backgroud above,the main research work of this thesis is listed below:We propose SCPMS algorithm to solve PMS problem combing structure feature in this paper.In SCPMS algorithm,we propose the concept of hard-blocked variable,soft-blocked variable and structure-feature-apparent clauses set.Dividing structure-feature-apparent into two parts,we can obtain hard-blocked variables and soft-blocked variables matching current solution using unit propagation.When using unit propagation to a part of structure-feature-apparent clauses set,soft-blocked variable value will be directly obtained if there are there is variable conflict in two clauses subsets.Hence,the solution space is significantly reduced.If there is no conflicts,we will continue to perform local search in search space,and this algorithm is still efficient for some structure-feature-inapparent clause set.The experiments on standard industrial diagnosis cases show that SCPMS improves the solving efficiency to a great extent compared to Dist UP and Deci Dist.Besides,we observe that Deci Dist and SATLike algorithm have the low sovling efficency drawback caused by the propagation disorder in hard unit clause and soft unit clause.Based on deep research that hard unit clause represents the structure feature of diagnosis system,we propose a CWPMS algorithm based on conflict-delay propagation local search algorithm.This algorithm perform soft unit clauses and conflict delay propagation mechanism.The mechanism propagates hard clause with high priority and perform delay propagation mechanism.The experiment result shows that compared with SATLike,the unsatisfiable soft clauses obtained by CWPMS is reduced to a great extent within 300 seconds.The above methods make certain improvement on Max SAT solvers from different aspects,and the solving efficiency is improved to a certain extent.