کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6901811 1446496 2017 9 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A parallel SAT solving algorithm based on improved handling of conflict clauses
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر علوم کامپیوتر (عمومی)
پیش نمایش صفحه اول مقاله
A parallel SAT solving algorithm based on improved handling of conflict clauses
چکیده انگلیسی
In this study, a new parallel algorithm for solving Boolean satisfiability problem (SAT) is suggested. This algorithm is based on the Conflict Driven Clause Learning (CDCL) algorithm. Given an original SAT instance, CDCL is launched on it. Some types of conflict clauses, which are produced by CDCL, are collected. Then the collected clauses are employed to construct a family of different SAT instances. In particular, each SAT instance from a family is produced by adding some subset of the collected conflict clauses to an initial set of clauses (which belong to the original instance). In order to solve the original SAT instance, it is sufficient to solve at least one SAT instance from the constructed family. The proposed algorithm was implemented in the form of a parallel SAT solver. It was compared with two high ranked state-of-the-art parallel solvers. As a test set, we used SAT instances which encode cryptanalysis of three keystream generators: summation generator, threshold generator, and Gifford generator. According to computational experiments, our solver outperforms those two solvers.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Procedia Computer Science - Volume 119, 2017, Pages 103-111
نویسندگان
,