Study On Parallel SAT Solver And Parallel Automated Deduction Reasoning Systems

Propositional logic and first-order logic are basic problems in logic,and also the core problems in computer science.Proposition is the smallest unit of logical formula in reasoning system.First-order logic can be regarded as the extension of propositional logic by complementing mainly the predicate and quantifier,and is the classical predicate logic.SAT is short for ‘Satisfiability Problem'.SAT solving and first order logical automatic theorem proving are widely used in various fields of natural science and social science,such as mathematical theorems proving,reliability verification of the communication protocol,the reliability verification of the integrated circuit,the automatic program generation and test cases automatic generation,formal verification,intelligent planning,knowledge compiling,password security reliability analysis,and even the unambiguity analysis validation of laws and regulations.These problems can be converted to the SAT solving,and also can be converted into first-order logic theorem proving.Therefore,it is of great theoretical significance and practical application value to study SAT problem solving and first-order logic theorem proving theories and methods.Parallel mechanisms are effective means to improve the efficiency of propositional logic solver and first order logic prover.In this dissertation,parallel propositional logic solving and parallel first order logic theorem proving is studied.For the aspect of propositional logic solving,this dissertation studies the relevant technology of parallel propositional logic solving,and then applies the relevant technology of parallel propositional logic solution to design and implement the parallel inverse deduction system based on contradiction separation based dynamic automated deduction theory proposed by Professor Xu Yang.This dissertation proposed a parallel hybrid genetic algorithm framework based on OpenMP,which combines genetic algorithm and local search algorithm organically to solve 3-SAT problems,and is able to make full use of the ability of local search algorithm to find local optimal solution and the ability of global search of genetic algorithm.At the same time,the limited local searches iteration and catastrophe operation can prevent the system from falling into the local optimization,and the improvement of the selection operation algorithm improves the efficiency of genetic algorithm.Under the OpenMP parallel programming framework,the hybrid genetic algorithm is parallelized by compiling guidance statements,which makes full use of computing resources.The testing results based on the test cases in SATLib,the international SAT problem benchmark library,shows that the proposed parallel hybrid genetic algorithm improves the efficiency and success rate of solving 3-sat problems compared with similar algorithms.Hardware acceleration parallel mechanism is applied for the SAT problem solving,the SAT solving algorithm is designed and improved accordingly based on GPU,which is able to improve the calculation process of GPU kernel function.The corresponding data structure is then designed to complete the BCP process on GPU via bit operation.At the same time,bit operation can reduce the number of branches in the kernel function and improve the efficiency of GPU.The experimental results show that the improved GPU-based BCP algorithm achieves a higher solving efficiency.The clause evaluation plays an important role in SAT solving and first-order theorem proving,while the existing clause evaluation algorithms consider only a single clause feature and the quality of the reserved learning clause is low.In order to improve the clause evaluation performance,this dissertation proposes a new method to evaluate the learnt clauses,i.e.,a clause evaluation strategy based on frequency and LBD mixing.In the parallel solver,the original clause evaluation method in the periodic learnt clause deletion module is replaced with the proposed evaluation method,and the hybrid evaluation algorithm is applied to the clause sharing module of the parallel algorithm to form a new clause sharing strategy.Experimental results show that the solver with hybrid evaluation algorithm has higher solving ability than the original one.The versions by combining the proposed method with Syrup and abcd-sat-p have solved 43 problems that the original versions can not solve.This dissertation studied the contradiction separation based dynamic automated deduction theory and proposed the deductive path control algorithm based on backtracking.A parallel inverse deduction system of contradiction separation based dynamic automated deduction is designed and implemented,which realizes the parallel partitioning of first-order logic problems of automating deduction based theorem proving.Experimental results on benchmark problems show the superiority of the contradiction separation based dynamic automatic deduction theory and the parallel theorem proving system based on this theory.