Research On Local Search Algorithm On Solving Diversified Top-k Maximum Satisfiability Problem

Max SAT,a well-known NP-hard problem,has a significant impact on computer science and theoretical fields,providing an effective solution for complex problems.The core of the problem is to find the assignment that satisfies the most clauses.Max SAT has broad application prospects,such as intelligent planning and scheduling,probabilistic reasoning,protein structure construction,etc.However,in these practical applications,there are usually not only single but k different solutions.Taking this as a starting point,the diversified Top-k Max SAT problem is studied,which is an extension of the Max SAT problem.It aims to find k assignments that satisfy all hard clauses and together satisfy the maximum number of soft clauses.The algorithms for solving these problems can be roughly divided into complete and incomplete categories.Complete algorithms can guarantee finding the best solution,but when facing large-scale problems,such algorithms always require a lot of computational work,leading to running time and memory consumption far beyond acceptable ranges and becoming impractical for real-world applications.In comparison,incomplete algorithms have less memory usage and can quickly find solutions,especially for solving large-scale problems,and have significant advantages.However,when the incomplete algorithm finishes searching,the obtained solution may not be the optimal solution,and if it cannot find a solution,it cannot determine whether the proposition has a solution.Nevertheless,many problems do not require high accuracy in their solutions,and incomplete algorithms have considerable advantages in these problems.Local search algorithms are representative incomplete algorithms,and based on this,an algorithm LS-DTKMS based on local search is proposed for solving the problem.The following innovations are made:(1)To avoid highly overlapping assignments,a new variable scoring function is designed to select variables.Unlike the previous way of evaluating variable superiority only in the current assignment,this function evaluates variables from both local and global perspectives.(v)is the difference in weight when flipping variable V in the current assignment,changing the clause state from unsatisfied to satisfied or from satisfied to unsatisfied.(v)emphasizes the importance of hard clauses from a local perspective;(v)is the number of soft clauses that change from unsatisfied to satisfied after the variable v is flipped,while(v)considers the contribution of flipping variables to the number of satisfied soft clauses from a global perspective.The algorithm evaluates the influence of the candidate variable on the current assignment and the set of assignments containing k assignments,considering the increase or decrease of the weights of soft and hard clauses.By calculating the variable scores,the algorithm can avoid falling into local optima,making the selection of flipping variables more reasonable.(2)A heuristic strategy LS-DTKMS is proposed to improve the diversity of algorithm search by using the Best from Multiple Selections(BMS)with probability sampling.In addition,a concept of the number of private soft subclauses is introduced to evaluate the importance of assignments,which means the number of soft subclauses satisfied by an assignment alone,rather than the total number of soft subclauses satisfied by the assignment.Based on this,a new assignment scoring function is designed,because a higher total number of satisfied soft subclauses by an assignment does not necessarily mean that the assignment is the best for solving the problem instance.Instead,the quality of an assignment is judged by the number of private soft subclauses satisfied by the assignment.(3)Based on the assignment scoring function,a new assignment set updating rule is designed.In the assignment set updating phase,the updating rule first selects the assignment with the lowest score in the current assignment set and iteratively updates it using the assignment updating mechanism,while ensuring that the updated assignment satisfies the corresponding rules and is better than the previous assignment,before putting it into the assignment set.This ensures that the contribution of each iteratively updated assignment to the assignment set is better than the previous one,gradually approaching the optimal solution.Through experimental analysis,LS-DTKMS algorithm is compared with three existing excellent algorithms in traditional test cases and large-scale test cases.The experimental results demonstrate that the proposed LS-DTKMS algorithm performs well on all three types of test cases and shows stable and excellent performance as the problem size and complexity increase.