Revisiting the Learned Clauses Database Reduction Strategies
  In this paper, we revisit an important issue of CDCL-based SAT solvers,
namely the learned clauses database management policies. Our motivation takes
its source from a simple observation on the remarkable performances of both
random and size-bounded reduction strategies. We first derive a simple
reduction strategy, called Size-Bounded Randomized strategy (in short SBR),
that combines maintaing short clauses (of size bounded by k), while deleting
randomly clauses of size greater than k. The resulting strategy outperform the
state-of-the-art, namely the LBD based one, on SAT instances taken from the
last SAT competition. Reinforced by the interest of keeping short clauses, we
propose several new dynamic variants, and we discuss their performances.
