In this paper, we propose a new dynamic management policy of the learnt clause database in modern sat solvers. 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 on sat instances taken from the last competitions demonstrate the efficiency of our proposed technique. © 2011 Springer-Verlag.
CITATION STYLE
Audemard, G., Lagniez, J. M., Mazure, B., & Saïs, L. (2011). On freezing and reactivating learnt clauses. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6695 LNCS, pp. 188–200). https://doi.org/10.1007/978-3-642-21581-0_16
Mendeley helps you to discover research relevant for your work.