标签：删除 计算方法 关系 ued col OWIN removing 特定 zed
参考文献：
1. Gilles Audemard，Laurent Simon: On the Glucose SAT Solver
一、对学习自己作用的认识
The first answer was just abouttrying to contain the combinatorial explosion by simply periodically cleaning the learnt clause database.this was essentially to try to make sufficient room for new learnt clauses by removing unused previouslylearnt clause. Indeed, keeping too many learnt clauses slows down the unit propagation process, while deleting too many of them breaks the overall learning benefit.
A CDCL-based SAT solver can be formulated as a resolution proof system.[48,11]. Consequently, the practical incarnation of modern SAT solvers can be seen as a clauses producer procedure with a deletion strategy.译文：一个基于cdcl的SAT求解器可以被表述为一个解决证明系统。48,11.因此，现代SAT求解器的实际体现可以被视为具有删除策略的子句生成程序。
在完成证明之前确定什么是有用的子句并不简单， (Occurring on the proof for UNSAT? Forcing a value for SAT?)。
学习子句的作用在SAT和UNSAT问题求解中是否有用的定义不同的。对于UNSAT问题样例，求解期间生产的学习子句有一半左右是没有用的，是指不会出现在最后UNSAT的最后证明中。对于SAT问题求解，学习子句的是否有用需要专门的定义。For SAT instances, the role of learnt clauses is to conduct the solver on some particular search space, and also, probably, to explicit some dependencies between variable assignments.译文：对于SAT实例，学习子句的作用是在某些特定的搜索空间上执行求解程序，并且可能还会明确变量分配之间的某些依赖关系。
This being said, the crucial questions remain: what are the good clauses to learn? How to identify them during the search? if one is able to determine good clauses, then, one can often remove useless ones.
二、早期对学习子句管理的基本方法
In the early years of CDCL, the importance of clause deletion strategies was not clearly identified as one of their essential components. The aim was just to help the solver managing too many clauses.
Nevertheless, a few proposal were made. In Ref. 36, authors proposed the idea of bounding the size of learnt clauses, keeping only clauses smaller than a certain threshold. The authors of Berkmin25 considered that recent clauses were better than older ones. They used a FIFO to remove old clauses while keeping in memory short clauses (smaller than 8). In Chaff, 41 a clause was marked to be deleted when a certain number of literals became unassigned (between 100 and 200). In Minisat, 21 learnt clauses are deleted based on an activity heuristic. Each time a clause is used in conflict analysis, its activity is increased. Then, periodically, half of the clauses are deleted (the ones with small activities). This technique is very interesting, because it also deletes without additional cost subsumed learnt clauses (they will never be used in the future, then their activity will always decrease).
三、 The Literal Block Distance (LBD) measure —— glucose 首先提出的子句质量评价方法
1.glucose求解器的重大创新——子句LBD属性提出的背景和意义
We noticed that, for most of the instances, the number of decisions made before reaching a conflict globally decreases during the search.5 译文：我们注意到，在大多数情况下，在搜索过程中，在达成全球性冲突之前做出的决策数量减少了，传播文字增多了。This can be seen as a natural phenomenon for unsatisfiable instances (thanks to learning), but it was somehow surprising to observe this phenomenon also on satisfiable ones.译文：对于无法满足的情况，这可以看作是一种自然现象. 译文：但令人惊讶的是，这种现象也出现在可满足的人身上。
Each decision can potentially create a lot of propagated literals (what we call blocks), especially in the deepest parts of the search tree. 译文：每个决策都可能潜在地创建大量传播的文字(我们称之为块)，特别是在搜索树的最深处. 译文：每个决策都可能潜在地创建大量传播的文字(我们称之为块)，特别是在搜索树的最深处. Then, if we want to reduce the number of decisions, we need to add dependencies between independent blocks, and, then, to add the strongest possible constraints between them.译文：然后，如果我们想减少决策的数量，我们需要在独立块之间添加依赖关系，然后在它们之间添加可能的最强约束。This observation is at the origin of our measure LBD (Literal Block Distance), formalized in the following.
Intuitively, it is easy to understand the importance of learnt clauses of LBD 2: they only contain one variable of the last decision level (they are FUIP), and, later, this variable will be “glued” with the block of literals propagated above, no matter the size of the clause.LBD值为2的学习子句中只包含最后一个决策级别的一个变量，不管子句的大小，这个变量将与之前所传播的文字块“粘合”在一起。译文：我们猜想所有这些LBD值比较小的学习子句在搜索过程中都非常重要，我们给它们起了一个特殊的名字:“粘合子句”。
自glucose于2007年提出以来，lbd评价学习子句质量被证明是求解器发展非常重大的革新。该方法提出的主要发端是基于大量实验发现，如果我们想减少决策的数量，我们需要在独立块之间添加依赖关系，然后在它们之间添加可能的最强约束。
2.LBD子句的计算方法
lbd值为学习子句联系文字块的个数。
考虑: 为什么core中一些学习子句的LBD较小，但后续被使用并不比tier2中的某些子句更多？core中为什么也是少数学习子句被大量使用？与多次陷入局部靠重启跳出有关吗？
标签：删除 计算方法 关系 ued col OWIN removing 特定 zed
原文地址：https://www.cnblogs.com/yuweng1689/p/13064743.html
