Too much information: why CDCL solvers need to forget learned clauses

Tom Krüger, Jan-Hendrik Lorenz, Florian Wörz

Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. Instead of a simple depth-first backtracki…