A General Clause Weighting Method for Solving the Weighted Partial MaxSAT Problem
The Maximum Satisfiability Problem(MaxSAT)is an optimization form of the well-known Satisfiability Problem(SAT)and a classic NP-hard combinatorial optimization problem.The Weighted Partial MaxSAT(WPMS)is the most general type of MaxSAT problem,which includes hard clauses that must be satisfied,corresponding to the constraints in optimization problems,and weighted soft clauses that correspond to the optimization objective in optimization problems.WPMS aims to satisfy all hard clauses while maximizing the total weight of the satisfied soft clauses.Many optimization problems in industrial scenarios and academic fields can be trans-formed into WPMS for solving.Therefore,WPMS has a wide range of application domains and is of important research significance.The local search method is a well-known and widely studied incomplete method for solving WPMS.The clause weighting technique is an effective and crucial technique that is commonly used in WPMS local search algorithms,which assigns dynamic weights to clauses and updates them during the search process to guide the search direction,helping the algorithm escape from local optima.The most advanced WPMS local search algorithms have proposed or adopted effective clause weighting techniques to help them search in different solution spaces.However,existing clause weighting techniques only update the dynamic weights of clauses based on the current local optimal solution without considering any historical information,which may limit the perspective of clause weighting and lead to inaccurate guidance of search direction.To address this issue,a new clause weighting technique called Hist-Weighting(Clause Weighting with Historical Information)is proposed,which simultaneously considers the current and historical information to update the dynamic weights of clauses,in order to improve the search accuracy and efficiency of the clause weighting scheme and the local search algorithm.Specifically,Hist-Weighting assigns greater dynamic weight increments to clauses that are not satisfied by both the current and historical local optima,making the algorithm more inclined to satisfy clauses that have not been satisfied for a long time and are difficult to satisfy,so as to improve the accuracy of the clause weighting scheme.In addition,in Hist-Weighting,the increment of clause dynamic weights can be adaptively adjusted to make the clause weighting scheme more flexible.Hist-Weighting also sets upper and lower limits for the increment of dynamic weights in clauses,ensuring the stability of the clause weighting scheme.To evaluate the performance of the proposed Hist-Weighting clause weighting technique,it was applied to three state-of-the-art WPMS local search algorithms,namely BandMaxSAT,SATLike3.0,and CCEHC.The experimental results on all WPMS instances of the incomplete track of the last five years of MaxSAT Evaluations show that the improved algorithm using Hist-Weighting can increase the number of winning instances by about 10％to 60％compared to the baseline algorithm,indicating the effectiveness of the proposed Hist-Weighting clause weighting technique in solving WPMS.In addition,ablation studies are performed by comparing the improved local search algorithms using Hist-Weighting and their variant algorithms,indicating the effectiveness of the mechanisms in Hist-Weighting,including restricting the upper and lower limits of dynamic weight increments and adapting dynamic weight increments.
MaxSAT problemlocal searchclause weighting techniquehistorical information
NETL
NSTL
万方数据
