Researches On Incomplete And Complete Algorithms For Maximum Satisfiability Problem

The maximum satisfiability problem(Max SAT)is an optimization extension of the satisfiability problem(SAT),the first proved NP-complete problem.As a constrained optimization model,Max SAT has a strong expressive ability.Many problems in academic research and real world can be transformed into Max SAT to apply its solving technologies.In recent years,researchers have carried out researches on solving Max SAT in two approaches,namely incomplete algorithms and complete algorithms.Significant progress has been made in solving methods and technologies of Max SAT.The goal of incomplete algorithms is to find a better solution in a shorter time,without guaranteeing the global optimality of the solution,while complete algorithms need to ensure the optimality of the solution.The solvers of incomplete algorithms have obvious advantages in non-complex instances with random,crafted or some specific structures,but they are weaker than the solvers of complete algorithms in large-scale complex instances such as industrial instances.Most of the current excellent complete solvers are based on the SAT solvers,that is,the SAT solvers are called in Max SAT solvers to indirectly exert the powerful solving ability of the clause learning strategy for SAT.As another class of complete solvers for Max SAT,the solvers based on Branch and Bound(Bn B)have developed slowly in recent years.This dissertation has carried out in-depth research on the incomplete algorithm and has finished the following three works.Firstly,we propose a new local search strategy,called the path-breaking strategy and an algorithm combining the path-breaking strategy and the adaptive restart and mutation strategy.The path relinking strategy in local search is studied by designing experiments and analyzing the experimental results,and reasons for its poor performance in Max SAT solving are found.Based on the above analysis,we propose a breaking condition and improve the initial solution strategy,thus propose a new path search strategy called the Path-Breaking(PB).Then,we design an iterative search framework combined with the restart strategy for the PB strategy.In order to effectively utilize the local optimal information,the mutation strategy for the local optimal solution is proposed,including a strong and a weak mutation.Finally,an efficient local search algorithm is formed,called the IPBMR(Iterative PathBreaking approach with Mutation and Restart strategies).The experimental results show that IPBMR outperforms the best local search algorithms at that time,such as CCLS,etc.In most instances of the international Max SAT Evaluation(MSE)MSE 2016,the solving speed of IPBMR is one order of magnitude higher than that of CCLS.Secondly,we analyze the reasons for the poor performance of non-complete algorithms in solving large industrial cases,and propose a new algorithm for constructing initial solutions,which includes a global information feedback strategy.Then,we propose an algorithm combining initial solution constructing strategy and PB strategy.The IPBMR is experimentally analyzed,and its weaknesses in solving large industrial instances are found and the reasons are analyzed.Then,we propose an algorithm for constructing initial solutions based on tree assignment,called the ASIF(Assignment approach by Search Information Feedback).Some meaningful quantities are selected and defined in the search process.These quantities are used to design a global search information update and feedback mechanism.This mechanism accumulates the experience in the initial solution construction process and provides guidance information for the construction of initial solutions.It feeds back and updates the global experience according to the effect of the initial solutions,so as to effectively utilize the experience and information in the construction process.Taking ASIF as the initial solution construction algorithm,combined with the PB strategy in IPBMR,a new algorithm is formed called PB-ASIF(Path-Breaking approach with ASIF strategies).The experimental results show that the ASIF algorithm can quickly construct high-quality initial feasible solutions,and the ability of PB-ASIF to solve industrial instances is significantly higher than that of IPBMR,which effectiveness improves the effect of using PB strategy to solve industrial instances.Notably,PB-ASIF has the potential to improve the solving ability of other solvers.Thereafter,we study the conflict-driven clause learning strategy and branch and bound strategy for complete algorithms,then propose the clause learning strategy for the Max SAT problem and a new complete algorithm combined with the clause learning strategy and branch and bound strategy.At present,there is no conflict driven clause learning method directly used for solving the Max SAT problem.Relying on the progress of SAT solving technology will limit the development of the complete algorithm for Max SAT.The branch and bound based algorithms have been developed slowly in recent years.It does not directly apply clause learning strategy or applicable effective knowledge accumulation strategy.In order to construct the knowledge accumulation strategy of the complete algorithm,we propose a clause learning strategy for solving the Max SAT problem,and design a new bound strategy for the branch and bound in order to solve large-scale instance.Then,combining with the improved branch and bound strategy and the new clause learning strategy,we propose a new complete algorithm for solving the Max SAT problem,called the Max CDCL.The experimental results show that the algorithm rank in the top five compared with the solvers in MSE2020.Many of the instances can be solved by Max CDCL but not by SATbased solvers,indicating that the new clause learning strategy for Max SAT has strong potential for further development.Like the conflict driven clause learning strategy for the SAT problem,the clause learning strategy for Max SAT has shown strong competitiveness just after being proposed.The development of the clause learning strategy for Max SAT will effectively promote the improvement of the solving ability of complete algorithm for Max SAT.Moreover,Max CDCL effectively improves the solving performance of complete algorithms based on branch and bound,and provides a new perpective for further development.