求解加权偏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中限制动态权重增量上下限,以及使动态权重增量根据变元得分自适应调整的机制的有效性.

一种求解Max-SAT问题的快速模拟退火算法

最大可满足性问题(Max-SAT)是经典的NP难问题,目标是寻找一组变元赋值使得满足子句个数最多。近年来,随着算例规模在实际应用中的逐渐增大,传统的启发式算法已不再适用。传统模拟退火算法在求解Max-SAT问题时会出现收敛速度慢、局部搜索能力弱,以及无效的盲目扰动等弊端,为此提出一种改进的快速模拟退火算法,针对初始赋值的随机性和盲目性,采用变元权值计算初始解,结合基于概率的随机扰动和选择扰动两种方式,并在Metropolis接受准则中添加记忆功能,用于搜索当前局部最优解,引入高低温两种降温模式,较大程度地提高算法的全局搜索能力,进而加快算法的收敛速度,有效减少求解时间。最后,在公开数据集和随机生成的数据集上进行仿真实验,结果表明,所提算法在求解Max-3-SAT问题上优于传统启发式算法。

利用命题逻辑最大可满足性的冗余通孔最优插入方法

在纳米尺度的集成电路设计中,冗余通孔插入是减轻通孔失效造成良率降低问题的常用技术.文中将最优冗余通孔插入问题规约到命题逻辑最大逻辑可满足性(maximum satisfiability,Max SAT)问题,并利用完备求解器求取最优解.Max SAT问题是一个NP困难问题,采用2种方法来降低求解难度;一是预选取方法,将提前确定的不与其他通孔产生冲突的冗余通孔作为部分解来降低问题的规模;二是分治法,根据连通分量将原问题划分成多个子问题分别求解,降低求解的复杂度.同时,从理论上证明这2种方法能够保证解的最优性.在2019年国际物理设计研讨会(ISPD)举办的详细布线比赛基准测试集上进行实验的结果表明,所提出的插入方法带来的时间开销不到详细布线时间的5%,算法的最优性保证了最大化解决插入冲突后的插入率,在所有可插入通孔中,冗余通孔的插入率为67%~87%.

MAX-SAT问题的分子信标解决方法

文章采用分子信标编码方法,在解决SAT问题的同时解决MAX-SAT问题。这种方法可以用在最优化计算领域。

一种改进的警示传播算法求解Max-SAT问题

Max-SAT问题是SAT问题的优化版本,目标是在给定的子句集中找到一组变元赋值,使得满足子句数最多,该问题是典型的NP-hard问题。随着大数据和人工智能的深度发展,过去原有的算法已不再适用,设计新的求解算法或对已有的求解算法进行优化是目前研究的热点。针对警示传播算法求解随机Max-3-SAT问题的局限性,提出了一种基于变元权值计算的警示传播算法,结合随机游走算法,给出一种新型算法WWP+WalkSAT,通过改进求解的局限性,更好地得到一组有效的初始解,从而提高算法的局部搜索能力。利用2016年Max-SAT国际竞赛部分基准实例,将WWP+WalkSAT算法与八种局部搜索算法进行精度方面的对比实验。实验结果表明,WWP+WalkSAT算法有较好的性能。

基于部分最大可满足性问题的动态系统中最小故障检测隔离集求解方法

选择一组能够检测并隔离所有故障的故障检测隔离集(FDIS)是动态系统基于模型故障检测与隔离(FDI)的重要步骤,该步骤通常要求FDIS的基数最小,即求解最小故障检测隔离集(MFDIS),MFDIS的求解时间随着问题规模增大呈指数级增长。BILP(Binary integer linear programming)完备方法是现行动态系统中通用和最高效的MFDIS求解方法,但该方法的求解效率有待提高。本文首次提出了基于部分最大可满足性问题(PMS)的MFDIS求解方法。提出极小超定方程集(MSO)的概念,将部分MSO集合用MSO等价集表示,以缩减问题规模。将MFDIS求解问题转化为PMS问题,进而提高求解效率。实验结果表明,本文方法将问题规模平均约简至原来的8.22%;与BILP方法相比,本文方法的求解效率提高了4.18~9.5倍。

基于搜索信息反馈策略的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算法与其它局部搜索类算法有很强的互补性,有提升其它求解器求解效果的能力.

基于模型诊断的一种新编码方法

基于模型诊断(model-based diagnosis,MBD)是人工智能诊断领域中著名的诊断求解方法之一,旨在识别诊断问题的根本原因.由于求解诊断解在计算上具有挑战性,一些MBD算法提出通过修改模型的编码来提高诊断效率,如面向统治者的编码(dominator-oriented encoding,DOE)方法.面向观察的编码(observation-oriented encoding,OOE)方法使用2种方法对MBD模型进行约简.首先,利用系统观测和统治组件输出的一些过滤边来约简系统描述和观测.其次,通过查找基于观测的过滤节点来过滤更多的组件,进而有效约简组件的编码规模.此外,在ISCAS85和ITC99基准测试用例上的实验结果表明,与目前最新的MBD编码方法DOE和传统的基础编码(basic encoding,BE)相比,上述2种约简方法有效减少了MBD实例的编码子句数量比,降低MaxSAT求解器求解诊断的难度,进而能在更短的时间内返回一个诊断解.

面向最大串扰噪声的测试生成方法

