As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Conflict-driven clause learning (CDCL) is well-known to be the predominant SAT solving approach. Its main idea consists in using conflict clauses to guide the effective traversal of the complete search space. Despite the undoubted usefulness of this powerful mechanism, a CDCL solver may end up computing (exponentially) many conflict clauses. To resolve this issue, a number of efficient heuristics exist aiming at aggressive conflict clause filtering, which leads to some of the clauses being removed. Thus, when processing a particular instance, a solver may learn and remove the same clause multiple times. One might see it as an indication that such relearned clauses pose extra value. In the paper we show that extracting duplicate clauses and storing them indefinitely can be beneficial for the CDCL solver performance which is indicated by the fact that the family of solvers incorporating the corresponding heuristic won in the UNSAT and SAT+UNSAT tracks of the SAT Race 2019. We perform the detailed experimental evaluation of this heuristic on the instances from the SAT Competitions 2017 and 2018, and also SAT Race 2019 and show that it improves both PAR-2 and SCR scores.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.