Research On The Game Algorithm To Maximum Satisfiability Problem

The Maximum Satisfiability Problem(MaxSAT)is one of the most important prob-lems in artificial intelligence research fileds,it can naturally encode and solve many practical problems,and developing effcient MaxSAT algorithms is important from both a theoretical and a practical point of view.In recent years,due to the developing of in-dustrial applications and scientific research,the scale of MaxSAT instances is doubled and redoubled.In order to solve the new MaxSAT instances,we proposed two variants of game algorithms in this paper,including the basic game algorithm bgmaxsat,which is applied to solving general MaxSAT instances,and the grouping game algorithm bg-maxsat|_m,which is more suitable to solve large scale MaxSAT instances.The contributions of this paper are summarized as follow four points.Firstly,we proposed a new modelling method that maps the MaxSAT instance to the boolean game model,and utilzes the players' selection on strategies in game to simulate the assign-ment on variables in MaxSAT instances.The game players select the strategies based on the redefined goal function and payoff calculation function,and update self strategy in the view of other players.Secondly,we improved the classcial static game model by the properties of MaxSAT problem,and proposed a new dynamic game model,which is combined with dynamic payoff matricx.In dynamic game model,player's payoff is changeable during the game playing,so that players can converge to the goal function quickly.And we proposed our basic game algorithm on the top of dynamic game model,called bgmaxsat,which is applied to solving general MaxSAT instances.Thirdly,we proposed an new players grouping method to avoid the tremendous players generated by large scale MaxSAT instances.To be specific,we reconstructed players' relations via undirected graph,and divided all players into several groups which makes every player be independent with others in the same group.Finnally,we proposed the grouping game algorithm based on the players grouping method,called bgmaxsat_m.In bgmaxsat_m algorithm,we set a players group as a game playing unit,and only assigned communi-cation channels between groups.In the experimental evaluations,we conducted several experiments on four bench-marks.Firstly,We evaluated bgmaxsat on 846 general MaxSAT instances,and com-pared the overall performance with three state-of-the-art algorithms,including CCLS2016,Swcca-ms and ahmaxsatl.55.And the experimental results show that bgaxsat is com-petitive with CCLS2016,and is superior to Swcca-ms and ahmaxsatl.55.Secondly,we evaluated bgmaxsat_m on 100 large scale MaxSAT instances with variable scale ex-ceeds 105,and compared the overall performance with five state-of-the-art algorithms,including CCLS2016,wbo,Open-wbo,pwbo and CnC-LS.The experimental results show that bgmaxsat_m is obviously superior to CCLS2016,wbo and Open-wbo on all large scale MaxSAT categories.Meanwhile,bgmaxsat_m is superior to Open-wbo and CnC-LS on large scale random MaxSAT instances,but it is not dominant in large scale industrial MaxSAT instances.