On Freezing and Reactivating Learnt Clauses
On Freezing and Reactivating Learnt Clauses
复制标题
关于冻结和重新激活习得子句
DOI：
10.1007/978-3-642-21581-0_16
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
L. Sais
中科院分区：
文献类型：
--
作者：
Gilles Audemard;Jean;Bertrand Mazure;L. Sais
在本文中，我们提出了一种新的动态管理策略的学习子句数据库在现代求解器。它是基于一个动态的冻结和激活原则的学习子句。在给定的搜索状态下，使用相关选择函数，它激活最有前途的学习子句，同时冻结不相关的。通过这种方式，在先前步骤中学习的子句可以在当前步骤中冻结，并且可以在搜索过程的未来步骤中再次激活。我们的策略试图利用从过去收集的信息来推断剩余搜索步骤中给定子句的相关性。这个策略与所有众所周知的删除策略形成对比，在这些策略中，一个给定的学习子句肯定会被删除。在最后一次比赛中的实例上的实验证明了我们所提出的方法的有效性。
In this paper, we propose a new dynamic management policy of the learnt clause database in modernsatsolvers. It is based on a dynamic freezing and activation principle of the learnt clauses. At a given search state, using a relevant selection function, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, clauses learned at previous steps can be frozen at the current step and might be activated again in future steps of the search process. Our strategy tries to exploit pieces of information gathered from the past to deduce the relevance of a given clause for the remaining search steps. This policy contrasts with all the well-known deletion strategies, where a given learned clause is definitely eliminated. Experiments onsatinstances taken from the last competitions demonstrate the efficiency of our proposed technique.