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

A Dynamic Decision Strategy Based on Identification of Duplicate Trail

在现有基于冲突学习子句的求解器中,重启和变量相位存储技术的频繁应用,导致重启之后产生大量重复变量赋值序列,在求解过程中对变量重复赋值会浪费求解资源.本文提出一种基于识别重复路径的动态决策策略.首先,检测搜索过程中产生的重复赋值变量序列,算法中参数依据子句数与变元数的比率而动态变化;其次,更新参与冲突次数最多的变量的活跃值,选择合适的分支决策变量,改变变量赋值序列.本文基于国际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个,但求解时间有所减少.实验表明,所提策略可有效识别重复路径,适时选择合适的分支决策变量,改变搜索路径,减少计算时间.

It is obvious that frequent restarts were introduced in current conflict driven clause learning(CDCL)solvers.Due to the wide adoption of variable state independent decaying sum(VSIDS)and phase saving,a large proportion of the assignment trails are re-created exactly as the ones before restarts.It empirically exploits the observation that CDCL solvers tend to make the same variables in a similar order.Repeated assignment of variables in the solution process will waste the calculation resources.This paper proposed a new strategy—A dynamic decision strategy based on the identification of duplicate trail(DDIDT).Firstly,the phenomenon of duplicate assignments trails between two succeeding restarts is illustrated by an example and experiment,then designing an algorithm for identifying those duplicate trails feasibly.And the setting of parameters of the threshold of trails is determined by a series of experiments.Secondly,one of the most surprising aspects of the relatively recent practical progress of CDCL solvers is that VSIDS decision selection heuristic.The VSIDS strategy selects decision variable based on a strong activity-based heuristic.Initially,the score of each variable is the frequency of a literal occurrence in all clauses,and increase all variables additively by 1 which involved in conflicts.These scores are sorted in a trail.More significantly,the size of the real-world instances always being millions of clauses and variables,then the score of every variable which occurs most frequently is also high,so few variables of the front of the trail are still the same even if the trail updates scores periodically(every 256th conflict),because of the increment is one,which is too small that compared to its initial score.As a consequence,when restart for instance,which contains millions of clauses and variables,the front of the trail maybe still holds the same.Changing the assignment trails is essentially turning the order of assigning those variables.Therefore,for changing the activity of variable to a greater degree,the paper proposed a new branching strategy,that is,counting the number of times each variable participates in a conflict and recording the variable that responsible for the most conflict between two restarts,then rewarding this variable with a bonus in order to turn the assignment sequence,accordingly the search path is transformed.We implemented the DDIDT algorithm respectively as a part of these well-known solvers:Glucose3.0,MapleCOMSPS,Glucose4.1 and Lingeling solver,all these solvers got better ranking in international SAT competitions.These empirical results further shed light on that,compared with the Glucose3.0 solver,the rate of reducing decisions of modified Glucose_DDIDT solver is decreased by 11.2%-61.6%,and the number of solved hard instances of modified Glucose_DDIDT is increased by 63.9%compared with Glucose3.0,the above experimental results show that the proposed strategy can work well.To better illustrate the advantages of the proposed method,Application Main-track instances,which originated from the SAT Competitions 2015 to 2017,were also tested by those solvers which integrated DDIDT algorithm:MapleCOMSPS_DDIDT,Glucose4.0_DDIDT and Lingeling_DDIDT.Compared with Glucose3.0,the number of solved instances of the improved Glucose_DDIDT is improved by 6.0%;compared with MapleCOMSPS,the number of solved instances of MapleCOMSPS_DDIDT is added by 2.5%,meanwhile,the number of solved instances of Glucose4.0_DDIDT is improved up to 3.1%compared with Glucose4.0;Although the total number of solved instances of Lingeling_DDIDT is increased by 1 compared with Lingeling,the overall solution performance is improved.Experimental results indicate that the proposed dynamic decision strategy can efficiently identify duplicate assignments trails and deal with it by choosing appropriate decision variable adaptively,reduce the computation time.