CDCL SAT求解中胶水变量的刻画
人工智能
2019-04-26 v1
摘要
评估给定学习子句重要性的一种前沿准则称为文字块距离（LBD）分数。它衡量给定学习子句中不同决策层的数量。学习子句的LBD分数越低，其质量越好。LBD分数为2的学习子句被称为胶水子句（glue clauses），已知其具有很高的剪枝能力，在现代CDCL SAT求解器的子句数据库中永远不会被删除。在这项工作中，我们将胶水子句与决策变量联系起来。我们将截至当前搜索状态出现在至少一个胶水子句中的变量称为胶水变量（Glue Variables）。我们首先通过运行前沿CDCL SAT求解器MapleLCMDist于SAT Competition-2017和2018的基准测试集进行实验，表明使用胶水变量进行分支决策在推理和冲突效率上绝对优于非胶水变量。基于这一观察，我们开发了一种结构感知的CDCL变量激活度提升方案，该方案根据胶水变量在搜索迄今所学胶水子句中的出现次数来提升其活跃度分数。实证评估显示了新方法在SAT Competition 2017和2018主赛道实例上的有效性。
引用
@article{arxiv.1904.11106,
title = {Characterization of Glue Variables in CDCL SAT Solving},
author = {Md Solimul Chowdhury and Martin Müller and Jia-Huai You},
journal= {arXiv preprint arXiv:1904.11106},
year = {2019}
}