论文研究-基于演绎长度的学习子句删除策略.pdf

发布时间：2022-05-29 发布人：admin 分类：说明书资料大小：0.69M 资料格式：pdf 举报版权申诉

weixin_38743481-11692132-4744300845397831849.pdf-第1页.png

第1页 / 共7页

weixin_38743481-11692132-4744300845397831849.pdf-第2页.png

第2页 / 共7页

weixin_38743481-11692132-4744300845397831849.pdf-第3页.png

第3页 / 共7页

weixin_38743481-11692132-4744300845397831849.pdf-第4页.png

第4页 / 共7页

weixin_38743481-11692132-4744300845397831849.pdf-第5页.png

第5页 / 共7页

weixin_38743481-11692132-4744300845397831849.pdf-第6页.png

第6页 / 共7页

weixin_38743481-11692132-4744300845397831849.pdf-第7页.png

第7页 / 共7页

文本预览

30 2018，54（16） Computer Engineering and Applications 计算机工程与应用基于演绎长度的学习子句删除策略常文静 1，3，徐扬 2，3，吴贯锋 1，3 CHANG Wenjing1，3, XU Yang2，3, WU Guanfeng1，3 1. 西南交通大学信息科学与技术学院，成都 610036 2. 西南交通大学数学学院，成都 610036 3. 系统可信性自动验证国家地方联合工程实验室，成都 610036 1.School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610036, China 2.School of Mathematics, Southwest Jiaotong University, Chengdu 610036, China 3.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610036, China CHANG Wenjing, XU Yang, WU Guanfeng. Learned clauses reduction strategy based on length of deduction. Com- puter Engineering and Applications, 2018, 54（16）：30-36. Abstract：Learned clauses database reduction heuristics are one of the most important components of a Conflict Driven Clause Learning（CDCL）SAT solver, which are used to avoid memory consumption and sustain unit propagation speed. The learned clause to be removed is different based on different evaluation criteria, which is measuring the usefulness of learned clause. A CDCL based SAT solver can be formulated as a resolution proof system with a learned clause deletion strategy. On this basic, a learned clauses reduction strategy based on length of resolution is proposed, and combined with Literals Blocks Distance（LBD）evaluation criteria. According to the basis of sorting clauses, two different combination algorithms are formed. Based on international SAT competition instances, this paper analyzes the experimental compari- son with the current mainstream solver. Experimental results indicate that compared with the LBD-based criteria method, the number of the proposed combined method is increased by 4.1%. The proposed strategy can preferably estimate the use- fulness of learned clauses and efficiently improve the performance of solving instances. Key words：satisfiability problem; conflict driven clause learning; learned clauses reduction; length of deduction 摘要：学习子句删除策略是 CDCL-SAT 求解器中的一个重要内容，可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的，极大地影响求解效率。基于 CDCL 算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程，基于此，提出一种基于演绎长度的学习子句评估方法，并与现有的基于文字块距离的评估方法结合，根据排序子句的基准不同，形成两种不同的结合算法。采用国际 SAT 竞赛的基准实例，与目前主流的求解器进行了实验对比分析。结果表明，所提的结合算法能更好地评估学习子句的有用性，较基于文字块距离策略的求解个数提高了 4.1%，说明所提策略具有一定的优势。关键词：可满足性问题；冲突驱动子句学习；学习子句删除；演绎长度文献标志码：A 中图分类号：TP311.1 doi：10.3778/j.issn.1002-8331.1805-0439 1 引言布尔可满足问题（Boolean Satisfiability Problem， SAT 问题）是首个被证明是 NP 完全的问题[1]，具有十分重要的理论意义。布尔变量 x 可以被赋值为 true（1）或 false（0），由一个或多个变量的析取组成一个子句，若子句中至少存在一个变量赋值为 1，则该子句是可满足的。由一个或多个子句的合取构成合取范式（Conjunction Normal Form，CNF），SAT 问题一般可转化成 CNF 表基金项目：国家自然科学基金（No.61673320）；中央高校基本科研业务费专项资金（No.2682018ZT10）。作者简介：常文静（1989—），女，博士，研究领域为智能信息处理和自动推理，E-mail：wenjing1021@163.com；徐扬（1956—），男，博士，教授，博导，研究领域为逻辑代数、不确定性推理和自动推理；吴贯锋（1986—），男，博士，研究领域为智能信息处理和自动推理。收稿日期：2018-05-29 修回日期：2018-07-11 文章编号：1002-8331（2018）16-0030-07 计算机工程与应用www.ceaj.org

