A Complete Genetic Algorithm Based SAT Solver By Combining CDCL Algorithm

Boolean satisfiability problem(SAT)is the problem of determining a satisfying assignment for a given Boolean constraint formula represented in conjunctive normal form(CNF).A solution is a Boolean assignment that results in a true evaluation of the formula.A SAT solver attempts to find a solution for a formula if exists.SAT problem has a wide-spread application domain,including computer aided design,artificial intelligence,planning,etc.Various Electronic Design Automation(EDA)applications such as equivalence checking,model checking,test pattern generation,placement and route,can be formulated as SAT problems.Much research has been dedicated on developing highly scalable and efficient SAT solvers.Although a number of practical instances can be solved within reasonable computational resources by the state-of-the-art SAT solvers,due to the NP-Complete nature of SAT[1],many instances still remain extremely difficult.In this thesis,a hybrid SAT solver based on Genetic algorithm(GA)and conflict driven clause learning(CDCL)is proposed.This solver is a complete one which can performs relatively fare well on all three categories of SAT instances(Applications,Random and Crafted).The main hybrid method of this solver is to use a Genetic algorithm method combined with local search techniques as a lead solver that integrates CDCL algorithm concluding Boolean constraint propagation,conflict analysis,clause learning,and consideration of the dependencies between variables and falsified clauses during GA part.This hybrid method is to let the both parts guide each other to jointly solve the process to a satisfied solution,avoiding the process of finding a solution mainly depends on mainly one side.By compared with the original CDCL SAT solvers and related works,the implemented solver can solve SAT problems in different categories with wide scale range.It especially performs better with less time consumed and reasonably larger memory on some instances which are not easily handled by the CDCL solver Minisat(0.56x time consumed on best instance,1.88x memory used(actually dozens MB)on worst instance compared with Minisat).When setting the appropriate mechanism and parameters in GA part,this solver even used lower memory in the meanwhile(0.76x time consumed and 0.62x memory used in average on the largest instance).It empirically shows the obvious effectiveness on proving the unsatisfiability on UNSAT application instances compared with complete solvers,and show the advantages of applying GA than simply choosing the local search as the incomplete part of a hybrid solver.The proposed solver is a complete solver that combines the strength of both GA and CDCL sides and has potential to perform better on more SAT problems,which shows the promising prospect to apply itself on solving more real-world application problems.