通过几篇重点文献来综合学习学习子句管理
【A】
Jerry Lonlac, Engelbert Mephu Nguifo:
Towards Learned Clauses Database Reduction Strategies Based on Dominance Relationship. CoRR abs/1705.10898 (2017)
【B】
- Saïd Jabbour, Jerry Lonlac, Lakhdar Saïs, Yakoub Salhi
:
Revisiting the Learned Clauses Database Reduction Strategies. Int. J. Artif. Intell. Tools 27(8): 1850033:1-1850033:19 (2018)
【C】
V. Kondratiev, I. Otpuschennikov and A. Semenov, "Using Decision Diagrams of Special Kind for Compactification of Conflict Data Bases Generated by CDCL SAT Solvers," 2020 43rd International Convention on Information, Communication and Electronic Technology (MIPRO), 2020, pp. 1046-1051, doi: 10.23919/MIPRO48935.2020.9245180.
C文没有讲管理学习子句库，讲的是如何编码存储海量的冲突形成的子句库。
1.学习子句管理的重要性
2.主要的技术方法
| 1 |
译文：Minisat[11]认为近期冲突分析中涉及最多的条款是相关的，删除了近期冲突分析中涉及较少的学习条款。 11. Niklas E´en and Niklas S¨orensson. An extensible sat-solver. In SAT 2003, pages 502–518, 2003. |
| 2 |
LBD方案 Literal Block Distance was proposed in [2]. LBD based measure is also exploited by most of the best state-of-the-art SAT solver (Glucose, Lingeling [6]) and whose efficiency has been proved empirically. LBD based measure uses the number of different levels involved in a given learned clause to quantify the quality of the learned clauses. 译文：基于LBD的测量方法使用给定的学习子句中所涉及的不同层次的数量来量化学习子句的质量。 Hence, the clauses with smaller LBD are considered as more relevant. |
| 3 |
冻结与激活策略 In [3], a new dynamic management policy of the learned clauses database is proposed. It is based on a dynamic freezing and activation principle of the learned clauses. At a given search state, using a relevant selection function based on progress saving (PSM), it activates the most promising learned clauses while freezing irrelevant ones.译文：在[3]中，提出了一种新的学习子句数据库动态管理策略。它是基于对所学分句的动态冻结和激活原则。在给定的搜索状态下，使用基于进度保存(PSM)的相关选择功能，它会激活最有希望的学习条目，而冻结不相关的条目。 |
| 4 | BTL In [14], a new criterion to quantify the relevance of a clause using its backtrack level called BTL for BackTrack Level was proposed. From experiments, the authors observed that the learned clauses with small BTL values are used more often in the unit propagation process than those with higher BTL values. 译文：通过实验，作者发现，学习后BTL值小的子句在单元传播过程中的使用频率高于BTL值高的子句。 More precisely, the authors observed that the learned clauses with BTL value less than 3 are always used much more than the remaining clauses. 译文：更准确地说，作者观察到，学习后BTL值小于3的子句总是比其余子句使用得更多。 Starting from this observation, and motivated by the fact that a learned clause with smaller BTL contains more literals from the top of the search tree, the authors deduce that relevant clauses are those allowing a higher backtracking in the search tree (having small BTL value). 译文：从这一观察出发，并考虑到具有较小BTL的学习子句包含来自搜索树顶部的更多字面量，作者推断相关子句是那些允许在搜索树中进行更高回溯的子句(具有较小的BTL值)。 译文：从这一观察出发，并考虑到具有较小BTL的学习子句包含来自搜索树顶部的更多字面量，作者推断相关子句是那些允许在搜索树中进行更高回溯的子句(具有较小的BTL值)。 |
| 5 | 规模限制学习策略--学习子句的长度指标？ In [15], the authors explore a number of variations of learned clause database reduction strategies, and the performance of the difffferent extensions of Minisat solver integrating their strategies is evaluated on the instances of the SAT competitions 2013/2014 and compared against other state-of-the-art SAT solvers (Glucose, Lingeling) as well as against default Minisat. From the performances obtained in [15], the authors have shown that size-bounded learning strategies proposed more than fifteenth years ago [19, 4, 5] is not over and remains a good measure to predict the quality of learned clauses. 译文：从[15]中获得的成绩来看，作者已经表明，超过15年前[19,4,5]提出的规模限制学习策略并没有结束，仍然是预测学习子句质量的一个很好的方法。 They show that adding randomization to size bounded learning is a nice way to achieve controlled diversifification, allows to favor the short clauses, while maintaining a small fraction of large clauses necessary for deriving resolution proofs on some SAT instances. 译文：他们表明，在规模有限的学习中加入随机化是实现可控多样化的一个好方法，允许支持短的条款，同时保留在一些SAT实例中导出分辨率证明所必需的大条款的一小部分。 This study opens many discussions about the learned clauses database strategies and raises questions about the effectiveness proclaimed by other strategies of the state-of-the-art [11, 2]. |
| 6 |
社区结构识别对应有用的学习子句 In [1], the authors use the community structure of industrial SAT instances to identify a set of highly useful learned clauses. They show that augmenting a SAT instance with the clauses learned by the solver during its execution does not always mean to make the instance easy. 译文：他们表明，用求解器在执行过程中学习到的子句来扩充SAT实例并不总是意味着使实例变得容易。 However, the authors show that augmenting the formula with a set of clauses based on the community structure of the formula improves the performance of the solver in many cases. 译文：然而，作者表明，在公式的社区结构的基础上，用一组子句来扩充公式，可以在许多情况下提高求解器的性能。 |
| The different performances obtained by each strategy suggests that the question on how to predict efficiently the ”best” learned clauses is still open and deserves further investigation. 每种策略所获得的不同性能表明如何有效地预测 “最佳”学习条款仍然是开放的，值得进一步研究。 | |
| 7 |
多种学习条款的相关度量都可以整合到支配关系中---相关度量之间的支配关系是获取每个度量收益的一种很好的方法。 下面蓝色标出文献[A]给出的一种信息的策略:在解决过程中确定相关的学习条款，而不偏向于任何最好的报告相关措施，并释放每次需要删除的条款数量
译文：这是首次将优势关系应用于可满足域来提高CDCL SAT求解器的性能。 【A】Jerry Lonlac, Engelbert Mephu Nguifo |
3. 管理落实频率与力度
| 1 | On the other hand, it is important to note that the effiffifficiency of most of these state-of-the-art learned clauses management strategies heavily depends on the cleaning frequency and on the amount of clauses to be deleted each time. 译文：另一方面，重要的是要注意到，大多数这些最先进的学习条款管理策略的效率在很大程度上取决于清洗频率和每次删除的条款数量。 |
| 2 |
文献 Jerry Lonlac, Engelbert Mephu Nguifo 译文： 该方法避免了另一个重要问题，即学习子句数据库在每一步约简时需要删除的学习子句数量。 |
| Generally, all the CDCL SAT solvers using these strategies exactly delete half of the learned clauses at each learned clauses database reduction step. 译文：一般来说，所有使用这些策略的CDCL SAT解算器在每个学习子句数据库约简步骤中都准确地删除了一半的学习子句。 For example, the CDCL SAT solver Minisat [11] and Glucose [2] delete half of the learned clauses at each cleaning. Therefore, the efficiency of this amount of learned clauses to delete (e.g the half) at each cleaning step of the learned clauses database has not been demonstrated theoretically, but instead experimentally. 译文：因此，在学习子句数据库的每个清理步骤中，这种数量的学习子句删除(例如一半)的效率并没有在理论上得到证明，而是在实验中得到证明。 For our knowledge, there are not many studies in the literature on how to determine the amount of clauses to be deleted each time. | |
| This paper proposes an approach to identify the relevant learned clauses during the resolution process without favoringany of the best reported relevant measures and which frees itself of the amount of clauses to be removed at each time: the amount of learned clauses to delete corresponds at each time to the number of learned clauses dominated by one particular learned clause of the set of the current learned clauses which is called in the following sections, the reference learned clause. 译文：本文提出了一种方法，在解决过程中确定相关的学习条款，而不偏向于任何最好的报告相关措施，并释放每次需要删除的条款数量: 译文：每次需要删除的学习子句的数量对应于当前学习子句集合中由一个特定的学习子句支配的学习子句的数量，这一集合在下文中称为参考学习子句。 | |
| 译文：由于对学习的子句的评价因测量的不同而不同，使用几种测量方法可能导致不同的输出(与测量相关的子句)。 Since the evaluation of learned clauses varies from a measure to another one, using several measures could lead to difffferent outputs (relevant clauses with respect to a measure). | |
| This difffference of evaluations is confusing for any process of learned clauses selection. Hence, we can utilize the notion of dominance between learned clauses to address the selection of relevant ones. Before, formulating the dominance relationship between learned clauses, we need to defifine it at the level of measure values. To do that, we defifine dominance value as follows: 译文：这种评价的差异对于任何学习的子句选择过程都是令人困惑的。因此，我们可以利用学习分句间的优势概念来解决相关分句的选择问题。在此之前，我们需要在度量值的水平上定义学习过的子句之间的支配关系。为此，我们将主导价值定义如下: | |