常文静，徐扬，吴贯锋：基于演绎长度的学习子句删除策略 2018，54（16） 31 示。判定 SAT 问题的满足性是指若存在一组变量赋值 {x1,x2,⋯,xN}（ N 为子句集 F 中的变量个数），使得子句集 F 中所有的子句都是可满足的，则子句集 F 是可满足的，或者给出证明，对于变量的任何赋值，子句集 F 都是不可满足的。近年来，SAT 问题的判定技术也应用在实际领域中，如人工智能规划（AI Planning）、定理证明、软件及硬件验证、集成电路设计与验证等。求解 SAT 问题的算法主要分为两类：完备算法和不完备算法。尽管不完备算法可快速求解，却不能证明问题是不可满足的。完备算法不仅能在问题的属性是可满足时给出问题的解，而且在问题无解时可以给出一个完备的证明，证明此问题是不可满足的。现实生活中许多实际应用问题需要证明问题的无解，因此本文主要介绍完备算法的相关内容。当前主流的 SAT 完备求解算法几乎都是基于 DPLL （Davis Putnam Longmann Loveland）算法 [2]衍生而来， DPLL 算法主要利用单文字规则、纯文字规则和分裂规则，通过深度优先搜索二叉树，求解子句集，但是由于 SAT 问题的特殊性，导致 DPLL 算法在最坏情况下具有以问题规模为指数的时间复杂性。因此，许多研究学者提出了改进算法。其中，冲突驱动子句学习（Conflict Driven Clause Learning，CDCL）算法 [3]在 DPLL 算法基础框架上，主要在以下方面做出改进：变量决策[4-7]，冲突分析与子句学习[3]，重启[8]和数据结构[7，9]。 CDCL 算法的主要思想是：当基于深度二叉树搜索时发生冲突，分析出冲突产生的原因，导致冲突产生的子句就会被记录下来，称为学习子句。每次冲突时，相应地产生一个学习子句，由于实际应用问题的规模较大，其冲突次数达到百万次，学习子句的数目会随着冲突数目的增加而不断增大，在最坏情况下这种增长速度是变量规模的指数级。学习子句数目的增加影响 BCP 的效率，并最终导致可用内存耗尽。Silva 和 Sakallah[3] 曾证明，大量的已学习子句对于减小搜索树的空间并不是特别有用，有时只会对搜索过程带来额外的开销。因此现今的许多 SAT 求解器都添加了学习子句的删除功能，提高 BCP 的效率以及避免出现内存爆炸问题。 Silva 和 Sakallah 设计的求解器 GRASP[3]中提出一种基于大小边界（size-bounded）的学习子句删除策略：一旦学习子句中文字个数超过设定的整数 k 时，则删除这些子句。Bayardo 和 Schrag 在求解器 RelSAT[10]中提出一种基于相关性边界（relevance-bounded）的学习子句删除策略：当学习子句中未被赋值文字的个数超过设定的阈值 i 时，则删除这些学习子句。求解器 Chaff[7]中采用一种“懒散”的学习子句删除策略，学习子句添加到子句数据库，当此学习子句中未被赋值的文字个数首次大于 n 个时（ n 一般取值范围为 100~200），此学习子句被标记为需要“删除”的状态，在之后的内存清理过程中统一被删除。求解器 BerkMin[11]的设计者认为最新得到的学习子句具有较大的价值，因为需要耗费更多的时间来推导出最新得到的学习子句。BerkMin 中不仅考虑学习子句生成的先后顺序，即将学习子句存储在队列中（先进先出），删除队列中前 1/16 的学习子句（但是不包含那些文字个数小于 8 的学习子句）；而且考虑学习子句的长度大小，当队列中后 15/16 的学习子句的文字个数大于 42 时，也会被删除。求解器 Minisat[12]中为每个学习子句设置活跃值 activity ，当子句与冲突有关时（包括学习子句），增加其活跃值，认为活跃值小于其设定的边界值 k 的子句是不相关的，需要被删除。Glucose 求解器[13]中使用一种新的评价学习子句的策略——文字块距离（Literals Blocks Distance，LBD），即子句中所有文字所在的不同的决策层个数。认为越小 LBD 值的子句的相关性越高，其价值越大，因此对学习子句按照 LBD 值的大小从大到小排序，删除一半的学习子句（但不包括 LBD 值为 2 的子句）。现有的大多数 SAT 求解器中也使用此子句策略，如 Lingeling[14]求解器中动态地选择 LBD 和 activity 两种评估学习子句质量的标准，如果学习子句的 LBD 值过大或过小，选择 activity 评估标准；求解器 MapleCOMSPS[15]中综合使用 LBD 和 activity 两种评估标准，只保留 LBD 值小于 6 的学习子句，其余子句按照 activity 评估。文献[16]建立一个基于过程保存的相关函数，此函数在搜索的某阶段动态地激活或者冻结子句。文献[17]提出一种基于回退层次（BackTrack- ing Level，BTL）的方法，计算学习子句中不同的 BTL 大小，实验发现当 BTL 小于 3 时学习子句在布尔约束传播中使用频率高于其他子句，因此认为对求解过程具有更大的相关度，删除那些相关度小的子句。文献[18]认为学习子句的长度对求解过程有着重要的作用，基于此，提出一种基于随机有界长度的子句删除策略，定义短子句的长度为 k（即子句中文字个数为 k ），随机删除子句长度大于 k 的子句，适当地保存一些长子句对于推演归结证明是必要的，实验表明增加随机性对于求解部分的 SAT 问题是有效的。文献[19]提出折中度的概念，综合考虑子句的长度 (size) 、活跃值 (activity) 和 LBD ，通过折中度的大小评估学习子句的质量。文献[20]针对现有 Glucose 中基于 LBD 的子句删除策略，通过大量实验发现对于 LBD 值为 2 的子句（Glue clause）的利用率过低，基于此，设置不同学习子句的生存时间是不同的。尽管已存在多种管理学习子句策略，但由于实际问题的多样性，目前不存在一种管理学习子句策略适用于求解所有的实例问题。因此，本文提出一种基于归结演绎长度评估学习子句有效性方法，并通过举例与现有的基于 LBD 评估方法进行了测试分析，根据学习子句排序基准不同，提出两种不同的结合算法。对比实验结果表明，所提策略能更好地识别对求解过程有用的学习子句，显著地提高求解效率。计算机工程与应用www.ceaj.org

