In [3], SAT conflict analysis graphs were used to learn additional clauses, which we refer to as back-clauses. These clauses may be viewed as enabling the powerful notion of "probing": Back-clauses make inferences that would normally have to be deduced by setting a variable deliberately the other way and observing that unit propagation leads to a conflict. We show that short-cutting this process can in fact improve the performance of modern SAT solvers in theory and in practice. Based on out numerical results, it is suprising that back-clauses, proposed over a decade ago, are not yet part of standard clause-learning SAT solvers. © 2012 Springer-Verlag.
CITATION STYLE
Sabharwal, A., Samulowitz, H., & Sellmann, M. (2012). Learning back-clauses in SAT (Poster presentation). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 498–499). https://doi.org/10.1007/978-3-642-31612-8_53
Mendeley helps you to discover research relevant for your work.