﻿ 基于变量混合特征的分支启发式策略
 计算机系统应用  2020, Vol. 29 Issue (3): 200-205 PDF

1. 西南交通大学 数学学院, 成都 611756;
2. 西南交通大学 系统可信性自动验证国家地方联合工程实验室, 成都 611756

Branching Heuristic Strategy Based on Variable Mixing Features
AI Sen-Yang, SONG Zhen-Ming, SHEN Xue
School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China;
National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 611756, China
Foundation item: National Natural Science Foundation of China (61673320)
Abstract: Advanced SAT solvers solve large application instances with efficient branching heuristics. At present, the VSIDS strategy is the most representative branching strategy based on conflict analysis. It is widely used because of its robustness. However, in each conflict analysis, the incremental method of determining the variable activity is too single. To solve this problem, this study proposes a branch heuristic algorithm based on variable mixing features. The purpose is to fully utilize the different information features carried in the variables involved in conflict analysis to distinguish variables, and further guide the variable activity growth. The proposed branching strategy algorithm is embedded into Glucose4.1 to form the solver Glucose4.1+MFBS. Through experimental comparison and analysis, the experimental results show that the improved branching algorithm has certain advantages over the original VSIDS strategy, and the number of solutions increases obviously.
Key words: SAT problem     CDCL algorithm     branch heuristic     conflict analysis     learning clause

1 预备知识 1.1 相关定义

1.2 相关过程

(1)布尔约束传播过程(Boolean Constraint Propagation, BCP)

BCP过程也称为单元推导. BCP过程即是反复利用单元子句规则对子句集里的合取范式不断地化简, 直到子句集中不再存在单元子句或者出现冲突子句为止. 随着搜索的不断进行, 一个合取范式想要被满足, 则要求其所组成的子句都是可满足的, 所以通过单元规则会导致一些变量必须被赋值为真(子句中除了一个未赋值的变量外, 其余变量都被赋值为0), 通过单元规则导致的变量赋值被称之为蕴涵[12,13]. 因为子句集中变量的蕴涵关系, 所以BCP过程又可以通过蕴涵图直观地表示出来.

 \begin{aligned} C = \{ &{C_3} = \neg {x_2} \vee {x_{12}},{C_4} = {x_4} \vee \neg {x_{13}}, \\ &{C_5} = {x_6} \vee {x_8} \vee \neg {x_{12}},{C_6} = {x_3} \vee {x_2}, \\ &{C_7} = {x_{10}} \vee \neg {x_6} \vee {x_{13}},{C_8} = \neg {x_2} \vee \neg {x_8} \vee {x_{15}}, \\ &{C_9} = \neg {x_4} \vee \neg {x_6} \vee {x_{11}}, \cdot \cdot \cdot \} \\ \end{aligned}

 图 1 蕴涵图

(2)学习子句形成过程

2 现有分支启发策略

Chaff算法表明整个搜索过程中布尔约束传播占用大部分时间, 一个好的分支策略可以快速找到决策变量, 减少冲突次数, 加速BCP过程, 因此好的分支决策对提高整个SAT求解器的运行效率意义重大.

2.1 VSIDS策略

VSIDS (Variable State Independent Decaying Sum)分支变量启发式策略, 该策略由Moskewic等于2001年提出[8]. 相比早期的分支启发式, VSIDS分支变量启发式策略很好地结合了冲突分析过程.

(1)每一个变量的正、负文字都分配一个计数器s, 并且初始值设置为0;

(2)当学习子句加入到子句集时, 该子句中所有的文字活性;

(3)每次分支决策时选择计数器分值最高未赋值的文字进行赋值, 在有多个相等计数器的情况下, 随机选择一个文字进行赋值;

(4)所有文字的得分周期性地除以一个常数.

2.2 VSIDS策略的有效变体