32 2018，54（16） Computer Engineering and Applications 计算机工程与应用 2 基础知识算法 1 典型 CDCL 算法输入：CNF 公式 Σ 。输出：可满足 SAT 或不可满足 UNSAT。 1. ξ = Ф ； // ζ 表示变量赋值集合 2. Δ = Ф ； // Δ 表示学习子句数据库 3. dl = 0 ； // dl 表示决策层次 4. while (true) do 5. conflict = unitPropagation(Σ,ζ) ； if (conflict! = null) then 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16. 17. 18. 19. 20. learntclause = conflictAnalysis(Σ,ζ) ； btl = computeBackLevel(learntclause,ζ) ； if (btl == 0) Δ = Δ ⋃{ then return UNSAT learntclause ； } if（restart（）） then btl = 0 ； backjump(btl) ； dl = btl ； else if (ζ ⊧Σ) then return SAT； if（timeToReduce（）） then reduceDB (Δ) ； var = pickDecisionVar(Σ) ； dl = dl + 1 ； ξ = ξ ⋃{ selectPhase(var) ； } 21. end 算法 1 为基于 CDCL 的 SAT 求解器的框架。通过变量决策分支函数 pickDecisionVar（）选择决策变量 var, 并通过函数 selectPhase（）进行赋值（算法第 18~20 行），若所有变量都已被赋值，即 ζ 表示公式 Σ 的一个赋值集合，则可判定子句集 Δ 的属性是可满足的（SAT），并且终止算法（算法第 15~16 行）。unitPropagation（）是单元传播函数，若单元传播过程中发生冲突 conflict，则利用 conflictAnalysis（）函数生成学习子句 learntclause，且将学习子句添加到子句集 F ，并通过computeBackLevel（）函数非时序回退到决策层次 btl ，如果 btl = 0 ，则说明子句集 Δ 为不可满足的，否则，利用 backjump（）函数，回退到 btl ，从新的决策层次重新开始搜索赋值。restart（）表示重启函数，当求解器达到设置的触发重启条件时，则直接回退到第 1 决策层，撤销之前所有的变量赋值。算法第 17 行的 timeToReduce（）表示达到删除学习子句的条件，此时需要调用函数 reduceDB（）对学习子句数据库 Δ 进行删除。删除学习子句时需考虑两方面：（1）选择需要删除的子句，即对应于算法 1 中 reduceDB（）函数；（2）删除子句的频率，即何时需要删除无用的学习子句，即对应于算法 1 中的 timeToReduce（）函数。Minisat 和 Glucose 中函数 timeToReduce（）满足以下条件：冲突次数达到条件 lfirst + linc × x,其中 x 为调用删除策略的次数，lfirst = 2 000, linc = 300 。当调用 reduceDB（）函数时，将子句按照某种评估标准的值从大到小排序，删除序列中前一半的子句。这里，依然保持 timeToReduce（）函数的条件不变，主要研究 reduceDB（）函数中学习子句质量的评估标准。 3 基于演绎长度的学习子句删除策略对于一个以 CNF 形式表示的公式 F 和子句 Ck ，若存在一个子句序列 Π ={C1,C2,…,Ck} ，则称 Π 是由公式 F 推导出子句 Ck 的一个归结式。其中，∀Ci ∈ F ，子句 Ci 满足以下任意条件即可：（1）Ci ∈ F ；（2）Ci 是由子句 Cm 和 Cn (m,n ≤ i) 推导出来的，其推导规则如下： Cm = x ∨ A,Cn = -x ∨ B ⇒ Ci = A ∨ B 其中 A 和 B 为子句，x 为变量。文献[21]已证明基于 CDCL 的 SAT 求解器可被形式化为归结演绎证明系统。因此，现有的 CDCL-SAT 求解器的求解过程可以是一个包含删除子句集策略的归结演绎过程。当有冲突发生时，通过学习子句确定搜索树的回退层次，若学习子句中每个变量相对应的赋值层次都较小（即距离二叉搜索树的根节点较近），确定的回退层次也越小，对搜索空间的约简能力也越强，因此认为这些学习子句对搜索过程是相关的、有效的。学习子句可以通过归结过程演绎得到，因此通过演绎的长度 length 来评估学习子句的相关性。设有学习子句 Cl ，假设 Π ={C1,C2,…,Cl} 是由公式 F 推导出学习子句 Cl 的一个归结式，则称学习子句 Cl 的演绎长度 length 为 l ，记 Cl(length) = l 。若学习子句的 l 值越小，说明通过归结得到此学习子句演绎路径越短，进而此学习子句中的每个变量的决策层也较小，相对应的回退层次也越小，这些学习子句应该被保留。 3.1 举例说明为了说明学习子句的演绎长度 length 和 LBD 值在求解过程中的变化规律，随机选取 SAT 竞赛库中的实例 g2-ak128boothbg1btisc.cnf 测试说明。 3.1.1 依据 LBD 值排序首先，将生成的学习子句按照 LBD 值从大到小排序，如图 1 所示。 X 轴表示生成的学习子句数量，求解实例 g2-ak128boothbg1btisc.cnf 的冲突次数为 954 次，因此生成 954 个学习子句。 Y 轴表示学习子句分别对应的 LBD 值。从图 1 可以看出，生成的学习子句的 LBD 值的分布范围不连续，有一定的区间变化。当需要删除学习子句时，按照 LBD 值从大到小的排序顺序，删除一半的学习子句，即删除图 1 中 1 到 477 的子句。当学习子句依据 LBD 值排序时，每条子句所对应的 length 值如图 2 所示。 X 轴表示生成学习子句数量， Y 轴表示每条学习子句所对应的 LBD 值和 length 值。计算机工程与应用www.ceaj.org

