Diagram And Tree Structure-based Mus Solution

Propositional satisfiability problem(SAT)is a research hotspot in the field of artificial intelligence.It is also a core problem in mathematical logic and computer research.The SAT problem is good at transforming some difficult fault solutions into probabilistic formulas in the problem system,whether there is a problem that can satisfy the assignment,and gives fault identification.Minimal unsatisfiable problems are extensions of SAT problems.When solving minimal unsatisfiable solutions,the unsatisfiable problem is usually converted into a SAT problem,and a SAT solver is used to give a judgment as to whether they are consistent and satisfiable.At present,the two ergodic structures with minimal unsatisfiable subset efficiency are Haase Diagram and enumeration tree.Haase Diagram structure is mainly used to construct the relationship between nodes by the logical structure of the graph,which is suitable for extensive constraint relationship processing.The diagram structure is mainly used in problems such as debugging relational specifications,detecting inconsistencies,and validating models.The minimal conflict problem is the application of the minimal unsatisfiable problem to model-based diagnosis.It mainly uses an enumeration tree structure and uses the characteristics of the tree to traverse the full enumeration of the component set in the circuit system.Compared with diagram structure traversal,tree structure traversal is convenient to jump nodes.With the pruning strategy,the nodes that do not need to traverse in the enumeration tree are cut to make the solution faster.In the diagram structure-based of solution,the MARCO is currently the most efficient method for solving MUS using a maximized model,but this method does not further effectively prun the solution space.Aiming at the shortcomings of the MARCO method,combined with the characteristics that the complexity of the satisfiable problem is lower than that of the unsatisfiable problem,a MARCO-MAM method based on the dual model,that is,the maximum-middle model,is proposed to solve the MUS.If the solution of middle model is a maximal satisfiable subset,the non-solution space will be reduced,and reduce the unexplored space to improve the efficiency of MUS solution;if the solution of middle model is a unsatisfiable set,the number of unsatisfiable iterative solutions of a single MUS is reduced.This method avoids the problem that the single maximization model of MARCO method does not effectively use other optimization techniques to prune the solution space when solving MUS.The experimental results show that the MARCO-MAM method is more efficient than the MARCO method,especially in large-scale problems or large search space,the efficiency is more obvious.In solving the minimal conflict set problem based on the tree structure,the MCS-SFFO method traverses a set enumeration tree(SE-Tree)in a reverse depth manner,and then prunes a combination of unrelated components of the fault output.In this paper,based on the MCS-SFFO method,combined with the fault logic relationship of the circuit,a further pruning method to solve the minimal conflict set MCS-FLR is proposed,firstly,the single component non-conflict theorem is proposed,and the single component is pruned to avoid access to non-solution space;Secondly,a non-minimal conflict theorem is proposed,and it is deduced that the superset of the fault output related components are conflict sets,so the non-minimum solutions in the solution space are pruned.Based on MCS-SFFO method,MCS-FLR method reduces the number of times the SAT solver is called in a large number of solution spaces and partial non-solution spaces,saving solution time.Experimental results show that compared with MCS-SFFO method,the MCS-FLR method has significantly improved solution efficiency.