基于动态奖惩的CDCL SAT求解器分支启发式算法

分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。     

基于学习子句删除策略的SAT求解器分支策略

对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突.但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响.针对此问题,提出了 一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度.基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD.以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较.实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了 15.5％.在2019年的例子测试中,Maple-DL_VDALCD 比 MapleLCMDistChronoBT-DL-v2.1 多求出 17个例子,增加了 7.6％.     

基于Expectimax搜索与Double DQN的非完备信息博弈算法

麻将作为典型的非完备信息博弈游戏主要通过传统Expectimax搜索算法实现,其剪枝策略与估值函数基于人工先验知识设计,存在假设不合理等问题。提出一种结合Expectimax搜索与Double DQN强化学习算法的非完备信息博弈算法。在Expectimax搜索树扩展过程中,采用Double DQN输出的估值设计估值函数并在限定搜索层数内获得分支估值,同时设计剪枝策略对打牌动作进行排序与部分扩展实现搜索树剪枝。在Double DQN模型训练过程中,将麻将信息编码为特征数据输入神经网络获得估值,使用Expectimax搜索算法得到最优动作以改进探索策略。实验结果表明,与Expectimax搜索算法、Double DQN算法等监督学习算法相比,该算法在麻将游戏上胜率与得分更高,具有更优异的博弈性能。     

基于趋势强度的SAT问题学习子句评估算法

针对命题逻辑公式求解过程中难以有效评估学习子句是否有利于后续搜索的问题,提出了一种基于学习子句趋势强度的评估算法。该算法首先通过分析学习子句在生存期内参与冲突分析的时间分布特征,将随机、离散的时间分布转换为连续的累积趋势强度;然后在删除周期达到时,通过设定趋势强度阈值删除在后续搜索过程中“不大可能”被使用的子句,保留“可能”被使用的子句;最后采用2015年、2016年SAT问题国际竞赛实例,将该算法与经典的活跃度评估算法和文字块距离(LBD)评估算法进行对比。实验结果表明,趋势强度评估算法在效率上明显优于活跃度评估算法,且求解的实例更多,同时与LBD算法基本持平。     

半结构化数据相似搜索的索引技术研究

为了在海量、高维、动态的半结构化数据集上进行有效的相似搜索，该文提出一种采用聚类技术进行索引构建与更新的多路平衡树－－CSS－树以及基于CSS－树的相似搜索与动态更新的算法。CSS－树借鉴SS^ -树基于聚类进行节点组织与分裂的基本思想，避免了根据坐标准进行分裂时所要求的维不相关性，同时在节点组织、分裂算法和搜索算法等方面进行了改进，提出了新的搜索剪枝策略，实验表明，该结构及算法对海量半结构化数据相似搜索和效率明显优于传统算法。     

基于加强概率控制策略的SAT局部搜索算法

局部搜索算法是目前求解SAT问题比较有效的方法,而Sattime算法是在SAT国际大赛中获得大奖的一种典型局部搜索算法。在Sattime算法的求解过程中,记录变元翻转事件流数据库,通过数据分析与模式挖掘,发现Sattime算法的局部搜索行为中会出现相邻搜索步选择同一个变元的现象,即所谓的回环现象,从而降低了求解效率。为解决此问题,提出两种概率控制策略：加强子句选择策略和加强变元选择策略,并将这两种策略应用到Sattime算法中,形成新的局部搜索算法Sattime-P。实验结果表明,与Sattime算法相比,改进后的Sattime-P算法求解效率有显著的提升。该方法也对其他局部搜索算法的改进具有参考价值。     

基于动态惩罚因子的改进蚱蜢算法求解经济负荷调度和经济排放联合调度问题

