Information Entropy Based Local Search Max-sat Algorithm

The satisfiability problem is known as the “seed” for many NP complete problems because it is used frequently in real life.It draws great attention from experts and scholars in the computer field,and has been applied in artificial intelligence,computer vision and combinatorial optimization.Given the importance of the SAT problem,this thesis focuses on the Max-SAT problem.The solutions to Max-SAT problem can be divided into complete algorithm and incomplete algorithm.Complete algorithm would find the optimal solutions in a long time,while incomplete algorithm could only find sub-optimal solutions in a fixed time.MaxSAT problem is NP-hard due to the difference of CNF's complexity and size,making it necessary to use incomplete algorithms as a temporary solution to this problem.In this thesis,an efficiently incomplete algorithm is proposed through studying the unweighted Max-SAT problem.The aim of this algorithm is to find a set of variables assignment,which can meet the maximum number of clauses in a given CNF.The main work of this article is as follows:1.This thesis studies the classical incomplete algorithms in China and abroad,including GSAT algorithm,CCLS algorithm and cross-entropy based satisfying algorithm.It also compares the preprocessing of different incomplete algorithms on the CNF respectively.In the process of solving the CNF,preprocessing can make the subsequent variable search faster.The variables in the CNF are different in diverse clauses.Through the study and research of information entropy,the author found that information entropy can distinguish the importance of variables in the current CNF.Thus,more important variables are chosen to put in the variable pool as candidate variables.Therefore,this thesis selects information entropy,which has not been used to solve such problems before,as the first step of preprocessing.2.The aim of this algorithm is to select the variables that are optimal for the current CNF and make the maximum number of clauses to meet the state.As for the variable put into the candidate variable pool after the preprocessing,the local search is carried out by using the association degree method to further select the better variables.Then,the value of the variable is assigned by the pruning method so that the number of clauses is minimized every time.After that,the CNF is updated to perform the next iteration.3.Finally,to test the effect of the algorithm of this thesis,using cross-entropy for satisfiability and the algorithm of the global Max-SAT competition in 2016 are selected as comparison experiments.Through analysis of the experimental results,the algorithm of this dissertation improves the number of search clauses that can be satisfied compared with other algorithms,and it also improves the speed of search to satisfy clauses significantly.