On Exact Algorithms For SAT And Related Problems

Given a CNF formula ?,the SAT problem is to find an assignment of the variables that satisfies all the clauses of ?,the MinSAT problem is to find an assignment that can unsatisfied most clauses,the MaxSAT problem is to find an assignment that can satisfy most clauses.These problems are the most classical NP problems.They are widely used in practical problems such as circuit control,community detection,resource location,AI planning,supply chain optimization,etc.They are also closely related to other classical NP problems such as maximum independent set,minimum vertex coverage,graph coloring,etc.There are great theoretical significance and application value to study the algorithm for solving these problems.Current algorithms for solving these problems mainly include two categories: heuristic algorithms and exact algorithms.Heuristic algorithms can usually give relatively high quality solutions in short time but can not guarantee that the solution is optimal.By searching the whole solution space of the problem,the exact algorithm can ensure that the final solution is the global optimal solution.Although the time complexity of existing exact algorithm for solving SAT problem is exponential in the worst case,the research progress in recent years has greatly improved the practical solving ability of the exact algorithms.In this paper,our studies include two parts: the exact algorithm of CDCL SAT solvers that based on DPLL algorithm,and provides a complete calculus for MinSAT and also extended it to solve the MinSAT problem of the multiple-valued clausal forms known as Signed CNF formulas.These two problems are closely related,because the most important point of accurate algorithm for solving SAT problem is to find conflicts as soon as possible to reduce the search space,but how to find conflicts faster is very difficult.The goal and strategy of solving MinSAT are to find the most conflicts from the clauses of the input CNF.The study of MinSAT's strategies for finding the most conflicts and the relationship between these conflicts will also be of great help to the study of SAT.All the research work in this paper is closely related to finding conflict quickly.For SAT problem:This paper focuses on three key strategies: branching heuristics,clause database reduction and clause minimization.The specific work is as follows:We propose a branch heuristic strategy that based on complete implication graph.Because the existing branch heuristic strategies are based on the past involvement of variables in past conflict,except for some different parameters,these heuristics compute the score of a variable in the same manner at the beginning,middle and end of the search process.The scores of all variables in a conflict are incremented by a value without considering how these variables contribute to the conflict.However,at the beginning of the search,the score of a variable is not sufficiently accurate because it is based on aggregated occurrences in very few conflicts.Therefore,we propose a branching heuristic that score variables based on the complete implication graph that more information are considered in the initialization phase of a CDCL SAT solver.The empirical results demonstrate that using the proposed branching heuristic in the initialization phase can significantly improve the performance of solvers.Original CDCL SAT solvers often contain redundant literals.This may have a negative impact on the performance of solvers because redundant literals may deteriorate both the effectiveness of boolean constraint propagation and the quality of subsequent learned clauses.To overcome this drawback,we propose a clause vivification approach that eliminates redundant literals by applying unit propagation.The proposed clause vivification is activated before the SAT solver triggers some selected restarts and can be used for vivify both original and learned clauses.One of the SAT solvers described here was ranked first in the main track of SAT Competition 2017 thanks to the incorporation of the proposed clause vivification.That solver was further improved in this paper and won the bronze medal in the main track of SAT Competition 2018.We present a measure called nbSAT based on the saved assignment to predict the usefulness of a learnt clause when reducing clause database in Glucose 3.0.The learnt clauses are essential for the performance of a CDCL SAT solver.However,the solver is slowed down when there is a large number of learnt clauses,the solver will be slow during the UP process.Moreover,these learnt clauses can also overflow the memory.So the solver need to measure the quality of learnt clause and delete some learnt clauses regularly.The proposed measure nbSAT,together with a resolution method to keep the learnt clauses or resolvents produced using a learnt clause that subsume an original clause,makes Glucose3.0 more effective for the application and hard combinatorial instances from the SAT 2014 competition.One of the most important strategy for solving SAT problems is to find conflicts as soon as possible thus can reduce the search tree.But it is not easy to find conflicts fast.Many state-of-art solvers can't find a better way at present.Progress tends to stagnate and saturate.The goal and strategy of the MinSAT problem is to find the maximum number of unsatisfied clauses.The purpose of our research on MinSAT is to find inspiration for finding conflicts faster by studying MinSAT's strategies for finding the minimum number of unsatisfied clauses,and the relationship between these conflicts.MaxSAT,unlike SAT,is only a natural extension of the SAT problem,aim to find the minimum number of unsatisfied clauses.It may be limited in helping us solving SAT problem.Therefore,we have done some research on bool MinSAT and extended it to multi-valued MinSAT.According to the improved algorithms mentioned above,the practical ability of SAT exact algorithm to solve problems is significantly improved,and we also won the gold medal and bronze medal in 2017 and 2018 SAT competition respectively.