| The Boolean Satisfiability Problem is the first NP Complete Problem and is one of the most important cores in the field of computer science.It is widely used in many fields,such as electronic design automation,model testing,software verification,integrated circuit verification,combinatorial optimization and computational biology.In this thesis,we would focus on the classical Boolean satisfiability problem and its extended problems.Our work includes the formal description of classical SAT reasoning methods and the reasearch.The research on related issues which is referd to clause learning algorithms.In addition,we also study the extended rule method,which is the inverse operation of the resolution method,and # SAT,which is the extended form of the reasoning problem.The main contributions of this thesis as follows.(1)In order to formally describe the entire reasoning process of the DPLL algorithm ith clause learning by the cell membrane calculus,we use a formal method of ell membrane calculus to describe the DPLL algorithm with clause learning.Some reaction rules are defined,such as partial assignment,variable flip,backtracking,maximum backjumping level and membrane dissolution.The general process of DPLL and the process of conflict analysis are described.Finally, the feasibility of the formal method is verified by solving benchmarks with different complexity.Depending on the membrane calculus,the reasoning process of the DPLL algorithm can be displayed more intuitively and concisely,the descriptive abilities and processing abilities of the membrane calculus can be displayed at the same time.(2)Clause Learning Technology has been widely used in satisfiability problems.In this article,we propose a new optimization method for learnt clauses based on the original MiniSAT solver.Our method optimizes the learnt clauses database. Specifically,it uses the game theory to adjust the growth parameters after several restarts according to the real-time feedback of the current solver.The goal of our method is to make the capacity of the learnt clause database reach the equilibrium and Pareto optimality as much as possible.Experiments show that the proposed method is effective and outperforms optimization methods in random SAT problems.This method neither affects the speed of unit propagation because of too many clauses in the learnt clause database,nor destroys the integrity of learning because of too few clauses in the learnt clause database.(3)ERACC algorithm is the most efficient and powerful algorithm in the current extension rule solver.Based on ERACC,we design a parallel framework called PERACC.Our method is based on the configuration checking of local search method.There are three stages in our method: initializing variables,simplifying the solution space and heuristics.Specifically,after decomposing the original maximum term space into several maximum term subspaces and simplifying the original clause set,all subspaces are processed in parallel.Experiments show that, compared with the original algorithm,the new algorithm not only has a significant improvement in solving efficiency,but also can solve larger test cases,which makes the extension rule method break through the limitation of formula size again.(4)When processing benchmarks with few models,iterative SWcc method and incremental SWcc optimized method are more applicable than other existing complete model counting methods.In this article,we propose a new parallel model counting algorithm based on configuration checking in this thesis.The algorithm focuses on simplifying the solution space and heuristics.After decomposing the original maximum term space into several maximum term subspaces and simplifying the original clause set,these subspaces are processed in parallel.The experimental results show that our algorithm is more applicable than the original algorithm when solving benchmarks with fewer models and large-scale formulas.In conclusion,this thesis studies the following aspects: formal description of the DPLL algorithm with clause learning using membrane calculus,the optimization method of learnt clauses,local search-based parallel extension rule reasoning method and configuration checking-based parallel model counting method.The proposed method can intuitively describe the process of reasoning and improve the efficiency of reasoning algorithms.It also enhances the applicability of reasoning methods.Therefore,the work in this thesis can provide a reference for solving the classical and extended SAT problems. |
