Minimizing learned clauses is an eective technique to reduce
memory usage and also speed up solving time. It has been implemented
in MINISAT since 2005 and is now adopted by most modern SAT solvers
in academia, even though it has not been described in the literature
properly yet. With this paper we intend to close this gap and also provide
a thorough experimental analysis of it's eectiveness for the rst time.