AAAI Publications, Tenth Symposium of Abstraction, Reformulation, and Approximation

Font Size: 
Adding New Bi-Asserting Clauses for Faster Search in Modern SAT Solvers
Saïd Jabbour, Jerry Lonlac, Lakhdar Saïs

Last modified: 2013-06-19

Abstract


In this paper, a new approach for clauses learning is proposed. By traversing the implication graph sepa- rately from x and ¬x, we derive a new class of bi-asserting clauses that can lead to a more compact implication graph. These new kinds of bi-asserting clauses are much shorter and tend to induce more implications than the classical bi-asserting clauses. Experimental results show that exploiting this new class of bi-asserting clauses improves the performance of state-of-the-art SAT solvers particularly on crafted instances.

Full Text: PDF