Research On Key Techniques For Solving Boolean Satisfiability Problems

Boolean satisfiability(SAT)problem is one of the most widely studied NP-complete(NPC)problems.SAT problem not only occupies an important position in the research of mathematical logic and computation theory,but also is increasingly used in computer science,artificial intelligence and practical applications.Thus it attracts the attention of many researchers at home and abroad.Encoding,preprocessing and solving algorithms are three key technologies for solving SAT problems.In recent years,a lot of results have emerged.Except for P=NP,which is not polynomial time complexity in the worst case,the design of efficient and feasible SAT solving solution is still a hot research topic.This thesis is systematically studied focusing on the preprocessing and solving algorithms,proposes a series of improvement strategies and new methods according to the characteristics of different types of problems based on the existing methods,and verifies the validity by theoretical analysis and experiment.Finally this thesis studies the method of the reduction to the SAT problem,which is based on the NP class problem of the annotation propagation in the view update of relational database.The main work of this thesis includes:(1)In order to improve the simplification ability and solving success rate,reduce the time consumption of solving process,based on the widely used preprocessing method SATELITE,this thesis puts forward a variable elimination resolution simplification method(RCS-VER)based on the state constraint of the redundancy attribute of resolution clause,presents a binary clause probing simplification method(CBCP)based on conflict detection and learning,and proposes variables choosing heuristic strategies(HVC-VER and HVC-PRB)corresponding to the variable features of the rules of variable elimination resolution and probing.Experiments verify the feasibility and effectiveness of the above methods and strategies on application and combination SAT problem instances,the preprocess and solving performance is better than that of the previous SATELITE.(2)In order to give full play to the role of restart strategy for the deterministic CDCL solver,this thesis selects the representative restart strategies and carries out comparative experiments firstly,and then proposes serveral improvement strategies from two new points of "when restart,and "where restart".The first one is according to the parameters of the average conflict decision level,the conflicts numbers of decision level,the decision-making numbers between conflicts,the variable assignment numbers between conflicts etc.,evaluating the local solving state of search branches,and puting forward the dynamic heuristic "when restart" strategy correspondingly.The second one is puting forward the dynamic heuristic "where restart" strategy based on the subsequent decisions number,the subsequent assignment variables number,the variable restart numbers etc.Finally this thesis achieves the 2WSAT(When&Where SAT)algorithm based on the popular MiniSAT solver.The experiments verifies the feasibility and effectiveness of 2WSAT on application and combination SAT problem instances,shows that the solving performance is better than that of the standard MiniSAT.(3)In order to further study and expand the solving algorithms on random SAT instances,the SAT problem is transformed into a combinatorial optimization problem with the minimum value of the corresponding objective function,the discrete design of standard artificial bee colony(ABC)algorithm is carried out.This thesis first applies the ABC algorithm to SAT solving,and then improves the initial solution,fitness function,neighborhood selection,new generation,onlooker bee selection strategy,introduces the tabu search idea,and proposes a new SAT algorithm(ABCSAT).The experiments verifies the feasibility and effectiveness of ABCS AT on random instances.ABC SAT is proved to have obvious advantages in solving the success rate,solving time and memory consumption.(4)In order to further expand the application field of SAT problem,this thesis converts some NP class problems to SAT problems,such as view side effect,source side effects,annotations placement problems of the three basic problems of view update annotations propagation in relational database,and studies the reduction and encoding method of SAT problem.