基于动态奖惩的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％.     

与并行条件表达式的生成

逻辑程序的与并行是子句体中文字的并行执行。如果若干文字共享某个变量,获得与并行的一种途径是:仅启动其中一个文字执行,该文字称为该变量的产生器,其它的文字(称为该变量的消耗器)处于等待状态,这称为排序。排序方法大致为完全动态排序、完全静态排序和动静结合排序。本文给出无用户启发信息时的静态排序算法,采用     

智能空间中的冲突问题研究

智能空间和回答集程序的整合解决了智能空间中固定优先关系下的资源冲突问题。然而,智能空间处在一个上下文敏感的、动态的环境中,信息更新以及环境变化都会导致资源分配的顺序重新发生变化,从而产生新的冲突问题。针对该问题,基于回答集程序提出一种动态优先的方法。首先,引入缺省规则并利用缺省决策理论动态决策智能空间中的优先关系;然后,使用回答集程序表达空间中的动态优先关系;最后,求解回答集程序得到冲突问题的解。实验结果表明,该方法可以动态决策空间中的优先关系,有效解决空间中的冲突问题,对空间中的资源实现合理分配。     

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

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

一种基于图分割的动态回溯算法

动态回溯算法在进行回溯时保留所有已赋值变量的值,从而可能与后面赋值的变量产生冲突,其在解决不具有明显子问题结构的约束满足问题时效率较低。为此,将图分割技术应用于动态回溯,通过图分割将变量分为若干集合,当发生回溯时,不保留全部变量的值,舍弃那些与引起冲突的变量在同一集合变量中的值。实验结果表明,该算法在求解没有明显子问题结构的约束满足问题时具有较高的效率。     

可满足性求解器中一种可观无关性利用方法

为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.     

基于变量决策层的启发式变量选择策略

启发式分支策略是SAT求解器中不可或缺的一部分，直接影响求解器的效率。早期的启发式分支决策需要遍历整个子句数据库，效率比较低。随着独立变量状态衰减和（Variable State Independent Decaying Sum, VSIDS）分支策略的出现，SAT求解器的效率有所提高，但VSIDS策略以及它的延伸策略中变量的增量都只是与变量的冲突次数有关，没有考虑变量的决策层在分支策略中的影响。因此当发生冲突时，如果与冲突有关的变量的得分相同而决策层不同时，对于变量的选择就具有随机性。基于此，本文在阐述变量的决策层的重要性之后在VSIDS策略的基础上，提出一种基于变量决策层的启发式变量选择策略--HSVDL策略。然后通过实例显示HSVDL策略在变量决策阶段选择决策层低的变量的可能性比选择决策层高的变量的可能性要大，而且得分比较小，减少了内存的占用。最后通过实验表明HSVDL策略能够求解出更多的实例，求解器的效率也有所提高，说明该策略有一定的优势。     

基于决策变量关系的动态多目标优化算法

动态多目标优化问题(DMOPs)需要进化算法跟踪不断变化的Pareto最优前沿,从而在检测到环境变化时能够及时有效地做出响应.为了解决上述问题,提出一种基于决策变量关系的动态多目标优化算法.首先,通过决策变量对收敛性和多样性贡献大小的检测机制将决策变量分为收敛性相关决策变量(CV)和多样性相关决策变量(DV),对不同类型决策变量采用不同的优化策略;其次,提出一种局部搜索多样性维护机制,使个体在Pareto前沿分布更加均匀;最后,对两部分产生的组合个体进行非支配排序构成新环境下的种群.为了验证DVR的性能,将DVR与3种动态多目标优化算法在15个基准测试问题上进行比较,实验结果表明, DVR算法相较于其他3种算法表现出更优的收敛性和多样性.     

基于回答集程序的冲突问题研究

Smart M3是一个实现智能空间的交互平台,它允许软件实体和设备共享语义信息.在Smart M3中使用ASP可以处理固定偏好关系下的资源分配和冲突问题.然而在现实生活中,信息更新却会改变原有的资源分配顺序,从而引起新的冲突.为了处理这个问题,提出使用动态优先关系的方法解决该问题.将动态优先关系使用加权逻辑程序表示,然后求解程序得到回答集,该回答集就是冲突问题的解决方案.最后,以一个实例说明了该方法的应用.