Open AccessAn Effective Sharpsat Solution Method Based on Learnt Clause Minimization Approach
Author(s) -
Xi Chen,
Weikang Du,
Yingjie Xu,
Mingdian Ma
Publication year - 2020
Publication title -
iop conference series. earth and environmental science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.179
H-Index - 26
eISSN - 1755-1307
pISSN - 1755-1315
DOI - 10.1088/1755-1315/440/3/032143
Subject(s) - boolean satisfiability problem , solver , satisfiability , propositional calculus , computer science , literal (mathematical logic) , constraint satisfaction problem , conjunctive normal form , constraint (computer aided design) , constraint learning , boolean data type , maximum satisfiability problem , minification , mathematical optimization , algorithm , theoretical computer science , mathematics , artificial intelligence , local consistency , boolean function , programming language , geometry , probabilistic logic
The problem of satisfiability of the propositional logic formula (SAT problem) in computer science is an important and difficult problem. Learning clauses often contain redundant literal in CDCL SAT solving, which may have a negative impact on the performance of the solver. To overcome this shortcoming, we show a new sharpSAT solver based on learning clause minimization is proposed. By recoding the CNF formula to reduce the storage space, and applying Boolean constraint propagation to eliminate redundant literals in the learning clause, the algorithm reduces the time cost. The complexity is compared with the existing solver. The experimental results show that the solver has significant application value, reduces the time of instance solution, and increases the number of maximum solvable instances.