Loading…
Performance Evaluation of Parallel SAT Solver on Xeon Phi Processor
The satisfiability (SAT) problem is widely applicable to various industrial problems, such as formal verification of industrial systems. This study presents the performance evaluation of a parallel SAT solver (Glucose Syrup) on Intel Xeon Phi many-core processors. After limiting the number of learnt...
Saved in:
Published in: | Denki Gakkai ronbunshi. D, Sangyō ōyō bumonshi 2019/02/01, Vol.139(2), pp.119-126 |
---|---|
Main Authors: | , , |
Format: | Article |
Language: | eng ; jpn |
Subjects: | |
Citations: | Items that this one cites |
Online Access: | Get full text |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Summary: | The satisfiability (SAT) problem is widely applicable to various industrial problems, such as formal verification of industrial systems. This study presents the performance evaluation of a parallel SAT solver (Glucose Syrup) on Intel Xeon Phi many-core processors. After limiting the number of learnt clauses to be shared, the number of solved problems in the SAT Competition 2016 workload increased from 201 to 236, yet it was smaller than that of a Xeon processor. |
---|---|
ISSN: | 0913-6339 2187-1094 1348-8163 2187-1108 |
DOI: | 10.1541/ieejias.139.119 |