Research And Implementation Of An All-Solution SAT Solver

As the first proved NP-complete problem,satisfiability problem(SAT) has crucial significance both in theoretical research and practical application.It is the core problem in the computer theory and application,and has significant value in the area of computer science,artificial intelligence and other disciplines.All-solution satisfiability problem has an important application value in the field of electronic design automation(EDA).This paper described the significance of All-solution Boolean satisfiability problem both in theoretical and practical aspect.It compared several algorithms of SAT solvers and selected the algorithm with higher efficiency and better suitability for all-solution SAT solver.Two new algorithms,in terms of increment and blocking clause,were proposed which could be applied to all-solution SAT solver.(1) Adjust weight of literals for incremental solving,and conflict analysis and backtracking of blocking clauses.This algorithm integrates the variable state independent decaying sum(VSIDS) decision heuristic algorithms,adjust the weight of literals in the blocking clauses added while the all-solution SAT solver program is running and thus increase the efficiency of working out all solutions.A special analysis and backtracking mechanism was proposed,which can process the conflict caused by blocking clauses and make the program go to the next solving process quickly when a new blocking clause was added.(2) Improve the all-solution SAT solver on blocking clause.Supply the like-Don't cares algorithm based on CNF.This algorithm draws lessons from Don't cares algorithm based on hybrid representations(which combines the characteristics of circuit with CNF).To some extent,it improves the efficiency of all-solution SAT solver which is based on CNF input.Merging the blocking clause.This strategy can merge current blocking clauses without consuming too much time and space resources.The effect for improving the efficiency of SAT solver of these two algorithms can be seen from the results.