一种基于识别重复路径的动态决策策略

作者：常文静; 徐扬

来源：计算机学报, 2019, 42(10): 2309-2322.

• 可满足问题
• 冲突驱动学习子句
• 重启
• 分支决策策略
• 重复赋值序列

在现有基于冲突学习子句的求解器中,重启和变量相位存储技术的频繁应用,导致重启之后产生大量重复变量赋值序列,在求解过程中对变量重复赋值会浪费求解资源.本文提出一种基于识别重复路径的动态决策策略.首先,检测搜索过程中产生的重复赋值变量序列,算法中参数依据子句数与变元数的比率而动态变化;其次,更新参与冲突次数最多的变量的活跃值,选择合适的分支决策变量,改变变量赋值序列.本文基于国际SAT竞赛中知名求解器Glucose3.0,MapleCOMSPS,Glucose4.1以及Lingeling,分别实现了改进算法——DDIDT.实验结果可得,改进求解器GlucoseDDIDT相比Glucose3.0降低决策数为11.2%～61.6%,且GlucoseDDIDT求解难度较大实例的个数提高了63.9%.针对求解2015年到2017年SAT竞赛的应用类型的实例,GlucoseDDIDT相比Glucose3.0的求解个数增长了6.0%;改进求解器MapleCOMSPSDDIDT相比MapleCOMSPS求解个数提高了2.5%;相比Glucose4.1,改进求解器Glucose4.1DDIDT的求解个数增长了3.1%;虽然LingelingDDIDT求解实例总数相比Lingeling只增加1个,但求解时间有所减少.实验表明,所提策略可有效识别重复路径,适时选择合适的分支决策变量,改变搜索路径,减少计算时间.

• 单位
  西南交通大学; 数学学院