求解加权偏MaxSAT问题的通用子句加权方法  

A General Clause Weighting Method for Solving the Weighted Partial MaxSAT Problem

作　　者：郑迥之 何琨[1] ZHENG Jiong-Zhi;HE Kun(School of Computer Science and Technology,Huazhong University of Science and Technology,Wuhan 430074)

机构地区：[1]华中科技大学计算机科学与技术学院,武汉430074

出　　处：《计算机学报》2024年第6期1341-1354,共14页Chinese Journal of Computers

基　　金：国家自然科学基金项目(U22B2017)资助.

摘　　要：最大可满足性问题(Maximum Satisfiability Problem,MaxSAT)是著名的可满足性问题(Satisfiability Problem,SAT)的优化形式,也是一个经典的NP难组合优化问题.加权偏MaxSAT(Weighted Partial MaxSAT,WPMS)是最一般的一类MaxSAT问题,其中包含了必须要满足的硬子句,对应了优化问题中的约束条件,以及带权重的软子句,对应了优化问题中的优化目标.WPMS旨在满足所有硬子句的同时最大化被满足软子句的权重之和.工业场景中和学术领域中的许多优化问题都能够转化成WPMS问题进行求解,因此WPMS具有广泛的应用领域和重要的研究意义.局部搜索方法是求解WPMS问题的一种著名且被广泛研究的非完备方法.子句加权技术是WPMS局部搜索算法中常用的一种有效且关键的技术,通过为子句赋予动态权重并在搜索过程中更新它们以引导搜索方向,帮助算法逃离局部最优.最先进的WPMS局部搜索算法都提出或采用了有效的子句加权技术,以帮助它们在不同的解空间中搜索.然而,现有的子句加权技术仅根据当前局部最优解更新子句动态权重,而未考虑任何历史信息,可能导致子句加权的视野局限,对搜索方向的引导不够准确.为了解决这一问题,提出了一种新的子句加权技术,称为Hist-Weighting(Clause Weighting with Historical Information),同时考虑了当前及历史信息来更新子句的动态权重,以改进子句加权机制和局部搜索算法的搜索精度和效率.具体而言,Hist-Weighting为那些同时被当前和历史局部最优解所不满足的子句赋予更大的动态权重增量,使算法更倾向于满足那些久未被满足且难以被满足的子句,提高子句加权的准确度.此外,在Hist-Weighting中,子句动态权重的增量能够根据子句中的变元得分自适应地调整,使子句加权更具有灵活性.Hist-Weighting还为子句动态权重的增量设置了上下限,保证了子句加权的稳定性.为了评估所提出�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

关 键 词：最大可满足性问题 局部搜索 子句加权技术 历史信息 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]