Extended Resolution in Modern SAT Solving

ABSTRACT. Modern SAT solvers are applied in many academic and industrial fields. The used CDCL algorithm is based on resolution, but solvers also use stronger reasoning techniques in preprocessing steps. Only few attempts have been made to include stronger reasoning techniques into the search itself. The current work revisits the embedding of extended resolution into SAT solvers, and improves existing work. Experiments indicate that the approach is very promising.