基于学习子句删除策略的SAT求解器分支策略  

Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver

作　　者：王钇杰 徐扬[1,2] 吴贯锋 WANG Yi-jie;XU Yang;WU Guan-feng(School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610031,China)

机构地区：[1]西南交通大学数学学院,成都610031 [2]系统可信性自动验证国家地方联合工程实验室,成都610031

出　　处：《计算机科学》2021年第11期294-299,共6页Computer Science

基　　金：国家自然科学基金(61673320);中央高校基本科研业务费专项资金(2682020CX59)。

摘　　要：对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突。但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响。针对此问题,提出了一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度。基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD。以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较。实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了15.5%。在2019年的例子测试中,Maple-DL_VDALCD比MapleLCMDistChronoBT-DL-v2.1多求出17个例子,增加了7.6%。For the SAT solver,most popular branch variable decision-making strategies are based on the variable activity evaluation of conflict.The unassigned variable with the maximum activity is selected as the decision variable,and the most recent conflict is solved first.However,they all ignore the impact of the number of clauses containing decision variables on the Boolean constraint propagation(BCP).To solve this problem,this paper proposes a branch variable decision strategy(VDALCD)based on the learning clause deletion strategy,which reduces the activity of variables in the deleted clause when the clause is deleting.Based on the VDALCD strategy,Glucose4.1 and MapleLCMDistChronoBT-DL-v2.1 are improved to solvers Glucose4.1_VDALCD and Maple-DL_VDALCD.This paper uses 2018 and 2019 SAT international competition questions as benchmark test cases to compare the improved version with the original version of the solver.The experimental results show that Gluose4.1_VDALCD finds out 26 more examples than Gluose4.1,an increase of 15.5%in the 2018 example test.In the 2019 example test,Maple-DL_VDALCD finds out 17 more examples than MapleLCMDistChronoBT-DL-v2.1,an increase of 7.6%.

关 键 词：活跃度 学习子句 可满足性问题 学习子句删除策略 完备算法 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]