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

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