<p>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. </p>

<p>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.</p>

<p>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.</p>

CC BY-SA 4.0
2018-09-12T00:07:50.733Z
Maybe you could try to define more precisely what you mean by diversification?
Markus
CC BY-SA 4.0
2018-09-12T05:36:41.030Z
by diversification, I mean a reasonable coverage of the search space.
RTK
<ds.algorithms><sat><heuristics>
On the goal of learned clause database reduction in CDCL SAT solvers
RTK
# On the goal of learned clause database reduction in CDCL SAT solvers

(Asked by: username_0 on 2018-09-10)

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.

**Tags:** ds.algorithms, sat, heuristics
> **Comments:**
> **username_1**: Maybe you could try to define more precisely what you mean by diversification?  
> **username_0**: by diversification, I mean a reasonable coverage of the search space.  

---

## 0 answers