电力生产装置运行中各种燃料的成本逐步增加,需要最小化成本函数以求解此类复杂经济负荷调度问题.鉴于此,提出一种基于动态惩罚因子的改进蚱蜢算法求解经济负荷调度(economic load dispatch, ELD)问题和经济排放联合调度(combined economic emission dispatch, CEED)问题.为了提高蚱蜢算法(grasshopper optimization algorithm, GOA)性能,提出一种改进的混合蚱蜢算法(hybrid grasshopper optimization algorithm, HGOA),将重力搜索算子和鸽群搜索算子-地标算子加入GOA中,增强算法的搜索能力,平衡算法的勘探和开发.同时,为了更好地解决ELD和CEED问题中的约束问题,提出6个惩罚函数,包括2个V型函数、反正切函数、反正弦函数、线性函数和二次函数,并使用动态惩罚策略代替传统的固定值惩罚策略.选取3个ELD问题案例和4个CEED问题案例验证所提出方法的有效性,实验结果表明, HGOA相较于其他元启发式算法在求解质量上表现更好,且动态惩罚策略比固定值惩罚策略效果更...     

双人博弈问题中的蒙特卡洛树搜索算法的改进

蒙特卡洛树搜索(MCTS)是一种针对决策类博弈游戏,运用蒙特卡洛模拟方法进行评估博弈策略的启发式搜索算法。但是,在面对计算机围棋这种复杂的决策过程时,简单的蒙特卡洛树搜索过程往往由于计算量大,收敛速度非常慢。 由于双人博弈游戏中的蒙特卡洛树搜索不能收敛于双人博弈的最佳决策策略,因此提出蒙特卡洛树搜索结合极大极小值算法的改进算法,使得搜索结果不会因为蒙特卡洛方法的随机性而失真。为了进一步提高复杂双人博弈游戏中搜索算法的计算效率,还结合了几种常见的剪枝策略。实验结果说明,所提算法显著改进了蒙特卡洛树搜索的准确性和效率。     

基于频次的SAT问题学习子句混合评估算法

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器（GLUCOSE 4.1并行版本）为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。     

基于参与冲突分析次数的动态学习子句评估策略

针对现有学习子句评估策略的单一性,提出一种基于学习子句参与冲突分析次数的评估策略,并将该策略分别与经典的文字块距离评估策略和活跃值评估策略结合,形成两个动态学习子句评估策略。基于2018年SAT国际竞赛部分基准实例,将动态评估策略与原评估策略进行参数适应性对比实验,并通过2018和2017年的基准实例进行评估。结果表明动态评估策略能更好地评估学习子句的质量,由此生成的求解器在求解数量和速度方面表现出较好的求解性能。     

基于变量混合特征的分支启发式策略

先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略,它因其稳健性而被广泛使用,但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题,本文提出了一种基于变量混合特征的分支启发式算法,目的是充分地利用参与冲突分析的变量所携带的不同信息特征来区分变量,来进一步指导变量活性增长.并将所提出的分支策略算法嵌入到Glucose4.1中形成求解器Glucose4.1+MFBS,通过对比测试,实验结果表明改进的分支算法比原本的VSIDS策略,具有一定的优势,求解明显个数增加.     

基于顶点冲突学习的最大公共子图算法

针对最大公共子图（MCS）的传统分支策略依赖于图的静态属性,缺少学习历史搜索信息的问题,提出了基于顶点冲突学习的分支策略。首先,把上界的减少值作为分支点完成匹配动作的奖励;其次,由于当最优解被更新时,得到的最优解是分支点不断推理产生的结果,因此给予在完整的搜索路径上的分支点适当的奖励,从而强化这些顶点对搜索的积极作用;最后,设计了匹配动作的价值函数,并选择具有最大累计奖励的顶点作为新的分支点。在McSplit算法基础上,提出了糅合新分支策略的McSplitRLR算法。实验结果表明,除去均可以被所有对比算法在10 s之内解决的简单算例,在相同机器和求解限制时间条件下,相较当前先进的算法McSplit、McSplitSBS,McSplitRLR分别多解决了109、33个困难算例,求解率分别提高了5.6%、1.6%。     

