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...

Full description

Saved in:
Bibliographic Details
Published in:Denki Gakkai ronbunshi. D, Sangyō ōyō bumonshi 2019/02/01, Vol.139(2), pp.119-126
Main Authors: Nishiwaki, Shintaro, Fujieda, Naoki, Ichikawa, Shuichi
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!
Description
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