基于动态奖惩的CDCL SAT求解器分支启发式算法

计算机工程与科学

基于动态奖惩的CDCL SAT求解器分支启发式算法

陈秀兰，刘婷

（西南交通大学系统可信性自动验证国家地方联合工程实验室,四川成都 610031）

收稿日期:2018-05-24 修回日期:2018-07-13 出版日期:2019-03-25 发布日期:2019-03-25
基金资助:
国家自然科学基金（61673320）

A dynamic reward and punishment based branching

heuristic algorithm for CDCL SAT solvers

CHEN Xiulan，LIU Ting

(NationalLocal Joint Engineering Laboratory of System Credibility Automatic Verification,

Southwest Jiaotong University,Chengdu 610031,China)

Received:2018-05-24 Revised:2018-07-13 Online:2019-03-25 Published:2019-03-25

摘要/Abstract

摘要：

分支启发式算法在CDCL SAT求解器中有着非常重要的作用，传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率，受EVSIDS和ACIDS的启发，提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时，DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0，并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明，与传统、单一的奖励变量分支策略相比，所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。

关键词: SAT问题, 分支启发式算法, VSIDS, 决策层, 冲突决策层, 变量冲突频率

Abstract:

Branching heuristic algorithms play an important role in CDCL SAT solvers, and the conventional branching heuristic algorithms are more concerned with the number of conflicts when calculating the activity scores of variables and do not consider the influence of the decision level or conflict decision level. In order to improve the efficiency of solving SAT problem, we propose a dynamic reward and punishment based branching method (DRPB), which is inspired by the EVSIDS and ACIDS. Whenever a conflict occurs, the DRPB updates the activity score of variables by integrating the numbers of conflicts, decision-making level, conflict decision level, and conflict frequency of variables. We improve the Glucose version 3.0 by replacing the VSIDS algorithm with the DRPB, and conduct an empirical evaluation not only on instances of SATLIB benchmarks, but also on 2015 and 2016 SAT competitions. Experimental results show that compared with the traditional and single variable branching heuristic algorithms, the proposed strategy can reduce the size of the search tree and improve the performance of the SAT solvers by reducing the branches of the search tree and the number of Boolean constraint propagation.

Key words: SAT problem, branching heuristic algorithm, VSIDS, decision level, conflict decision level, conflict frequency of variable

陈秀兰，刘婷. 基于动态奖惩的CDCL SAT求解器分支启发式算法[J]. 计算机工程与科学.

CHEN Xiulan，LIU Ting.

A dynamic reward and punishment based branching

heuristic algorithm for CDCL SAT solvers

[J]. Computer Engineering & Science.

[1]	冯心妍, 吴贯锋, 张丁荣, 王恪铭, . 基于近期文字极性分配的学习子句评估算法[J]. 计算机工程与科学, 2023, 45(11): 1941-1948.
[2]	芦磊, 王晓峰, 梁晨, 张九龙. 多文字可满足SAT问题的相变点上界[J]. 计算机工程与科学, 2022, 44(07): 1282-1290.
[3]	王帅, 王晓峰, 梁田, 李志. 一种求解命题公式骨干集的警示传播算法[J]. 计算机工程与科学, 2021, 43(11): 2056-2061.
[4]	吴贯锋1,2，徐扬2,3,陈青山1,2,何星星2,3，常文静1,2. 基于频次的SAT问题学习子句混合评估算法[J]. 计算机工程与科学, 2019, 41(08): 1374-1380.
[5]	付慧敏1,2,徐扬2，何星星2,宁欣然1,2. 基于任务分配与调度的GSAT算法求解3-SAT问题[J]. 计算机工程与科学, 2018, 40(08): 1366-1374.
[6]	王晓峰,许道云,唐瑞雪. 基于DPLL的混合遗传算法求解SAT问题[J]. J4, 2010, 32(5): 54-56.
[7]	赵同昇[1] 朱文兴[2]. MAX—SAT问题一种改进的局部搜索算法[J]. J4, 2008, 30(11): 50-52.