基于加权平均值的一种分支启发式方法

在可满足性(Satisfiability,SAT)问题算法中提出有效的分支策略可以提高求解器的效率,文中主要从冲突分析的角度出发,依据变量是否发生冲突和冲突的次数,提出 一种基于加权平均值的分支启发式方法。该方法首先采用一组序列来记录变量是否参与冲突;其次赋予一个加权平均函数,依据变量的序列和决策层求出函数值;最后选择具有最大的函数值变量赋值,执行实例分析比较。由于该方法是对控制编码方法的改进,因此在进行例子分析时,采用了比较法和分析法,同时分析比较了所提方法、 SUM(Sum in experiment)策略和 ACIDS(Average Conflict-index Decision Score)策略。对SATLIB(SAT Little Information Bank)中的实例进行分析,结果表明所提方法能够实现更多子句被满足或最新冲突子句优先满足。     

融合递减策略与Fuch混沌机制的改进YSGA算法

为增强绯鲵鲣算法搜索的覆盖性及寻优的精准性以优化全局探索能力和局部开采能力,提出一种融合步长因子递减策略与混沌局部增强机制的改进绯鲵鲣优化算法(IYSGA)。首先,该改进算法在标准YSGA算法基础上,设计了一种动态的步长因子递变模式以实现绯鲵鲣算法高效全面的搜索,此策略有利于提高算法的搜索效率并扩大寻优范围;其次,混沌搜索机制则是借鉴Fuch映射理论优越的混沌特性与较好的局部收敛性能而构造的一种当前最优解的局部再开采方式,以完成对YSGA算法的局部搜索性能的改善。该耦合方法对YSGA的改进,有利于实现IYSGA算法全局探索与局部搜索能力间的多轮动态迭代平衡。最后,通过数值实验验证了IYSGA算法优越的并行迭代寻优性能与稳健性。     

面向多智能体博弈的并行蒙特卡洛树搜索算法研究

蒙特卡洛树搜索算法是一种常用的强化学习算法,博弈过程中动态空间的指数级增长是制约该算法学习效率的因素。基于并行方法对蒙特卡洛树搜索算法进行优化,提出基于胜率估值传递的并行蒙特卡洛树搜索算法。改进后的并行博弈搜索策略框架包含一个主进程和多个子进程,其中子进程用于探索,主进程根据子进程传递的胜率估值数据进行决策。结合多智能体博弈平台Pommerman进行实验验证,与传统的蒙特卡罗树搜索算法相比,并行蒙特卡罗树搜索算法有效提高了资源利用率、博弈胜率及决策效率。      

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

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

最坏情况下Min-2SAT问题的上界

最坏情况下MaxSAT问题上界的研究已成为一个热门的研究领域.与MaxSAT问题相对的是MinSAT问题,在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此对MinSAT问题进行研究.针对Min-2SAT问题提出算法MinSATAlg,该算法首先利用化简算法Simplify对公式进行化简,然后通过分支树的方法对不同情况的子句进行分支.从子句数目的角度分析算法的时间复杂度并证明Min-2SAT问题可在O(1.134 3m)时间内求解,对于每个变量至多出现在3个2-子句中的情况,得到最坏情况下的上界为O(1.122 5n),其中n为变量的数目.     

基于回跳层数的SAT求解器学习子句删除策略

目前学习子句删除策略广泛采用的是基于LBD的评估方式,LBD评估方式在每次执行删除时都会删除前一半LBD值大的学习子句,这种方式对LBD值大的学习子句的删除过于激进。针对此问题,提出了一种利用冲突回跳层数（back-jump levels）的评估方式来保留LBD值较大的相关学习子句。以CDCL（conflict driven clause learning）完备算法为框架,在子句删除环节形成了BJL删除算法。通过测试2017年SAT国际竞赛例,对新改进的版本与原版求解器进行了对比实验。实验表明,所提策略可显著提高求解器的求解性能和求解效率。