Learning polynomials over GF(2) in a SAT solver (Poster presentation)

Abstract

One potential direction for improving the performance of SAT solvers is by using a stronger underlying proof system, e.g., [1].We propose a step in improving the learning architecture of SAT solvers and describe a learning scheme in the polynomial calculus with resolution (PCR), a proof system that generalizes both resolution and Gaussian elimination. The scheme fits the general structure of CDCL solvers, so many of the other techniques of CDCL solvers should be reusable. © 2012 Springer-Verlag.