Learning for Dynamic Assignments Reordering

10 years 1 months ago
Learning for Dynamic Assignments Reordering
In this paper a new learning scheme for SAT is proposed. The originality of our approach arises from its ability to achieve clause learning even if no conflict occurs. This clearly contrasts with all the traditional learning approaches which generally refer to conflict analysis. To make such learning possible, relevant clauses, taken from the satisfied part of the formula are conjointly used with the classical implication graph to derive new and more powerful reasons for the implication of a given literal. Based on this extension a first learning scheme called Learning for Dynamic Assignments Reordering (LDAR) is proposed. It exploits the new derived reasons to dynamically reorder partial assignments. Experimental results show that the integration of LDAR within a state-of-the-art SAT solver achieves interesting improvements particularly on satisfiable instances.
Saïd Jabbour
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Authors Saïd Jabbour
Comments (0)