The Dynamic Convexized Method For Weighted MAX-SAT Problems

The Satisfiability problems (SAT problems for short) has been widely used in thehot areas of Operations Research, Artificial Intelligence，VLSI designing and testingand Computer Science nowadays, and it is the first problem proved to be NP-hard. Itis outstanding value of solving SAT problem in theory and applications. Completealgorithm spends a lot of time for solving SAT problems and can only solvesmall-scale ones, so it is difficult to apply it to practical problems. Since the ninetiesof last century, the research of SAT algorithms turns to incomplete search, especiallythe local search algorithms, although incomplete algorithms can’t be guaranteed tofind a solution, they have been found to be effective in tackling the large SATproblems. Note that SAT problems are a special case of the weighted MAX-SATproblems and algorithms for weighted MAX-SAT can be also suitable for SATproblems.In this thesis, we are researching well-known algorithms GRASP andGRASP+PR for SAT and weighted MAX-SAT problems, summing up thesealgorithms to improve performance and the strategy or mechanism used by jumpingout of the local optima. How to avoid getting trap in local optima or how to jump outthe trapped local optimal solution to improve the computational efficiency is the mainbottleneck encountered in the local search algorithms for SAT problems. The mainpurpose of this article is through effective way to solve how to jump out the trappedlocal optimal solution reasonably. Papers [50] and [51] present a local search methodfor nonlinearly constrained nonlinear integer programming problem over a boundedbox. This method is constructed based on an auxiliary function, it transforms theoriginal problem to a new combinatorial optimization problem by auxiliarytransformation. We prove the original and new problems have the same optimalsolution in the feasible region. Combined with local search strategy in the process ofminimizing the auxiliary function, and by increasing the value of a parameter canescape successfully from previously converged local minimizers when algorithm getsstuck at local optima. The above approach is called dynamic convexized method [50][51], and we extend this method for solving SAT problems. We present twodynamic convexized method based algorithms and compare them with GRASP andGRASP+PR on a standard set of benchmark instances, the comparisons show thehighly effective convergence of our algorithms.Secondly, we apply the dynamic convexized method to solve graph coloringproblem (GCP for short). By constructing auxiliary function and using the localsearch algorithm FM, we use the constructed algorithm to solve different scales ofGCP instances in the experiment, and compare with the known GRASP; Empiricalresults indicate that the proposed DCM implementation outperforms GRASP on threeinstances.Finally, we make an experimental analysis of Local Search Algorithms. Wesummarize the research on local search algorithm for SAT and GCP problems in thisarticle and make a prospect of corresponding work at last.