SAT Problem Solving Method And Its Application Research On Clique Problem

The satisfiability problem(SAT)is the first proven NP-complete problem,which occupies an important position in artificial intelligence and computer science,and many problems can be reduced to SAT.Recently Yang et al.proposed a new extension rule method based on local search method(ERACC),which breaks through the limitation of instance with large scale.However,the performance of ERACC on k-SAT(k>3)instances is not satisfactory,so we propose two new approaches based on extension rule.Secondly,with the development of SAT solving technology,the research on extended problem such as Max SAT problem,WPMS problem and #SAT problem has also made great progress.Among the above problems,the WPMS problem has a wide range of applications,such as the application of related clique problem.The clique problem includes maximum clique problem,maximum weight clique problem,maximal clique enumeration,etc.In this paper,we present a top-k maximal weight clique problem,which is a variant of maximal clique enumeration.Top-k maximal weight clique problem is to find the first k maximal weight clique in a given graph.And a new algorithm for this problem is proposed.The main innovations are as follows:(1)Two new methods for solving SAT problem based on extension rule are proposed.Firstly,we use the idea of IMOM to generate initial maximum terms when the algorithm searches the solution space composed of maximum terms.Inspired by CCA heuristic,CCA?ER heuristic strategy for extension rule reasoning is designed to provide a certain opportunity for the literals of the variables whose configurations have not been changed since their last flips in maximum terms.Then a new clause weight updating strategy PAWS?ER is proposed for clauses which can expand or can not expand current maximum term.Finally,for clauses which can not expand current maximum term,the attribute Subscore?ER of the variable is given and its derived attributes CScore?ER and HScore?ER are proposed.The variable's attribute Subscore?ER is used to break tie.Cscore?ER and Hscore?ER are used for the selection of variables corresponding to the flipped literals in greedy and random models respectively.(2)A method for solving top-k maximal weight clique problem is proposed.Firstly,we separate a critical subgraph from the input graph.The vertex set of the critical subgraph is composed of top-q degree vertices and their neighbors.The subgraph is coded as the WPMS problem,and the WPMS solver Dist is used to obtain the maximal weight clique.Secondly,in order to make Dist more efficient in finding maximal weight clique,some new strategies are proposed and incorporated into Dist.The main process is as follows: if there is a newly added variable,select the newly added variable with a certain probability p1,if there is a newly added variable but the probability is not in p1 or there is no newly added variable,randomly select a variable from the candidate set Vm with a certain probability p2,where Vm is a variable set composed of the first m variables that appear the least number of times in the candidate solution.Otherwise,variables are selected according to the variable selection strategy of Dist.Finally,this algorithm expands the critical subgraph and carry out iterative solution,in which enlarge critical subgraph by increasing the value of q.The algorithm ends until no new maximal weight clique is found or the maximum steps are reached.This paper studies SAT problem solving methods and the application of WPMS related solving techniques in top-k maximal weight clique problem,and the corresponding methods of the above two problems are tested respectively.For SAT problem,when the given formula is k-SAT(k>3)instances,the solving efficiency of ERACC?IAPS and CERACC?IAPS proposed in this paper is significantly better than that of ERACC and other extension rule-based methods.Compared with some popular local search algorithms at present,there have certain advantages in some instances.For top-k maximal weight clique problem,in order to adapt to top-k maximal weight clique problem,this paper modified four maximal clique enumeration algorithms Tomita,Hybrid,Degeneracy and D2 K algorithm.When given benchmark instance is DIMACS,compared with the modified algorithm,the algorithm proposed in this paper is obviously superior to other comparison algorithm in terms of solution quality and time.