International Journal of Computational Intelligence Systems

<Previous Article In Issue
Next Article In Issue>
Volume 10, Issue 1, 2017, Pages 824 - 834

A Logical Deduction Based Clause Learning Algorithm for Boolean Satisfiability Problems

Authors
Qingshan Chen1, *, qschen@home.swjtu.edu.cn, Yang Xu2, xuyang@home.swjtu.edu.cn, Jun Liu3, j.liu@ulster.ac.uk, Xingxing He2, x.he@home.swjtu.edu.cn
1School of Information Science and Technology, Southwest Jiaotong University, Chengdu, Sichuan 610031, China
2National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu, Sichuan 610031, China
3School of Computing and Mathematics, University of Ulster, Northern Ireland, UK
*Corresponding author
Corresponding Author
Received 9 February 2017, Accepted 17 March 2017, Available Online 3 April 2017.
DOI
10.2991/ijcis.2017.10.1.55How to use a DOI?
Keywords
Boolean Satisfiability; SAT Problem; Clause Learning; Logical Deduction; Implication Graph
Abstract

Clause learning is the key component of modern SAT solvers, while conflict analysis based on the implication graph is the mainstream technology to generate the learnt clauses. Whenever a clause in the clause database is falsified by the current variable assignments, the SAT solver will try to analyze the reason by using different cuts (i.e., the Unique Implication Points) on the implication graph. Those schemes reflect only the conflict on the current search subspace, does not reflect the inherent conflict directly involved in the rest space. In this paper, we propose a new advanced clause learning algorithm based on the conflict analysis and the logical deduction, which reconstructs a linear logical deduction by analyzing the relationship of different decision variables between the backjumping level and the current decision level. The logical deduction result is then added into the clause database as a newly learnt clause. The resulting implementation in Minisat improves the state-of-the-art performance in SAT solving.

Copyright
© 2017, the Authors. Published by Atlantis Press.
Open Access
This is an open access article under the CC BY-NC license (http://creativecommons.org/licences/by-nc/4.0/).

Download article (PDF)
View full text (HTML)

<Previous Article In Issue
Next Article In Issue>
Journal
International Journal of Computational Intelligence Systems
Volume-Issue
10 - 1
Pages
824 - 834
Publication Date
2017/04/03
ISSN (Online)
1875-6883
ISSN (Print)
1875-6891
DOI
10.2991/ijcis.2017.10.1.55How to use a DOI?
Copyright
© 2017, the Authors. Published by Atlantis Press.
Open Access
This is an open access article under the CC BY-NC license (http://creativecommons.org/licences/by-nc/4.0/).

Cite this article

risenwbib
TY  - JOUR
AU  - Qingshan Chen
AU  - Yang Xu
AU  - Jun Liu
AU  - Xingxing He
PY  - 2017
DA  - 2017/04/03
TI  - A Logical Deduction Based Clause Learning Algorithm for Boolean Satisfiability Problems
JO  - International Journal of Computational Intelligence Systems
SP  - 824
EP  - 834
VL  - 10
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.2017.10.1.55
DO  - 10.2991/ijcis.2017.10.1.55
ID  - Chen2017
ER  -