Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
On Freezing and Reactivating Learnt Clauses
verfasst von : Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs
Erschienen in: Theory and Applications of Satisfiability Testing - SAT 2011
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.