2009 21st IEEE International Conference on Tools with Artificial Intelligence (2009)
Newark, New Jersey
Nov. 2, 2009 to Nov. 4, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICTAI.2009.22
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.
Constraint Programming, Satisfiablity
L. Saïs, Y. Hamadi and S. Jabbour, "Learning for Dynamic Subsumption," 2009 21st IEEE International Conference on Tools with Artificial Intelligence(ICTAI), Newark, New Jersey, 2009, pp. 328-335.