Modern SAT solvers frequently reduce the size of their learned clause database in order to keep its size as manageable as possible. This has as effect not to slow down the speed of unit propagations.
I think that in addition to keep reasonable the size of the learned clause database, the reduction also helps to improve diversification which increases the chance of the solver to rapidly find a solution for satisfiable formulas. I also think that restarts don't help enough to increase diversification in the solver since upon restart all learned clauses are kept as well as variable activities and polarities. For myself these information contribute to redirect the search in the same search space.
can the reduction of the learned clause database in CDCL SAT solvers be seen as a way to increase diversification ? By diversification, I mean a reasonable coverage of the search space.