Sciweavers

Share
ICTAI
2009
IEEE

Learning for Dynamic Subsumption

10 years 1 months ago
Learning for Dynamic Subsumption
This paper presents an original dynamic subsumption technique for Boolean CNF formulae. It exploits simple and sufficient conditions to detect, during conflict analysis, clauses from the formula that can be reduced by subsumption. During the learnt clause derivation, and at each step of the associated resolution process, checks for backward subsumption between the current resolvent and clauses from the original formula are efficiently performed. The resulting method allows the dynamic removal of literals from the original clauses. Experimental results show that the integration of our dynamic subsumption technique within the state-of-the-art SAT solvers Minisat and Rsat particularly benefits to crafted problems.
Youssef Hamadi, Saïd Jabbour, Lakhdar Sais
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where ICTAI
Authors Youssef Hamadi, Saïd Jabbour, Lakhdar Sais
Comments (0)
books