基于演绎长度的学习子句删除策略

学习子句删除策略是CDCL-SAT求解器中的一个重要内容,可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的,极大地影响求解效率。基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程,基于此,提出一种基于演绎长度的学习子句评估方法,并与现有的基于文字块距离的评估方法结合,根据排序子句的基准不同,形成两种不同的结合算法。采用国际SAT竞赛的基准实例,与目前主流的求解器进行了实验对比分析。结果表明,所提的结合算法能更好地评估学习子句的有用性,较基于文字块距离策略的求解个数提高了4.1%,说明所提策略具有一定的优势。

基于学习子句删除策略的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%。

基于学习子句长度和LBD的删除策略

学习子句的删除在求解器的构成中是非常重要的。因为学习子句删除策略的"优劣"不仅影响BCP的效率,还影响内存的占用问题,为避免出现这些问题,很多学者做了大量的工作,提出了很多良好的学习子句删除策略。然而当前的学习子句删除策略都有一个缺点:删除学习子句时有可能会删除在后续搜索过程中有很大作用的子句,因为不能确保每次删除的都是没有"价值"的子句。在充分考虑学习子句的长度和变量的决策层的基础上,本文提出基于学习子句长度和LBD的删除策略——LLBD策略,并形成算法,然后用该策略替换Glucose求解器中的删除策略,最后通过实验表明LLBD策略能够求解出更多的实例,求解器的效率也有所提高,表明本文策略有一定的优势。

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

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