Towards Learned Clauses Database Reduction Strategies Based on Dominance
  Relationship
  Clause Learning is one of the most important components of a conflict driven
clause learning (CDCL) SAT solver that is effective on industrial instances.
Since the number of learned clauses is proved to be exponential in the worse
case, it is necessary to identify the most relevant clauses to maintain and
delete the irrelevant ones. As reported in the literature, several learned
clauses deletion strategies have been proposed. However the diversity in both
the number of clauses to be removed at each step of reduction and the results
obtained with each strategy creates confusion to determine which criterion is
better. Thus, the problem to select which learned clauses are to be removed
during the search step remains very challenging. In this paper, we propose a
novel approach to identify the most relevant learned clauses without favoring
or excluding any of the proposed measures, but by adopting the notion of
dominance relationship among those measures. Our approach bypasses the problem
of the diversity of results and reaches a compromise between the assessments of
these measures. Furthermore, the proposed approach also avoids another
non-trivial problem which is the amount of clauses to be deleted at each
reduction of the learned clause database.
