Looking Inside Literal Blocks: Towards Mining More Promising Learnt Clauses in SAT Solving

摘要

Literal Block Distance (LBD) is the criterion to evaluate the quality of learnt clauses and is used as a standard technique to reserve important ones in the reduction phase of state-of-the-art SAT solvers. A LBD of a clause can be updated (decreased) during the search when it is re-evaluated at the Boolean constraint propagation phase. The update is essential to evaluate the real LBD value of a learnt clause and to enhance the solver performance. We are interested in what kind of clause tends to be updated, and we conduct a survey for them by using statistical tests. The results indicate that features of literal blocks affect the update of LBD. Moreover, we utilize the fact to save more promising learnt clauses in the reduction phase of them, and we improve the performance of the solver.