Study On Several Methods Based On Boolean Satisfiability

Boolean satisfiability problem(SAT)is a classic problem in automated reasoning in the field of Artificial Intelligence.Tracing back to 1971,Cook proved that SAT is a nondeterministic polynomial(NP)complete problem from the perspective of a Turing machine.As the first proved NP-complete problem,SAT is of important theoretical and practical significance.With the continuous development of SAT,the research results have been widely applied to the studies of computer science,mathematical logic and integrated circuits.Besides,SAT has gradually presented the core technology for solving many problems in these domains nowadays.Since SAT is always expressed in Boolean logic,a variety of problems can be transformed into SAT problem and be effectively solved.The minimal correction subset(MCS)solving is an important extension of SAT problem and plays a crucial role in hot issues ranging from model-based diagnosis(MBD)to single-objective optimization and multi-objective combinatorial optimization(MOCO).When there exists an infeasible system,i.e.,the set of constraints which cannot be satisfied simultaneously,it is necessary to explore the unsatisfiable reasons and make the system feasible.Computing the MCS is a cornerstone task in infeasibility analysis since its removal corrects the infeasibility.This paper studies the related methods for SAT-based MCS algorithms.Directed towards the shortcomings and technical challenges of combining MCS with MBD and MOCO problems,this paper proposes several solutions and optimizations,with the purpose of improving the efficiency of current MBD methods and the performance of MOCO methods.The main contents are as follows:1)A new method for minimality-checking of diagnosis based on subset consistency detection is proposed,referred to as SCD method.The SAT-based MBD method combined with the set enumeration tree is one of the mainstream direct diagnosis methods currently.This kind of methods checks the consistency of the candidate solutions to determine whether it is a diagnosis with SAT solver.However,since the minimality of the diagnosis cannot be guaranteed,a minimality-checking process is necessary.The disadvantage of the traditional minimality-checking process is that as the number of diagnoses increases,the difficulty of detection increases gradually,thus the timeconsuming increases.Therefore,this paper proposes a new method for minimalitychecking of diagnosis based on subset consistency detection.When the MBD problem is compiled to SAT,the minimal subset diagnosis is equivalent to MCS.This method first combines the interoperability between the minimal subset diagnosis and MCS,then studies the relationship among the minimality of the diagnosis and its subsets.A theorem for minimality-checking of diagnosis based on subset consistency detection is presented.Moreover,this method checks the consistency of a few subsets of the diagnosis to determine the minimality.The experimental results illustrate that the method effectively avoids the effect of the increasing amount of diagnosis and further improves the overall efficiency of diagnosis methods.2)A core-guided path diversification method for minimal correction subset enumeration is proposed,referred to as Cg PDMCS algorithm.In recent years,researchers have proved that enumerating MCSs can be effectively applied to solving MOCO problem.In other to obtain a better solution set,current MCS-based MOCO methods mainly integrate some mechanisms in the process of MCS enumeration.One of the mechanisms which improve the performance of MCS-based MOCO methods is the addition of path diversification.However,although the path diversification method provides a better solution set for MOCO,there still exists redundant search space that has not been reduced effectively.Therefore,in view of the shortcomings,this paper proposes a novel core-guided path diversification method.This method first takes strength of the information provided by unsatisfiable cores and proposes the definition and theorem of the infeasible path.Then the redundant search space of the MOCO problem is pruned by exploiting unsatisfiable cores.Moreover,in order to enrich the diversity of the solution set for MOCO,the method generates diversification paths built by a core-guided variable selection.Preventing the waste on infeasible paths,the method takes more time to serve for the valid paths and expands the path diversification,thus a better solution set can be generated within a limited time.Experimental results demonstrate that the novel approach provides a considerable performance improvement on the previous methods and produces solutions with better convergence and diversity for MOCO,especially for the instances tightly constrained.3)A dynamic score based method for stratification is proposed,referred to as DSSCLD algorithm.For MOCO instances with constraints which are easy to be satisfied,most MCS-based MOCO methods usually do not perform as well as evolutionary algorithms,further improvement is necessary.As the stratified MCS strategy has resulted in a good performance on single-objective optimization problems,the stratification of MCS for MOCO also leads the algorithm to obtain better performance under loose constraints,producing a solution set with better approximation quality and diversity.However,this stratification method lacks the balance among multiple objectives.Therefore,this paper proposes a dynamic score based method for stratification to solve the MOCO problem.First,the definition of dynamic score is presented and two scoring rules are formulated for the partitions of objective functions.RULE-1 guides the method to update the dynamic scores when generating a combined partition sequence by the selection among objectives.After obtaining an MCS,RULE-2 assigns the initial dynamic scores for a new sequence in the next iteration according to the optimization ratio of objectives.Then,the Softmax function is used for mapping dynamic scores to probabilities for partitions in order to dynamically adapt the selection among objective functions.Experimental results show that the dynamic score based method guides the stratified MCS-based MOCO method to reach solutions with better convergence and diversity for MOCO,thus provides an effective improvement on the current state-of-theart MCS-based MOCO method.