International Journal of Computational Intelligence Systems

Volume 12, Issue 1, November 2018, Pages 250 - 258

A Hybrid Learnt Clause Evaluation Algorithm for SAT Problem

Authors
Guanfeng Wu1, 2, *, Qingshan Chen1, 2, Yang Xu2, Xingxing He2
1School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China
2National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China
*

Corresponding author. Email: wl520gx@gmail.com

Received 20 October 2018, Revised 30 October 2018, Accepted 4 November 2018, Available Online 19 November 2018.
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)

Journal
International Journal of Computational Intelligence Systems
Volume-Issue
12 - 1
Pages
250 - 258
Publication Date
2018/11/19
ISSN (Online)
1875-6883
ISSN (Print)
1875-6891
DOI
10.2991/ijcis.2018.125905645How to use a DOI?
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/).

Cite this article

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  -