常文静，徐扬，吴贯锋：基于演绎长度的学习子句删除策略 2018，54（16） 33 值 D B L 的句子习学 400 350 300 250 200 150 100 50 0 200 400 600 学习子句个数 800 1 000 图 1 学习子句的 LBD 值的排序值 h t g n e l 的句子习学 7 000 6 000 5 000 4 000 3 000 2 000 1 000 0 200 400 600 学习子句个数 800 1 000 图 4 学习子句的 length 值的排序值数 7 000 6 000 5 000 4 000 3 000 2 000 1 000 0 LBD length 200 400 600 学习子句个数 800 1 000 数次用使 35 30 25 20 15 10 5 0 1 000 2 000 3 000 4 000 5 000 6 000 7 000 学习子句的 length 值图 2 学习子句对应的 LBD 值和 length 值图 5 不同 length 值的学习子句被使用的次数同时统计了不同 LBD 值的学习子句在求解过程中被使用的次数（即参与单元传播和冲突分析的总次数），如图 3 所示。 X 轴表示每个学习子句相对应的 LBD 值，Y 轴表示不同 LBD 值的学习子句在求解过程中被使用的次数。数次用使 300 250 200 150 100 50 0 50 100 150 200 250 300 350 400 学习子句的 LBD 值图 3 不同 LBD 值的学习子句被使用次数从图 3 可以看出，LBD < 10 时学习子句被使用次数较多。当 LBD = 6 时，其被使用次数多达 291 次。 3.1.2 依据 length 排序类似于 3.1.1 小节，图 4 表示学习子句相对应的 length 值的排序变化。从图 4 可以看出，length 值的变化范围广泛。图 5 表示不同 length 值的学习子句被使用的次数情况。从图 5 可以看出，学习子句的 length 值越小，在求解过程中被使用的次数越多，随着 length 值的增大，大多数学习子句被使用的次数为 1。 3.1.3 比较分析当求解器执行删除操作时，进一步分析被删除的学习子句的 LBD 值与 length 值之间的关系。按照 3.1.1 小节中基于 LBD 值的评估方法，1 到 477 范围的子句需要被删除。但是从图 2 得出，被删除子句的 length 值的变化范围较大，最小值为 lengthmin = 51 ，最大值为 lengthmax = 6 169 ，因此，若这些被删除的学习子句按照 length 值评估其质量时，给出不同 length 值的被删除的学习子句在求解过程中被使用的次数在图 5 中的分布情况，如图 6 所示。图 6 中绿色的点表示被删除的学习子句的 length 值在求解过程中被使用的次数。从图 6 可以看出，当依据 LBD 值的评估方法删除学习子句时，仍有部分学习子句的 length 较小，被使用次数较高，当 length = 212 时，使用次数为 48 次，这些子句的相关性较高，对求解作用较大，应该被保留。同理，当按照 3.1.2 小节中 length 值的评估方法，1 到 477 范围的子句需要被删除，为了方便观察，单独列出图 4 中被删除学习子句所对应的 LBD 值变化。如图 7 所示。从图 7 可以看出，被删除的那些学习子句部分的 LBD 值较小，最小 LBD = 9 ，在图 3 中其对应的被使用次数为 72 次。同理，给出被删除的学习子句在依据 LBD 值评估时在求解过程中被使用的次数在图 3 中的分布情况，如图 8 所示。计算机工程与应用www.ceaj.org

