A Hybrid Learnt Clause Evaluation Algorithm for SAT Problem

DOI

10.2991/ijcis.2018.125905645How to use a DOI?

Keywords

SAT problem; Parallel SAT solver; VSIDS; LBD; GLUCOSE

Abstract

It is of great theoretical and practical significance to develop the efficient SAT solvers due to its important applications in hardware and software verifications and so on, and learnt clauses play the crucial role in state of the art SAT solvers. In order to effectively manage learnt clauses, avoid the geometrical growth of learnt clauses, reduce the memory footprint of the redundant learnt clauses and improve the efficiency of the SAT solver eventually, learnt clauses need to be evaluated properly. The commonly used evaluation methods are based on the length of learnt clause, while short clauses are kept according to these methods. One of the current mainstream practices is the variable state independent decaying sum (VSIDS) evaluation method, the other is based on the evaluation of the literals blocks distance (LBD). There have been also some attempts to combine these two methods. The present work is focused on the hybrid evaluation algorithm by combining the trend intensity and the LBD. Based on the analysis of the frequency of learnt clauses, the trend of learnt clause being used is taken as an evaluation method which is then mixed with the LBD evaluation algorithm. The hybrid algorithm not only reflects the distribution of learnt clauses in conflict analysis, but also makes full use of literals information. The experimental comparison shows that the hybrid evaluation algorithm has advantages over the LBD evaluation algorithm in both the serial version and the parallel version of SAT solver, and the number of problems solved has significantly increased.

Copyright

© 2019 The Authors. Published by Atlantis Press SARL.

Open Access

This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)
View full text (HTML)

TY  - JOUR
AU  - Guanfeng Wu
AU  - Qingshan Chen
AU  - Yang Xu
AU  - Xingxing He
PY  - 2018
DA  - 2018/11/19
TI  - A Hybrid Learnt Clause Evaluation Algorithm for SAT Problem
JO  - International Journal of Computational Intelligence Systems
SP  - 250
EP  - 258
VL  - 12
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.2018.125905645
DO  - 10.2991/ijcis.2018.125905645
ID  - Wu2018
ER  -