کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6901811 | 1446496 | 2017 | 9 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A parallel SAT solving algorithm based on improved handling of conflict clauses
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
علوم کامپیوتر (عمومی)
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
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
Journal: Procedia Computer Science - Volume 119, 2017, Pages 103-111
نویسندگان
Oleg Zaikin,