ACIDS (Average Conflict-Index Decision Score)[16], ACIDS策略与EVSIDS一样, 对每个变元不区分正负方向, 只保留一个计数器. 变元活跃度累加方式为 ${s^{'}} = (s + i)/2$ , 式中 $i$ 为冲突次数. ACIDS策略不仅给后来的涉及冲突的变量赋予更大的权重, 而且随着冲突次数的增加较早发生的冲突对搜索的影响呈指数下降. 同时ACIDS中变量的得分仅受冲突次数 $i$ 的限制, 因此, ACIDS策略比EVSIDS策略更加平滑.

3 基于变量混合特征分支策略

(1)为每个变量设置一个计数器, 初始为0;

(2)对于参与冲突分析的变量, 活跃度增长方式为 ${s'} = s + Hyb\left( v \right) \cdot Inc$ ;

(3)每次分之决策时, 挑选计数器分值最大的为赋值的变量, 作为下一个决策变量. 若多变量值相同, 则随机挑选一个文字赋值.

 $Hyb(v) = \alpha \frac{{lastconflict}}{{nconflicts}} + (1 - \alpha )\frac{1}{{LBD + 1}}$

1. for $\scriptstyle v \in Vars$ do

2. 　　 activity[v] = 0

3. 　 end for

4. loop

5. 　 if a conflict occurs then

6. 　　 for $v \in$ variables involved in conflict analysis

7. 　　　 $\scriptstyle activity\left[ v \right] = activity\left[ v \right] + Hyb(v)* Inc$

8. 　　 end for

9. 　 else

10. 　　 unassigned = unsigned variables

11. 　　 $\scriptstyle {v^*} = \arg {\max _v} \in {}_{unassigned}activity[v]$

12. 　 end if

13. end loop

14. return ${v^*}$

4 实验分析

Glucose作为国际先进的求解器, 近些年部分优秀的求解器都是在此基础上的改进, 2009年Glucose 3.0获得SAT Main Track组竞赛冠军, 2017年其并行版本求解器Syrup获得冠军等, 本文则选取最新的Glucose4.1求解器为基础, 把MFBS分支策略嵌入Glucose4.1生成Glucose4.1+MFBS版本, 下一步将两版本进行实验对比分析.

4.1 实验环境

4.2 实验方法

4.3 实验结果分析

 图 2 Glucose与Glucose_4.1+MFBS的求解性能对比

 图 3 Glucose4.1与Glucose4.1+MFBS( $\alpha$ )求解性能对比

5 结论与展望

 [1] Cook SA. The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing. New York, NY, USA. 1971. 151–158. [2] Davis M, Logemann G, Loveland D. A machine program for theorem-proving. Communications of the ACM, 1962, 5(7): 394-397. DOI:10.1145/368273.368557 [3] Marques-Silva J, Lynce I, Malik S. Conflict-driven clause learning SAT solvers. In: Biere A, Heule M, Van Maaren H, et al, eds. Handbook of Satisfiability. Amsterdam: IOS Press, 2009. 131–153. [4] Marques-Silva J. The impact of branching heuristics in propositional satisfiability algorithms. Proceedings of the 9th Portuguese Conference on Artificial Intelligence. Évora, Portugal. 1999. 62–74. [5] Marques-Silva JP, Sakallah KA. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 1999, 48(5): 506-521. DOI:10.1109/12.769433 [6] Audemard G, Simon L. Predicting learnt clauses quality in modern SAT solvers. Proceedings of the 21st International Joint Conference on Artificial Intelligence. Pasadena, CA, USA. 2009. 399–404. [7] Gomes CP, Selman B, Crato N. Heavy-tailed distributions in combinatorial search. Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming. Linz, Austria. 1997. 121–135. [8] Moskewicz MW, Madigan CF, Zhao Y, et al. Chaff: Engineering an efficient SAT solver. Proceedings of the 38th Design Automation Conference. Las Vegas, NV, USA. 2001. 530–535, doi: 10.1109/DAC.2001.935565. [9] Mahajan YS, Fu ZH, Malik S. Zchaff2004: An efficient sat solver. Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing. Vancouver, BC, Canada. 2005. 360–375. [10] Eén N, Sörensson N. An extensible SAT-solver. Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Santa Margherita Ligure, Italy. 2004. 502–518. [11] Audemard G, Simon L. GLUCOSE: A solver that predicts learnt clauses quality. SAT Competition, 2009. 7–8. http://www.satcompetition.org/2009/. [12] 王国俊. 数理逻辑引论与归结原理. 北京: 科学出版社, 2003. [13] 张建. 逻辑公式的可满足性判定——方法、工具及应用. 北京: 科学出版社, 2000. [14] Zhang LT, Madigan CF, Moskewicz MH, et al. Efficient conflict driven learning in a Boolean satisfiability solver. Proceedings of the 2001 IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers. San Jose, CA, USA. 2001. 279–285. [15] Biere A. Adaptive restart strategies for conflict driven SAT solvers. Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing. Guangzhou, China. 2008. 28–33. [16] Biere A, Fröhlich A. Evaluating CDCL variable scoring schemes. Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing. Austin, TX, USA. 2015. 405–422. [17] Liang JH, Ganesh V, Poupart P, et al. Exponential recency weighted average branching heuristic for SAT solvers. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Phoenix, AZ, USA. 2016. 3434–3440. [18] Liang JH, Ganesh V, Poupart P, et al. Learning rate based branching heuristic for SAT solvers. Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing. Bordeaux, France. 2016. 123–140.