随着特征尺寸进入纳米尺度,相邻连线之间的电容耦合对电路的影响越来越大,并可能使得电路在运行时失效.为此提出一种面向受害线上最大串扰噪声的测试生成方法,该方法基于多串扰脉冲故障模型,能够有效地模型化故障并生成合适的向量.为了能够激活尽可能多的侵略线以造成受害线上的最大脉冲噪声,首先将测试生成问题转化为一个加权的最大可满足问题,再使用解题器求解,以得到测试向量;此外,将子通路约束加入到可满足问题的描述之中,以保证所有被激活的侵略线能够同时跳变.针对ISCAS89电路的实验结果显示,文中方法适用于较大规模电路的串扰噪声测试,并且具有可接受的运行时间.

基于优化冲突集提高下界的MAXSAT完备算法

最大可满足性问题(MAXSAT)是经典的NP完全问题SAT的一个扩展问题.基于分支限界设计MAXSAT完备算法时,如何有效地提高下界是设计高效算法的关键和难点.基于优先找到规模小、结构简单的冲突集的思想,在Maxsatz算法的基础上,提出了改进的算法Maxsatz2013.通过使用推理规则优先、改变单子句的传播顺序、进一步失败文字检测这3个优化策略,增加了检测到的冲突集数,从而有效地提高了下界.测试了MAXSAT 4个类别共800多个算例.实验结果表明,这3个优化冲突集的策略是可行且有效的,所提出的算法在每一类算例上均明显地提高了计算效率.

基于环型扩展推理规则的MaxSAT完备算法

最大可满足性问题(MaxSAT)是可满足性问题的优化求解问题,是经典的NP难问题.基于分支限界的MaxSAT完备算法采用推理规则、失败文字检测等方法缩短算法计算时间.推理规则产生的新子句可以构成更多的冲突集,从而有效地提高了二叉树的剪枝率和算法性能.在已有的工作基础上,针对环型结构冲突集进行分析,找到与步长大于2的环型结构冲突集等价的新子句集,并利用整数规划证明了新子句集和冲突集的MaxSAT等价性.该环型扩展推理规则产生的新3元子句亦可以提高冲突集数,提高下界.在Maxsatz2013算法的基础上实现了新算法Maxsatce.测试了MaxSAT竞赛4个类别算例集.实验结果表明环型扩展推理规则对子句长度大于等于3的MaxSAT问题,可以提高二叉树分支点的下界值,最终有效地缩减算例运算时间.

基于扩展失败文字检测的MaxSAT完备算法

为提高MaxSAT完备算法剪枝率和运算效率,分析失败文字检测寻找冲突集的过程,提出扩展失败文字检测方法。通过延长失败文字搜索冲突的路径,形成搜索1步、2步和任意步的递进失败文字检测方式,实现改进的MaxsatzEF算法。实验测试了MaxSAT国际竞赛4个类别的500多个算例,实验结果表明,递进失败文字检测方法找到了更多独立冲突集,可有效提高算法的下界,大幅缩短复杂算例的运行时间。

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

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

基于Partial MAX-SAT求解法的RBAC授权查询方法

为保证系统的安全性并体现授权的有效性,结合部分最大可满足性问题(Partial MAX-SAT)的研究,提出一种基于Partial MAX-SAT求解法的授权查询方法。使用转换规则将静态授权逻辑和动态互斥角色约束转化为严格子句,采用子句更新算法将满足不同匹配的请求权限转化为松弛子句,并利用子句编码及递归算法寻求真值指派,以满足所有严格子句和尽可能多的松弛子句。实验结果表明,该方法搜索的角色组合能够保证系统的安全性,并满足最小权限分配要求,且最大、精确匹配请求的查询效率优于MAX-SAT求解法。

基于RBAC的角色挖掘及授权查询方法的研究

针对现有角色挖掘结果存在冗余,以及授权管理在安全性等方面存在的问题,将角色挖掘与授权查询分别转化为布尔矩阵分解问题及部分最大可满足性问题,给出一种基于RBAC的角色挖掘及授权查询方法。应用实例结果表明:该方法挖掘的角色集更为简洁,且具有可解释性;查询搜索的角色组合能够严格保证系统的安全性,且满足授权的有效性要求。

一种结合结构特征求解诊断问题的PMS方法

部分最大可满足性问题(partial maximum satisfiability problem, PMS)是最大可满足性问题(maximum satisfiability problem, MaxSAT)的泛化问题,在很多领域中得到广泛应用.目前,在工业诊断实例方面PMS求解仍有待改进,在对基于随机搜索的PMS算法深入研究基础上,本文首次提出一种结合结构特征的随机搜索方法 (structure characteristics partial MaxSAT, SCPMS).首先,依据单元传播规则结合问题结构特征逐步将PMS问题中硬单元子句分成两部分,从而构造出因缺乏部分硬单元子句使得问题可满足的子问题;提出结合结构特征的随机搜索指导策略,对新的子问题再次利用单元传播找出原问题中的硬单元子句中硬阻塞变量,再结合子句特征翻转相应软阻塞变量,从而提高随机搜索的求解效率.实验结果表明,提出的SCPMS与最新的两个算法DeciDist和DistUp相比,在基于模型诊断问题(model-based diagnosis, MBD)的工业实例上, SCPMS求得的不满足软子句数有较大程度的减少.