给定一个命题逻辑合取范式(conjunctive normal form，CNF)，可满足性问题(satisfiability problem，SAT)是判断其是否可被满足的一个判定问题．最大可满足性问题(maximum satisfiability problem，MaxSAT)是SAT问题的优化版本，是一个经典的具有NP难度的组合优化问题，并且具有广泛的现实应用，例如应用于解决规划问题[1-2]、路径问题[3-4]、群组检测[5]、最大团问题[6-8]和时间表问题[9]等．给定一组布尔变量{x1,x2,⋯,xn}，xi∈{0，1} (i=1,2,⋯,n)，CNF公式中的各种组成成分定义如下．文字是变量本身xi或者是它的否定形式x¯i，当且仅当变量xi为真时(即xi=1)，正文字xi被满足，反之当且仅当xi为假时(即xi=0)，负文字x¯i被满足．子句是文字的析取，例如：ci=li1∨li2∨⋯∨lip，其中子句ci由p个文字组成，lij表示子句ci中第j个文字(j=1,2,⋯,p)．当一个子句中至少有一个文字被满足时，该子句被满足，否则该子句不满足．CNF公式F是子句的合取，即：F=c1∧c2∧⋯∧cm，当且仅当公式F中所有子句都被满足时，公式F被满足．V(F)表示一个CNF公式F中所有变量的集合，映射α:V(F)→{0,1}表示V(F)的一组赋值．若α将所有变量都映射成一个布尔值，则称其为完全赋值，否则为部分赋值．给定一个CNF公式F，MaxSAT及其各种变体问题的定义如下．MaxSAT问题的目标是找到一个完全赋值α，使被满足的子句数量最多．加权MaxSAT问题(weighted MaxSAT，WMS)赋予每个子句一个权重，旨在找到一个完全赋值α，使被满足的子句的权重之和最大．部分MaxSAT问题(partial MaxSAT，PMS)是MaxSAT问题的一个变体，其中子句被分成硬子句和软子句两种，其目标是找到一个完全赋值α，满足所有的硬子句，并使被满足的软子句数量最多．MaxSAT问题可以被看作硬子句数量为0的特殊的PMS问题．更一般地，PMS中每个软子句c被赋予一个权重w(c)，得到的问题称为加权部分MaxSAT问题(weighted partial MaxSAT，WPMS)，其目标在于找到一个完全赋值α，满足所有硬子句，并使被满足的软子句的权重之和最大．PMS问题可以被看作软子句权重都为1的WPMS问题．在解决实际的PMS或WPMS问题时，通常将每个硬子句的权重视为所有软子句的权重之和加1．另外，须要说明的是，MaxSAT问题的解的评估函数通常是不满足子句的权重之和．为了更好地区分不同类型的MaxSAT问题，本研究后续将用纯MaxSAT表示原始的MaxSAT问题，即不带权且不区分硬软子句的MaxSAT问题，用(W)PMS表示PMS和WPMS问题，用MaxSAT表示各类问题的统称．现有的解决MaxSAT问题的算法可分为完备算法和非完备算法．完备算法能够保证得到最优解，但当用于解决大规模实例时，可能难以在合理的时间内停止．MaxSAT问题的完备算法主要分为分支定界算法[10-15]和一种迭代调用SAT求解器的算法(SAT-based算法)[16-20]．分支定界算法通过搜索二叉树来求解MaxSAT问题，二叉树的每一个节点针对一个未被赋值的变量产生真、假两个分支．分支定界算法在随机生成和人工生成的算例上有较好的表现，但在工业算例上表现较弱．SAT-based算法每次迭代都会通过增加或减少变量的方式来调整CNF公式，并调用SAT求解器来更新问题的下界或上界，直到找到MaxSAT的最优解．SAT-based算法是目前最好的完备算法，在工业算例上有很好的表现．非完备算法虽然无法保证所得到的解的最优性，但能够在合理的时间内得到近似最优解甚至最优解．MaxSAT问题的非完备算法主要包括近似算法[21-24]、基于最小校正子集(minimal correction subset based，MCS-based)的算法[25-28]及局部搜索算法[29-34]．对于(W)PMS问题，由于近似算法难以保证解的可行性，因此主要用于解决纯MaxSAT问题．MCS-based算法将MaxSAT问题转化为找到权重之和最小的软子句集合，即一个MCS，使得存在至少一个赋值能够满足所有硬子句及除该MCS中所包含的软子句之外的所有软子句．MCS-based算法同样须要多次调用SAT求解器，但其性能无法与SAT-based算法相比．局部搜索算法是最具代表性的非完备算法，这类算法通过迭代地翻转变量的赋值在搜索空间中寻找高质量的解．目前最好的(W)PMS的局部搜索算法在解决工业算例中表现出与最好的SAT-based算法相当的性能．MaxSAT问题是一个有价值的且富有挑战性的组合优化问题，具有重要的现实应用价值．但目前仅存在针对MaxSAT问题某类求解算法的综述和对比，如SAT-based算法[35]或局部搜索算法[36-37]，而缺乏文献对MaxSAT问题的各种算法进行较为全面和系统的梳理，本研究对近年来MaxSAT问题的求解算法进行了归纳总结，旨在综述MaxSAT问题的完备及非完备算法的最新研究进展，同时讨论了求解MaxSAT问题的挑战及未来研究方向．1 MaxSAT问题的完备算法1.1　分支定界算法分支定界算法通过搜索二叉树来遍历解空间，典型的MaxSAT分支定界算法流程如图1所示．在算法起始时，所有变量都未被赋值，搜索树中的每个节点代表一个变量，其左右两个分支表示给该变量赋真值或假值．在搜索过程中，算法会即时地更新上界和下界，起始时上界可以等于所有软子句权重之和，当二叉树搜索至叶子节点时，即所有变量都被赋值，若当前解好于上界，即不满足子句的权重之和小于上界，则更新上界，下界则在每次给一个新的变量赋值时根据评估方法计算得到；若当前部分赋值的下界大于上界，则进行剪枝和回溯操作．算法在遍历完整个搜索树后退出，所得上界即是MaxSAT问题的最优解．代表性的分支定界算法有WMaxSatz[10-11]，MiniMaxSat[12]，Akmaxsat[13]及Ahmaxsat[14-15]．10.13245/j.hust.220214.F001图1MaxSAT分支定界算法流程近年来，相关研究主要从以下三个方面改进MaxSAT问题的分支定界算法：搜索树的分支策略、部分赋值的扩展方法(即推理规则)和下界估计方法．本节将从这三个方面介绍近年来的MaxSAT问题的分支定界算法．1.1.1　搜索树分支策略在MaxSAT问题的分支定界算法中，搜索树的分支策略主要用于选择下一分支节点．好的分支策略有助于算法快速剪枝，提高搜索效率．早期的MaxSAT分支定界算法的分支策略直接采用了SAT问题中的分支策略，或对其做了少量的改动．例如，算法BFA[38]采用了SAT中的分支策略MOMS[39]，该策略首先选择未确定的文字数量最少的子句，注意可能选择多个子句，然后在这些子句中选择出现次数最多的变量作为下一分支节点．随后有研究者在BFA算法的基础上增加了下界估计机制[40-41]，并对比了采用MOMS策略和另一SAT分支策略，Jeroslow-Wang (JW)策略[42-43]的性能，结果显示在求解(加权)Max-2-SAT问题(Max-k-SAT问题即每个子句都含k个文字的MaxSAT问题)时，JW策略比MOMS策略有更好的效果．JW策略定义了一种打分机制，使出现次数多的、出现在较短子句中的变量得分更高，然后选择得分最高的变量作为下一分支节点．实际上，MOMS策略和JW策略的思想是一致的，即倾向于得到更多的单元子句，有助于得到更紧的下界．文献[44]提出的算法同样采用JW策略作为分支节点选择策略．文献[45]针对Max-2-SAT和Max-3-SAT问题设计了不同的改进JW策略，对于Max-2-SAT问题，设置二元子句(子句中含有两个未赋值变量)的优先级高于单元子句(子句中仅含一个未赋值变量)，目的在于先选择二元子句中的变量进行分支，从而产生更多的单元子句，有利于得到高的下界；对于Max-3-SAT问题，根据实例的子句数量和变量数量之比设置了变量排序打分的动态权重，提高了算法的性能．近年来的MaxSAT分支定界算法提出了更加复杂的分支策略．如WMaxSatz算法[10-11]依据正、负文字在子句中出现的次数给每个未赋值的变量进行打分，变量的得分为对应的正、负文字得分的乘积．WMaxSatz算法选择分数最高的变量作为下一分支节点，并优先选择节点对应的正、负文字分数更高的布尔值进行赋值，其目的在于在搜索树的较高节点中获得较高的下界，同时保持其分支平衡．Akmaxsat算法[13]和Ahmaxsat算法[14-15]中的分支策略与WMaxSatz类似，其中Akmaxsat算法还根据文字是否在扩展部分赋值阶段导致产生不满足的子句来调整变量的得分．MiniMaxSat[12]是首个对带有硬子句的MaxSAT问题采用不同的分支策略的分支定界算法．当问题不含有硬子句时，MiniMaxSat采用加权的JW策略作为分支策略；当问题含有硬子句时，采用SAT问题中的变状态独立衰减和启发式方法(variable state independent decaying sum，VSIDS)[46]进行分支，该方法在搜索过程中增加冲突硬子句(如分别由变量x的正文字和负文字组成的两个单元子句)中文字的分数，并选择分数最高的变量作为分支节点，目的在于尽可能地满足冲突的硬子句．最近，MaxCDCL算法[47]将子句学习与分支定界算法相结合以解决MaxSAT问题，其中，向前看的子句学习机制能够预测出当前部分赋值扩展至完全赋值将会发生冲突的子句，MaxCDCL算法利用这些信息来改进VSIDS算法[46]，做法是将预测冲突子句中文字的分数增加．1.1.2　推理规则推理规则[10，48]是一些确定性的准则．对于当前部分赋值，依据这些推理规则，某些变量的赋值能够被确定，部分赋值能够被扩展，从而便于得到更紧的下界．首先介绍三种常见的推理规则．a. 硬单子句传播单子句传播(unit propagation，UP)是SAT问题的完备求解器中常见的推理规则，即单元子句必须被满足，因此可以确定单元子句中未赋值变量的布尔值，进而传播至含有该变量对应文字的子句．硬单子句传播(hard UP，HUP)的原理如下：在MaxSAT分支定界算法过程中，若由某个未确定的文字所组成的所有单元子句的权重之和大于或等于上界与下界之差，则这些单元子句必须被满足，否则当前部分赋值将被剪枝．b. 支配单元子句支配单元子句(dominating unit clause，DUC)规则的原理如下：对于某个未赋值的变量x，若含有其正文字的所有单元子句的权重之和大于或等于含有其负文字的所有子句的权重之和，则x必须为真，反之亦然．这是因为不满足这些单元子句的代价一定大于满足这些单元子句的代价，所以在当前部分赋值对应的最优完全赋值中，这些单元子句一定是被满足的．c. 纯文字纯文字(pure literal，PL)规则的原理如下：如果某个变量在公式中只有其正文字，则它可以被确定为真而不会导致任一子句不满足，反之亦然．以上三种经典的推理规则被广泛应用于MaxSAT的分支定界算法中[10-15，44-45，,48-50]．除此之外，许多先进的算法提出了一些更加强大的推理规则．例如，文献[45]提出了一种基于非线性规划的推理规则，将MaxSAT问题建模成非线性规划问题，为每个变量计算出一个系数，该系数的正负性决定了变量应被赋予的布尔值．Ahmaxsat算法[14-15]在估计下界的过程中动态地使用HUP，DUC和PL规则，从而确定更多变量的赋值，并提出一种多重传播源(multiple propagation source，MPS)的机制来增强HUP规则的效果．1.1.3　下界估计方法对MaxSAT的分支定界算法而言，下界估计方法至关重要，高质量的下界能够实现快速剪枝，避免不必要的尝试．下界估计方法通常须要通过UP技术检测不一致子集(inconsistent subsets，IS)[51-52]，即在UP过程中导致空子句的子句集合，进而估计出当前部分赋值扩展为完全赋值将会导致多少不满足的子句．最简单的下界估计方法就是当前部分赋值能够确定的不满足子句的权重之和[38]，由于这样的下界估计方法没有考虑未来可能产生的不满足子句，因此性能较差．更进一步的下界估计方法考虑了冲突的单元子句[40-41，53]，即由某个变量的正、负文字组成的无法同时满足的单元子句．文献[54-55]针对Max-2-SAT问题提出了更强大的下界计算方法，这些下界计算方法考虑了单元子句和二元子句之间的冲突．文献[45]提出了一种基于线性规划的下界，在当前节点，将MaxSAT实例中未赋值的部分建模成一个线性规划问题，约束每个未赋值的变量取值范围为[0，1]，再根据单元子句中变量对应的值估计单元子句是否被满足．例如，含未赋值变量x的单元子句，若线性规划解得x的值小于1/2，则判断其不满足，反之亦然．通过UP检测IS集合是MaxSAT分支定界算法中估计下界的一项关键技术[49]．其过程如下：将所有单元子句，包括UP过程中产生的单元子句，存放在一个队列Q中，遍历Q中的单元子句，对其执行UP操作，直至产生空子句，在这一过程中导致空子句产生的所有子句的集合就是一个IS．存在于已发现的IS中的单元子句不能再用于产生新的IS，即每个单元子句传播之后都会从Q中移除，这样可以保证每个IS之间相互独立．循环整个过程直至Q为空．对于纯MaxSAT问题，下界可以被估计为部分赋值所确定的不满足子句数量与UP得到的IS数量之和．显然地，MaxSAT的下界质量与UP得到的IS数量有关，因此单元子句的传播顺序影响着下界的质量．为了得到更紧的下界，文献[56]在原有技术的基础上，进一步提出了两种新的UP策略：UP*和UPS．其中，UP*维护了Q1和Q2两个队列，Q1中存放了当前公式中的所有单元子句，Q2存放了UP过程中产生的单元子句．UP*规定只有当Q2为空时才会传播Q1中的单元子句．UPS则使用一个栈S代替队列Q存放包括UP过程中产生的所有单元子句．这两种新的UP策略的思想是相似的，即每次希望用更少的单元子句检测出IS集合，将更多的单元子句保留下来，以检测出更多的IS集合，从而得到更紧的下界．此外，文献[56]还提出了另外一项IS检测技术，名为失败文字检测(failed literals，FL)[56-57]．FL采用了向前看的思想，应用于UP无法检测出更多的单元子句的情形，将UP技术与FL技术相结合，进一步提高了下界的质量．UP和FL技术主要用于IS集合的检测，为了避免在IS集合检测的过程中检测到相同的冲突，即检测到相同的空子句，须要采用MaxSAT中的重构规则(max-resolution rule)[58-60]对公式进行重构，该规则是SAT中重构规则的MaxSAT版本．目前最先进的MaxSAT分支定界算法[10-15]都采用了UP和FL技术及MaxSAT的重构规则来估计下界．最近，MaxCDCL算法[47]应用子句学习技术来指导分支定界算法中下界估计阶段的UP过程，使算法能够得到更紧的下界．MaxCDCL算法巧妙的将子句学习技术与分支定界算法相结合，极大地改进了分支定界算法，使其具有与SAT-based算法相当的性能，为MaxSAT的分支定界算法提供了新的思路．1.2　SAT-based算法SAT-based算法[61]通过将MaxSAT这一优化问题转换为一系列的SAT问题，再迭代地调用SAT求解器[62-64]来求解．SAT-based算法主要可分为两种．第一种被称为线性搜索，这类算法通过迭代地修改上界或下界得到最优解．第二种被称为核引导算法，这类算法须要计算出导致公式不满足的子句的集合，也被称为不可满足的核，再通过添加松弛变量计算满足每个核所需付出的最少代价，进而得出最优解．本节将分这两种算法介绍MaxSAT的SAT-based算法．1.2.1　线性搜索算法首先介绍迭代地修改上界的线性搜索算法[65-69]，初始化的上界可以是所有软子句的权重之和．假设实例公式F由硬子句集合H={H1,H2,⋯,Hn}和软子句集合S={S1,S2,⋯,Sm}组成，这类算法会给公式中每个软子句都添加一个松弛变量vi,i∈(1,2,⋯,m)，此时公式变为F'=H1∧ H2∧⋯∧Hn∧(S1∨v1)∧(S2∨v2)∧⋯∧(Sm∨vm)．显然，如果假设硬子句集合是可满足的，那么此时公式F'也是可满足的，因为只须要令所有松弛变量为真即可．同时，松弛变量为真的数量即等同于当前解中不满足的软子句数量．因此，MaxSAT问题即可转化为最小化松弛变量为真的数量，或最小化松弛变量为真的软子句权重之和．假设当前计算的上界为k，为了使上界更紧，算法在使用SAT求解器计算F'时，还须要添加松弛变量为真的软子句数量(或权重之和)小于k的约束，这须要用到基数约束(cardinality constraints)和伪布尔约束(pseudo Boolean constraints)的技术[63，70]．通过重复计算上界，修改约束的过程，这类算法的SAT求解器每次都会返回可满足，当返回不可满足时，说明当前计算的上界就是最优解．另外一类线性搜索算法通过迭代地修改下界来找到最优解[4，66，71]．这类算法与修改上界算法的思路相反，它们希望通过添加最少数量的松弛变量，或添加对应的软子句权重之和最小的松弛变量，使调整后的公式可满足．这类算法的SAT求解器每次都会返回不可满足，当返回可满足时，说明当前计算的下界就是最优解．还有一些算法采用二分搜索的策略来提高搜索速度[4，20，66]．这些算法须要同时维护上界和下界，每次迭代将上界和下界的平均值作为松弛变量的约束值，然后根据SAT求解器返回的结果调整上界和下界．1.2.2　核引导算法核引导算法实际上也是修改下界的算法．不同的是，当这类算法调用SAT求解器时，不仅须要返回公式是否可满足，而且如果公式不可满足，那么还须返回导致公式不可满足的核．由于每个核都是一些软子句的集合，每个核内的所有软子句无法同时满足，因此可以认为是这些不可满足核导致了整个公式不可满足．利用SAT求解器寻找不可满足核已经是一项成熟的技术[72]，核引导算法正是得益于这项技术才有实现的可能[4]．在不可满足核被检测完之后，核引导算法通过添加松弛变量来松弛权重之和最小的软子句，使每个核能够被满足，进而找到MaxSAT的最优解．最早的核引导算法[4]用于解决PMS问题，即软子句的权重都为1，算法首先检测不可满足核，然后对每个核进行独立的操作．对于每个不可满足核，为核中所有的子句添加松弛变量，再通过不断地增加松弛变量可取真值的个数找到消除不可满足核需要付出的最小代价．文献[73-74]提出了减少松弛变量个数的方法来改进文献[4]中的算法，避免由于增加过多的松弛变量导致的过高的内存消耗．以上几种方法都只能用于解决不加权的MaxSAT问题．随后，有研究者提出了能够解决WPMS问题的版本，将核引导算法扩展至能够解决加权的MaxSAT问题[75-76]．近年来，核引导算法采用了更先进的技术来改进算法的性能．部分算法通过简化基线约束来提高算法的性能，并减少资源消耗，例如：在每次迭代过程中通过重构公式来简化约束[20]；通过巧妙地提取和挖掘不可满足核中的结构来简化约束[77]；通过调整约束，限制松弛变量个数的方法来简化约束[78]．此外，有研究者在利用松弛变量消除不可满足核的过程中采用了二分搜索的方法，提高了算法的效率[79-80]．Loandra算法[19]将线性搜索与核引导两种算法相结合以解决MaxSAT问题，首先利用核引导算法计算MaxSAT实例，若没有得出最优解，则将核引导算法计算与调整的实例公式和上界输入给线性搜索算法继续计算，该算法在近年的MaxSAT evaluation (MSE)[81]上有较好的表现．SAT-based算法是目前最好的求解MaxSAT的完备算法，并且通过在每次发现更紧的上界时返回结果，SAT-based算法同样可以视为非完备算法．自2006年首届MSE举办以来，SAT-based算法多次获得完备组和非完备组各赛道的冠军．此外，由于SAT-based算法在工业算例上的优秀表现，因此在实际应用场景中，研究者们通常将问题建模成MaxSAT问题，再用SAT-based算法进行求解[1-9]．SAT-based算法的出现极大地推动了MaxSAT求解器的发展．2 MaxSAT问题的非完备算法虽然MaxSAT的完备算法很强大，但也存在着一些问题，例如，分支定界算法在工业算例上表现较差；SAT-based算法则十分依赖SAT求解器的性能，且完备算法在解决大规模问题时可能无法在时间限制内求出最优解，非完备算法具有一些其不具备的优势，如计算速度快、效率高，在某些情况下更能够适应对求解效率也有需求的应用场景．MaxSAT问题的非完备算法可分为近似算法，基于最小校正子集(MCS-based)的算法及局部搜索算法．本章将分这三类方法介绍MaxSAT的非完备算法．2.1　近似算法近似算法的结果具有近似比保证，例如，对于一个纯MaxSAT的α-近似算法(0α1)，即近似比为α的算法，其结果所满足的子句数量至少是最优解所满足的子句数量的α倍．文献[21]提出了首个贪心启发式的MaxSAT的1/2-近似算法，该算法每次满足未满足的子句中出现次数最多的文字，直至确定所有子句是否被满足．后续研究表明，将Johnson算法[21]中固定的变量访问顺序调整成随机访问能够得到更好近似算法[82-83]．随后，文献[84]提出了利用网络流模型和线性规划方法作为子程序的首个MaxSAT的3/4-近似算法．文献[85]同样展示了如何通过随机圆整线性规划结果得到一个MaxSAT的3/4-近似算法，并提出一个问题，即：是否能够不使用线性规划得到3/4的近似比？对此，文献[22-23]提出了Johnson算法[21]的3/4近似比的随机改进版本，完美地解答了这个问题．目前已证明的纯MaxSAT问题最好的近似比是一种改进的基于线性规划的松弛算法[86-87]，其近似比达到0.784 6．此外，许多研究针对特定的MaxSAT问题提出了具有更高近似比的近似算法．例如，文献[88]提出的针对Max-2-SAT问题的近似算法，其近似比达到0.94；文献[89]提出针对Max-3-SAT问题的近似算法，并证明对于公式可满足的Max-3-SAT实例，近似比可达7/8，对于公式不可满足的Max-3-SAT实例，实验结果满足了这一近似比．在解决实际的MaxSAT问题过程中，近似算法具有较大的局限性．例如，不存在针对(W)PMS问题的近似算法，因为近似算法无法保证能够得到可行解．此外，在许多时候，由于近似算法对解的性能保证无法满足实际的需求，因此和其他组合优化问题的近似算法一样，MaxSAT问题的近似算法在理论研究方面的价值远大于实际应用价值．2.2　MCS-based算法MCS-based算法是基于最小校正子集(minimal correction subset，MCS)和MaxSAT问题之间的关系而产生的．对于一个CNF公式F，若一个子句集合C满足F\C是可满足的，且对于∀c∈C，F\{C\c}是不可满足的，则C就是F的一个MCS集合．显然地，对于一个公式F，其MCS集合不是唯一的，每个MCS集合即对应了一个MaxSAT的可行解，但不一定是最优解，因此MCS-based算法是非完备算法．最简单的MCS检测算法是基于线性搜索的算法[23]，该算法维护一个可满足的子句集合S及MCS集合C，算法遍历公式F中的所有子句，对当前子句c，若S∪{c}是可满足的，则将c加入S中，否则加入C中．MCS-based算法同样须要频繁地调用SAT求解器．文献[90]提出了线性搜索的改进技术，例如，使初始化的集合S包含更多的子句，这样可以减少SAT求解器的调用次数．另外，文献[25]中的算法每次判断单个子句是否属于MCS集合，文献[90]还提出可以将公式F中未遍历的且被SAT求解器返回的赋值所满足的子句都加入S中，大大提高了算法的效率．FastDiag算法[26]提出一种基于模型的诊断策略用于MCS的检测，它采用了QuickXplain算法[91]所提出的分而治之的思想，递归地将剩余的子句一分为二进行检测，提高了搜索效率．文献[27]总结了几种检测MCS集合的先进技术，包括寻找不相交的不可满足核、骨干文字检测[28，92]及文献[90]提出的一次性添加多个子句至可满足子句集合S的方法．此外，SLS-MCS算法[93]提出将MCS检测与局部搜索相结合以解决MaxSAT问题，所提出的方法利用检测到的MCS集合来指导局部搜索过程，让局部搜索算法着重于调整MCS中出现的变量的赋值．MCS-based算法和SAT-based算法同样都须要频繁地调用SAT求解器，不同的是前者是非完备算法而后者是完备算法．相比较而言，在求解结构化的MaxSAT工业算例时，MCS-based算法的性能弱于SAT-based算法．2.3　局部搜索算法局部搜索算法是最具有代表性的MaxSAT非完备算法，当实例规模较大，或者全局信息很有限时，局部搜索算法通常是最有效的方法之一[94]．此外，局部搜索算法原理简单易懂，相较于SAT-based和MCS-based等须要调用SAT求解器的算法而言代码量极小且易于实现．局部搜索算法是一种通过在邻域空间中进行搜索以找到近似最优解，甚至最优解的算法．由于无法保证所找到的解是最优解，因此局部搜索算法属于非完备算法．MaxSAT问题的局部搜索算法的邻域空间通常被定义为：与当前的完全赋值只有一个变量的赋值不同的所有完全赋值的集合[29-34]．因此，MaxSAT最基本的局部搜索算法流程如下：步骤1：生成初始解；步骤2：根据启发式变量选择策略选择翻转(flip，即改变赋值)的变量，并翻转该变量；步骤3：判断是否达到停止条件，若达到则退出，并输出历史最优解，否则返回步骤2．实际上这也是SAT问题的局部搜索算法的基本流程，例如GSAT算法[95]和WalkSAT算法[96]．由于在局部搜索过程中，SAT问题和MaxSAT问题有着相似的目标，即都是希望最小化不满足的子句数量，因此SAT问题的局部搜索算法只要稍做改动就能用于解决MaxSAT问题，早期的部分研究直接将SAT的局部搜索算法转化为MaxSAT版本[97-98]．在SAT和MaxSAT的局部搜索算法中，对解的评价指标或评估函数通常都是该解对应的不被满足的子句数量或权重之和．并且，这些算法给每个变量都维护一个得分，变量v的得分就是翻转变量v所造成的不满足的子句权重之和的减少量．例如，对于一个纯MaxSAT问题，当前完全赋值α使k个子句不满足，若翻转α中变量v的赋值会导致不满足子句数量变成k'个，则变量v的得分就是k-k'．变量的得分是步骤2中选择下一翻转变量的重要依据，例如，GSAT算法[95]中每次都贪心的选择得分最高的变量，而WalkSAT算法[96]则引入了随机游走的策略，即以概率p随机选择一个不满足的子句中的变量进行翻转，以概率1-p遵循GSAT算法中的贪心规则选择变量，这两种算法的思想也都被用到MaxSAT的局部搜索算法中[97-98]．近年来，MaxSAT问题的局部搜索算法有了长足的发展，一些先进的算法[32，34]在解决(W)PMS问题的工业算例时也有与SAT-based算法相当的性能．这些局部搜索算法提出或使用了一些有效的、关键的技术，包括先进的变量选择启发式方法、先进的初始化方法、概率采样机制、子句动态权重机制和配置检测技术等．接下来将分别介绍MaxSAT局部搜索算法中的这些关键技术．2.3.1 变量选择启发式方法前文提到的GSAT算法[95]和WalkSAT算法[96]分别采用了基于贪心启发式和随机游走的变量选择方法．文献[99]提出一种使用自适应噪声机制来调整随机游走概率的方法．近年来一些优秀的局部搜索方法同样使用了随机游走方法来选择翻转变量，如CCLS算法[30]和CCEHC算法[31]．另一种较早的方法是基于模拟退火的启发式方法，这类方法最早也是出现在SAT的局部搜索算法中[100]，后来被用来求解MaxSAT问题[97-98]，模拟退火算法通过调整一个温度参数来控制变量翻转的概率．近年来的MaxSAT局部搜索算法采用了更复杂的变量选择策略．例如，Dist算法[29]给每个变量定义了硬得分和软得分，分别代表翻转变量所造成的不满足的硬子句和软子句权重之和的减少量，并在选择下一翻转变量时，设置硬得分的优先级高于软得分．还有一些算法采用了向前看的技术[101-102]扩大了邻域搜索范围[103-104]，使得算法每次迭代能够翻转不止一个变量，增强了算法的搜索能力．目前最好的一些MaxSAT局部搜索算法[29-34]的变量选择策略通常可分为未达到局部最优解的策略和达到局部最优解之后的策略．在未达到局部最优解时，即存在至少一个得分大于0的变量，这些算法会基于贪心的思想选择得分最高的变量；在达到局部最优解时，这些算法首先随机选择一个不满足的子句(硬子句优先)，再在所选择的子句中选择得分最高的变量，以此来逃离局部最优解．最近，FPS算法[103]通过向前看的技术提高了局部最优解的质量，并通过概率采样技术为算法提供了更多更好的逃离局部最优解的搜索方向，使算法能够找到更高质量的解．2.3.2 初始化方法最简单的初始化方法就是随机初始化，即为每个变量随机赋真值或假值，这种方法虽然简单，但也被广泛地应用在各种MaxSAT的局部搜索算法中[29-31，97-98]．文献[105]提出了一种基于单元传播的抽取构造算法，该算法通过UP技术确定所有变量的赋值，方法如下：当存在单元子句时(硬子句优先)，通过对其中的变量赋值令其满足，并将该变量的赋值传播到其他含有该变量对应文字的子句；当不存在单元子句时，随机选择一个未赋值变量，随机赋给它真值或假值，并传播至包含该变量对应文字的子句，重复上述过程直到不存在未赋值的变量，注意当同时有多个单元子句时，采取随机选择的方式打破平衡．通过实验表明，将该方法作为Dist算法[29]、CCLS算法[30]和CCEHC算法[31]的初始化方法能够显著提升这些局部搜索方法的性能[105]．文献[105]提出的初始化方法同样被用作著名的SATLike算法[32]的初始化方法．SATLike算法的改进版本[34]对该初始化方法做了如下改动：当同时存在多个单元子句时，算法贪心地选择能够满足更多软子句的单元子句进行传播，而不是通过随机的方式打破平衡．此外，还有一些局部搜索算法使用SAT求解器来生成初始的可行解[104]．例如，将硬子句集合输入到SAT求解器中得到能够满足所有硬子句的部分赋值，再将剩余未赋值的变量随机赋值以得到初始的可行解．使用SAT求解器虽然能够减少局部搜索算法无法得到可行解的情况，但这样会使得代码量急剧增加，失去了局部搜索算法简洁的优点．2.3.3 概率采样机制在MaxSAT的局部搜索算法中通常须要在一个候选集中挑选须要翻转的变量，例如在所有得分为正的变量中选出得分最高的变量．当问题规模很大时，遍历候选集将会非常耗时，概率采样机制能够有效地解决这个问题，提高算法的效率．文献[106]首次提出了一个概率采样技术(best from multiple selections，BMS)，其思想非常简单，即首先从候选集中采样t个元素，然后从这t个元素中选择最好的．BMS技术简单而有效，假设t=50，每次采样的元素是前10%的概率为0.9，那么所采样的t个元素中最好的元素是前10%的概率为1-0.9500.994 8，因此，BMS技术在很大程度上可以保证所选变量的质量，这项技术也被应用在目前最好的一些MaxSAT局部搜索算法中[29，31-32，34，103]．最近，FPS算法[103]结合了概率采样技术和向前看的技术，显著地提升了基线算法SATLike3.0[34]的性能．2.3.4 子句动态权重机制为子句添加动态权重是MaxSAT的局部搜索算法中的一项关键技术．这项技术在SAT的局部搜索算法中广泛的应用[100，107-110]，其核心思想是给那些难以被满足的子句以更高的权重，使算法在后续的搜索过程中更倾向于满足这些难以被满足的子句．注意在使用了加权机制的局部搜索算法中，变量的得分是与子句的动态权重而非MaxSAT实例中的原始权重相关．早期MaxSAT局部搜索算法中的加权机制都是直接将SAT中的加权机制迁移过来[98]，但这样的机制不适用于具有硬软子句之分的(W)PMS问题．直至2014年，Dist算法[29]首次提出了仅对硬子句加权的机制，大致如下：当算法每次陷入局部最优时，即不存在得分大于0的变量，将所有不满足的硬子句的权重加1，这一机制提高了MaxSAT局部搜索算法的性能．CCEHC算法[31]同样使用了该硬子句加权机制．SATLike算法[32]首次提出了对硬子句和软子句都加权的方法，其加权机制大致如下：硬子句起始权重为1，软子句起始权重为其原始权重，每当算法陷入局部最优时，将所有不满足软子句的权重加1，不满足硬子句的权重加h_inc(h_inc通常是大于1的整数)，同时为每个软子句设置了一个权重上限以避免因为软子句权重过高导致算法无法找到可行解．该加权机制有如下优点：第一，它将硬得分与软得分统一，从而简化了算法的变量选择机制；第二，它使软子句在搜索开始阶段具有不低于硬子句的优先级，这样能够使算法找到更好的解；第三，它使硬子句在搜索过程中的优先级逐渐超过软子句，避免算法无法找到可行解．SATLike算法[32]优秀的加权机制使其具有远超Dist算法[29]和CCEHC算法[31]的性能．2.3.5 配置检测技术配置检测技术(configuration checking，CC)是一项用于避免循环重复的搜索的技术．文献[111]首次提出了配置检测技术，用于解决最小顶点覆盖问题．后来配置检测技术被广泛应用到了SAT[112-113]和MaxSAT算法[30-32，34，114]中．在介绍MaxSAT问题的配置检测技术之前，首先要介绍变量的邻居概念，变量的邻居是与该变量对应的正、负文字出现在同一子句中的其他文字对应的所有变量的集合．MaxSAT问题的配置检测原理如下：若某个变量的所有邻居的赋值在该变量上一次翻转之后未发生改变，则该变量不应被翻转，以减少无意义的操作．配置检测技术被应用到一些著名的MaxSAT局部搜索算法中[30，32，34]．CCEHC算法[31]提出了只考虑硬子句中的邻居的配置检测方法，提升了其基线算法CCLS[30]的性能．3 讨论与展望首先对求解MaxSAT问题的各种算法的优缺点进行总结和分析，然后对解决MaxSAT问题未来可能的研究方向进行讨论．表1总结了求解MaxSAT问题的各种算法及优缺点．10.13245/j.hust.220214.T001表1求解MaxSAT的各种算法及优缺点MaxSAT算法代表性文献优点缺点完备算法分支定界算法[10-15，38，40，41，45，49，56]解具有最优性保证，在解决随机生成和人工构造的实例上有较好的性能求解大规模问题很耗时，在解决复杂工业算例时性能较差SAT-based算法[4，16-20，65-69，73-80]综合性能强大，在解决结构化困难的工业算例时有很好的效果对SAT求解器有很强的依赖，代码繁杂难以实现非完备算法近似算法[21-23，82-87]解具有近似比保证，有较大的理论研究价值实际应用价值较弱，难以扩展至(W)PMS问题MCS-based算法[25-28，90，93]作为非完备算法能够快速逼近最优解，且能够推动MCS检测与MaxSAT求解同步发展同样依赖SAT求解器，代码繁杂，且效果不如SAT-based算法局部搜索算法[29-34，97-99，103-104，114]算法简洁易懂，代码量极小且易于实现和扩展，在随机和人工构造算例上表现很好在工业算例上与SAT-based算法仍有差距，且部分实例不依赖SAT求解器难以得到可行解多样化的算法使MaxSAT问题的求解有了长足的发展，但仍然面临着一些挑战，接下来将讨论一些未来可能的研究方向．a. 更紧的下界下界的计算很大程度上决定着分支定界算法的性能，如果希望分支定界算法能够在工业算例上有良好的表现，那么提出更紧的下界计算方法具有重要意义．b. 子句学习的应用冲突驱动子句学习(conflict-driven clause learning，CDCL)技术在SAT求解器中取得了非常好的成就，将CDCL技术与分支定界算法相结合[42]或利用CDCL技术来引导各种算法的搜索过程是值得研究的方向．c. 针对WMS的近似算法现有的MaxSAT问题的近似算法几乎都是针对纯MaxSAT问题或Max-k-SAT问题，提出针对加权MaxSAT问题的近似算法能够极大的扩展近似算法的应用范围．d. 局部搜索算法的初始化现有的局部搜索算法获得初始解的方法较为单一，且在不依赖于SAT求解器的情况下，部分算例甚至难以获得可行解，提出合理的初始化方法以解决这一问题具有重要的意义．e. 局部搜索算法的搜索过程现有的大部分局部搜索算法的变量选择策略，每次迭代翻转一个变量的机制都比较简单，在解决结构复杂的工业算例时难以获得高质量的结果，这样的搜索过程还有很大的改进空间．4 结语本综述总结了近年来最大可满足性(MaxSAT)问题的各类求解算法，并根据解是否具有最优性保证将其分为完备算法和非完备算法两类．其中完备算法包括分支定界算法和SAT-based算法，非完备算法包括近似算法、MCS-based算法和局部搜索算法．本研究还总结和对比了各种算法的优缺点，并对解决MaxSAT问题未来可能面临的挑战及可能的研究方向做了讨论与展望．