A New SAT Algorithm Based On Regression Analysis And DCM Models

The Boolean satifiability (SAT) problem is the first problem showed to be NP-complete. Many problems in the application domain such as computer aided de-sign, artificial intelligence, cryptanalysis, electronic design automation, planning etc., can be formulated as SAT problems. It has been widely observed that there is no a SAT solver which can solve all the SAT problems, there are still a lot of problems which are not resolved. Modern SAT solvers can be divided into two categories:one is based on the DPLL search method; the other is based on local search algorithms. The DPLL-based SAT solver consists of two main types of approaches:look-ahead and conflict-driven. Look-ahead solvers are very strong on unsatisfiable random and crafted instances, conflict-driven solvers dominate on industrial instances, while lo-cal-search techniques are unbeatable on large satisfiable random instances.Since different solvers perform best on different instances, this paper introduces the strategy of algorithm portfolio for constructing a general SAT solver which choosing the optimal solver by some model. The regression analysis model constructs the relationship between the instance's features and the runtime of the algorithm for each instance, predicts each algorithm's runtime by the feature computation and se-lects the solver which has the shortest runtime to solve the problem. The Dirichlet compound multinomial (DCM) model makes solver behavior as the object, the run's outcome as the feature to get the probability of each algorithm on the instance and chooses the solver most likely to solve the problem. Finally, the hybrid model which mixed the regression analysis and DCM techniques selects a set of optimum solvers by the regression analysis model first, and then choose the solver most likely by DCM model to solve the problem. The experiments show that the profile algorithms can significantly increase the number of solved instances. The hybrid model solves more instances than the DCM does, while the DCM model solves more instances the regression analysis does. On the runtime of each algorithm, for the simple instances, the hybrid model and regres-sion analysis model are almost and both better than DCM model. For the complex in-stances, the hybrid model and DCM model are almost and both better than regression analysis model. Overall, the hybrid model integrates the advantages of the two models. Regardless of the solved instance's number or the runtime, it is slightly better than the previous two.