2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Maybe you could try to define more precisely what you mean by diversification? $\endgroup$ – Markus Sep 12 '18 at 0:07
  • $\begingroup$ by diversification, I mean a reasonable coverage of the search space. $\endgroup$ – RTK Sep 12 '18 at 5:36

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.