34 2018，54（16） Computer Engineering and Applications 计算机工程与应用数次用使 120 100 80 60 40 20 0 1 000 2 000 3 000 4 000 5 000 6 000 7 000 被删除的学习子句的 length 值图 6 被删除学习子句不同 length 值的被使用次数数次用使数次用使 400 350 300 250 200 150 100 50 0 100 200 300 400 500 被删除的学习子句图 7 被删除学习子句的 LBD 值 300 250 200 150 100 50 0 50 100 150 200 250 300 350 400 被删除的学习子句的 LBD 值图 8 被删除学习子句不同 LBD 值的被使用次数图 8 中绿色的点表示被删除的不同学习子句的 LBD 值被使用的次数。从图 8 得出，当依据 length 评估标准删除学习子句时，仍有部分子句的 LBD 值较小，这些子句在求解过程中被使用次数较多，当 LBD = 11 时，其被使用次数为 112 次，这些子句应该被保留。 3.2 基于 LBD 和 length 的学习子句删除策略由 3.1 节可知，评估学习子句的标准不同，相应删除的子句也是不同的。因此，本文综合考虑基于 LBD 值和 length 值两种评估标准，尽可能保留在求解过程中被频繁使用的子句。根据参照排序的基准值不同，给出两种不同的评估学习子句的方法。策略 1 当学习子句依据 LBD 值的大小排序，删除学习子句时，同时考虑学习子句的 length 值，若 C(length) < threshold1 ，保留此学习子句，其算法如下。算法 2 删除学习子句算法 reduceDB1（）输入：学习子句集合 Δ ，学习子句个数 n 。输出：新的学习子句集合 Δ ，学习子句个数 n/2 。 sortLearntClause（）； //根据 LBD 值排序 limit = n/2 ； init = 0 ； while init < limit do init ； clause = Δ[ if clause.length() ≥ threshold1 ] then removeClause（）； else saveClause（）； init + + ； return Δ ；算法 2 表示算法 1 中删除学习子句 reduceDB（）函数的执行过程。首先根据定义的排序标准—— LBD 值，对学习子句排序；假设学习子句的总数为 n ，需删除 n/2 的学习子句，即删除符合条件 clause.length() ≥ threshold1 的学习子句。为了确定参数 threshold1 的值，测试 2015 年 SAT 竞赛的 300 个 Application 类型的实例，运行时间设置为 2 000 s。表 1 表示使用不同的 threshold1 所对应的求解实例个数。表 1 不同 threshold1 的求解个数和时间 threshold1 平均求解时间/s 求解个数 100 200 300 400 170 161 153 154 419.75 408.98 378.45 409.10 在求解过程中，每条学习子句的 length 值较大，因此设置 threshold1 的值从 100 开始起步测试。从表 1 可以看出，随着 threshold1 的值逐渐增大，其求解实例个数逐渐减少，当 threshold1 = 300 和 threshold1 = 400 时，其求解个数相差 1 个，但是其平均求解时间相差较多。当 threshold1 = 100 和 threshold1 = 200 时，二者的平均求解时间相差不大，但是 threshold1 = 100 的求解个数最多。因此，threshold1 = 100 。策略 2 当学习子句依据 length 值的大小排序，删除学习子句时，同时考虑学习子句的 LBD 值，若 C(LBD) < threshold2 ，保留此学习子句，其算法如下。算法 3 删除学习子句算法 reduceDB2（）输入：学习子句集合 Δ ，学习子句个数 n 。输出：新的学习子句集合 Δ ，学习子句个数 n/2 。 sortLearntClause（）； //根据 length 值排序 limit = n/2 ； init = 0 ； while init < limit do init ； clause = Δ[ ] 计算机工程与应用www.ceaj.org

