faster search
Adding New Bi-Asserting Clauses for Faster Search in Modern SAT Solvers
Jabbour, Saïd (CRIL, Université d'Artois - CNRS) | Lonlac, Jerry (CRIL, Université d'Artois - CNRS) | Saïs, Lakhdar (CRIL, Université d'Artois - CNRS)
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.