| 基于学习子句删除策略的SAT求解器分支策略 |
| |
| 引用本文： | 王钇杰,徐扬,吴贯锋.基于学习子句删除策略的SAT求解器分支策略[J].计算机科学,2021,48(11):294-299. |
| |
| 作者姓名： | 王钇杰 徐扬 吴贯锋 |
| |
| 作者单位： | 西南交通大学数学学院 成都610031;系统可信性自动验证国家地方联合工程实验室 成都610031 |
| |
| 摘 要： | 对于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％.
|
| 关 键 词： | 活跃度 学习子句 可满足性问题 学习子句删除策略 完备算法 |
Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver |
| |
| WANG Yi-jie,XU Yang,WU Guan-feng.Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver[J].Computer Science,2021,48(11):294-299. |
| |
| Authors: | WANG Yi-jie XU Yang WU Guan-feng |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