常文静，徐扬，吴贯锋：基于演绎长度的学习子句删除策略 2018，54（16） 35 if clause.lbd() ≥ threshold2 then removeClause（）； else saveClause（）； init + + ； return Δ ；算法 3 同算法 2 一样，同样表示算法 1 中删除学习子句 reduceDB（）函数的执行过程，只是二者的排序标准不同和删除学习的条件不同。算法 3 中依据 length 排序，当符合条件 clause.lbd() ≥ threshold2 时，删除学习子句。在现有的 CDCL SAT 求解器中 reduceDB（）函数是根据 LBD 值排序，删除符合 clause.lbd() ≥ 2 和 clause.size() ≥ 2 的学习子句，但是通过 3.1 节的实验分析可知，此删除标准会删除部分对求解过程起到促进作用的子句，因此算法 2 和算法 3 综合考虑了两种标准，对学习子句进一步地删选，保留更多的有用子句。同理，为了确定参数 threshold2 的值，测试 2015 年 SAT 竞赛的 300 个 Application 类型的实例，运行时间设置为 2 000 s。表 2 表示使用不同的 threshold2 所对应的求解实例个数。表 2 不同 threshold2 的求解个数和时间 threshold2 平均求解时间/s 求解个数 10 15 20 25 180 153 171 165 392.970 415.310 1 437.590 387.972 从表 2 可以看出，不同 threshold2 相对应的求解个数相差较大，并不是随着 threshold2 增大而逐渐减少，当 threshold2 = 20 时的求解个数大于 threshold2 = 15 时的求解个数，但是当 threshold2 = 10 时，其求解个数最多，且平均求解时间最少。因此，threshold2 = 10 。 4 实验本文主要在求解器 Glucose3.0 版本的基础上进行实验测试，Glucose3.0 是国际上知名的求解器，最近几年国际 SAT 竞赛专设一个基于 Glucose3.0 版本求解器改进的求解器分组比赛，测试求解器版本为 4个，Glucose_lbd、 Glucose_length、Glucose_lbd + len、Glucose_len + lbd。 Glucose_lbd 中单独使用基于 LBD 的学习子句删除策略，Glucose_length 中单独使用基于 length 的学习子句删除策略，Glucose_lbd+len 中实现策略 1，参数 threshold1 设置为100，Glucose_len+lbd中实现策略2，参数 threshold2 设置为10。实验环境：Intel Core i3-3240 CPU，3.40 GHz 处理器，8 GB 内存，运行系统为 Windows7+Cygwin2.8.1。实验中采用的测试实例来自于 2015 年 SAT 竞赛的 300 个 Main-track 组实例以及 2016 年 SAT 竞赛的 Main-track 组的 300 个 Application 类型的实例。这些实例来自于不同的实际问题，例如软件测试、硬件电路测试、图着色问题、网络安全等。实验中每个实例的求解时间不超过 3 600 s。表 3 表示使用 4 种求解器求解实例的个数对比情况。从表 3 可以看出，求解器 Glucose_len+lbd 求解实例个数最多，Glucose_lbd 求解个数最少。其中，求解器 Glucose_length 的求解个数较 Glucose_lbd 增加了 1.9%，说明基于演绎长度 length 的学习子句管理优于基于 LBD 策略，增长个数主要体现在求解不可满足实例。求解器 Glucose_len+ lbd 较 Glucose_lbd 求解个数增长了 4.1%，较 Glucose_length 求解个数增长了 2.1%；求解器 Glucose_lbd+len 较 Glucose_lbd 求解个数增长了 2.5%，较 Glucose_length 求解个数增长了 0.5%。说明综合考虑学习子句的评估标准的策略具有一定的优势。图 9 表示 4 个求解器 Glucose_lbd、Glucose_length、 Glucose_lbd+len、Glucose_len+lbd 分别求解 600 个实例的运行时间对比。图 9 中的波点曲线越靠近右边以及越靠近 x 轴时，说明此曲线表示的求解时间越小和求解个数越多。由图 9 可以看出，求解器 Glucose_lbd+ len 和 Glucose_len+lbd 的求解性能均优于 Glucose_lbd s / 间时解求 4 000 3 500 3 000 2 500 2 000 1 500 1 000 500 0 Glucose_lbd Glucose_length Glucose_lbd+len Glucose_len+lbd 100 200 300 400 求解实例个数图 9 不同求解器的求解性能测试实例 SAT 2015 （300） SAT 2016 （300）总数类别 SAT UNSAT SAT UNSAT SAT （600） UNSAT sum 表 3 不同求解器的求解实例个数 Glucose_lbd Glucose_length Glucose_lbd+len Glucose_len+lbd 137 93 56 76 193 169 362 136 98 56 79 192 177 369 139 95 57 80 196 175 371 140 97 56 84 196 181 377 计算机工程与应用www.ceaj.org

