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

最大可满足性问题(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还为子句动态权重的增量设置了上下限,保证了子句加权的稳定性.为了评估所提出的Hist-Weighting子句加权技术的性能,将其应用于三种最先进的WPMS局部搜索算法,即BandMaxSAT、SATLike3.0和CCEHC.在近五届 MaxSAT国际算法竞赛 MaxSAT Evaluation非完备组的所有WPMS算例上的实验结果表明,应用Hist-Weighting技术的改进算法相比于原算法在获胜算例数上能够提升约10%至60%,体现了所提出的Hist-Weighting子句加权技术在求解WPMS问题时的有效性.此外,通过将应用了 Hist-Weighting的改进局部搜索算法与其变体算法对比以进行消融实验,表明了 Hist-Weighting中限制动态权重增量上下限,以及使动态权重增量根据变元得分自适应调整的机制的有效性.

基于搜索信息反馈策略的MaxSAT非完备求解算法

MaxSAT问题是SAT可满足性问题的优化形式,具有NP难度.本文分析了传统的MaxSAT局部搜索求解器对工业算例求解存在的局限性,并基于此分析提出了新的初始解构造算法ASIF.ASIF是一个基于树形赋值的初始解构造算法,其中包含了一个全局信息反馈策略.该算法选取并定义了构造过程中有意义的统计量,使用这些量设计了一个全局搜索信息更新反馈机制,对初始解构造过程中的经验进行积累并为后续解的构造提供指导信息,再根据后续解的构造情况对全局经验进行反馈和更新,从而有效利用了解构造过程中的经验和信息.进一步地,将ASIF作为初始解构造算法,结合IPBMR算法中的路径截断(PB)策略,提出了新的算法PB-ASIF.实验设计与比较共分为三个阶段.第一阶段,将ASIF在300秒内首次找到的可行解与IPBMR求解300秒的结果进行对比.ASIF初始可行解更优的数量是IPBMR在300秒内求解的可行解更优数量的两倍多,其中非加权偏类算例更优解数量上前者更是后者的3.68倍.该阶段的实验结果表明,ASIF算法能快速构造优质的初始可行解.第二阶段,将PB-ASIF与IPBMR进行对比实验,在300秒求解时间内,PB-ASIF求得更优解的数量总体上是IPBMR的2.38倍,在非加权偏类算例更优解数量上前者更是后者的3.85倍.该阶段的实验结果表明,PB-ASIF算法求解工业算例的能力明显超过了IPBMR算法,有效改进了使用PB策略求解工业算例的效果.第三阶段,将PB-ASIF与其它优秀求解器进行联合求解,包括CCEHC求解器和SATLike3.0求解器.该阶段的实验结果表明,PB-ASIF算法与其它局部搜索类算法有很强的互补性,有提升其它求解器求解效果的能力.

基于回溯法的全覆盖路径规划算法

随着扫地机器人的快速发展,作为其核心技术的全覆盖路径规划技术也变得日益重要。目前已经提出的许多算法,如人工势场法、模板法、单元分解法等,都存在一些问题,如覆盖率低、重复率高、运行效率低等等。针对目前已有算法存在的问题,提出了一种基于回溯法的全覆盖路径规划算法。首先利用West-MoveFirst算法实现局部区域覆盖,然后为了解决扫地机器人局部区域覆盖过程中存在遗漏区域未覆盖的问题,建立了完善的回溯机制,并采用改进的A*算法规划出一条从死点到回溯点的光滑无障碍路径。通过与BA*算法进行仿真对比分析,表明了该算法具有更高的运行效率和更低的重叠率。

最大可满足性问题的算法研究综述

最大可满足性问题(maximum satisfiability,MaxSAT)是一个著名的、具有NP难度的组合优化问题.本研究总结了近年来求解最大可满足性问题的各类算法.首先,给出了最大可满足性问题的定义;然后,基于完备算法和非完备算法两个类型,对求解MaxSAT的各类算法进行了综述.其中完备算法包括分支定界算法和迭代调用可满足性问题求解器的算法,非完备算法包括近似算法、基于最小校正子集的算法和局部搜索算法;最后,分析和对比了各类求解算法的优劣,并对最大可满足性问题求解所面临的挑战及可能的研究方向进行了讨论和展望.