36 2018，54（16） Computer Engineering and Applications 计算机工程与应用和 Glucose_length，其中，求解器 Glucose_lbd + len 和 Glucose_len+lbd 二者的求解性能较相近，但是由表 3 和图 9 综合来看，求解器 Glucose_len+lbd 在求解个数和求解时间上均表现了一定的优势，其求解性能最优。 5 结束语本文提出一种新的学习子句管理策略——基于归结演绎长度评估学习子句有效性，并与现有的基于 LBD 评估方法进行结合。实验结果表明，新结合算法能有效地识别出对求解过程有用的子句，提高求解效率。本文中一些参数的设置是带有实验性质的，因此，之后可以针对参数设置做进一步的研究，更好地提升求解器的求解能力。参考文献： [1] Cook S A.The complexity of theorem-proving proce- dures[C]//Proceedings of the ACM Symposium on Theory of Computing，Shaker Heights，1971：151-158. [2] Davis M，Logemann G，Loveland D.A machine program for theorem proving[J].Communications of the ACM，1962， 5（5）：394-397. [3] Silva J P M，Sakallah K A.GRASP：a new search algo- rithm for satisfiability[C]//Proceedings of the IEEE/ACM International Conference on Computer- Aided Design，Los Alamitos，2002：220-227. [4] Jeroslow R G，Wang J.Solving propositional satisfiability problems[J].Annals of Mathematics & Artificial Intelli- gence，1990，1（1/4）：167-187. [5] Buro M，Kleine-Büning H.Report on a SAT competition[J]. Bulletin of the European Association for Theoretical Com- puter Science，1993，5（2）：49. [6] Selman B，Kautz H，McAllester D.Ten challenges in prop- ositional reasoning and search[C]//Proceedings of the 15th International Conference on Artificial Intelligence，Aichi， 1997：50-54. [7] Malik S，Zhao Y，Madigan C F.Chaff：an efficient SAT solver[C]//Proceedings of the Design Automation Confer- ence，Las Vegas，2001：530-535. [8] Gomes C P，Selman B，Crato N.Heavy- tailed distribu- tions in combinatorial search[C]//Proceedings of the Inter- national Conference on Principles and Practice of Con- straint Programming，Linz，1997：121-135. [9] Zhang H.SATO：an efficient propositional prover[C]//Pro- ceedings of the 14th International Conference on Auto- mated Deduction，Townsville，North Queensland，1997： 272-275. [10] Bayardo R J，Jr，Schrag R C.Using CSP look-back tech- niques to solve real- world SAT instances[C]//AAAI， 1997：203-208. [11] Goldberg E，Novikov Y.BerkMin：a fast and robust SAT- the Design Automation and solver[C]//Proceedings of Test，Acropolis，2002：142. [12] Eén N，Sörensson N.An extensible sat solver[C]//Pro- ceedings of the International Conference on Theory and Applications of Satisfiability Testing，Santa Margherita Ligure，2003：502-518. [13] Audemard G，Simon L.Predicting learnt clauses quality in modern sat solvers[C]//Proceedings of the International Joint Conference on Artificial Intelligence，Pasadena， 2009：399-404. [14] Biere A.Lingeling，Plingeling and Treengeling entering the SAT competition 2013[C]//Proceedings of SAT Com- petition，Helsinki，2013：51-52. [15] Liang J H，Ganesh V，Poupart P，et al.An empirical study of branching heuristics through the lens of global learning rate[C]//Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing，Melbourne，2017：119-135. [16] Audemard G，Lagniez J M，Mazure B，et al.On freezing the and reactivating learnt clauses[C]//Proceedings of 14th International Conference on Theory and Applica- tions of Satisfiability Testing，2011：188-200. [17] Guo L，Jabbour S，Lonlac J，et al.Diversification by clauses deletion strategies in portfolio parallel SAT solving[C]//Proceedings of International Conference on Tools with Artificial Intelligence，2014：701-708. [18] Jabbour S，Lonlac J，Sais L，et al.Revisiting the learned clauses database reduction strategies[J].arXiv：1402.1956， 2014. [19] Lonlac J，Nguifo E M.Towards learned clauses data- base reduction strategies based on dominance relation- ship[J].arXiv：1705.10898，2017. [20] Nabeshima H，Inoue K.Coverage- based clause reduction heuristics for CDCL solvers[C]//Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing，Melbourne，2017：136-144. [21] Pipatsrisawat K，Darwiche A.On the power of clause- learning SAT solvers as resolution engines[J].Artificial Intelligence，2011，175（2）：512-525. 计算机工程与应用www.ceaj.org

分享到：

赞收藏

资料库

论文研究-基于演绎长度的学习子句删除策略.pdf

相关推荐

开发技术

热门标签

最新资料