Accelerating a continuous-time analog SAT solver using GPUs

Recently, a continuous-time, deterministic analog solver based on ordinary differential equations (CTDS) was introduced, to solve Boolean satisfiability (SAT), a family of discrete constraint satisfaction problems. Since SAT is NP-complete, efficient algorithms would benefit solving a large number o...

Full description

Saved in:
Bibliographic Details
Published in:Computer physics communications 2020-11, Vol.256, p.107469, Article 107469
Main Authors: Molnár, Ferenc, Kharel, Shubha R., Hu, Xiaobo Sharon, Toroczkai, Zoltán
Format: Article
Language:English
Subjects:
Boolean satisfiability
Continuous-time algorithm
GPU acceleration
NP-complete
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Recently, a continuous-time, deterministic analog solver based on ordinary differential equations (CTDS) was introduced, to solve Boolean satisfiability (SAT), a family of discrete constraint satisfaction problems. Since SAT is NP-complete, efficient algorithms would benefit solving a large number of decision type problems, both within industry and the sciences. Here we present a graphics processing units (GPU) based implementation of the CTDS and its variants and show that one can achieve significantly improved performance within a wide range of SAT problems. We present and discuss three versions of our GPU implementation and compare their performance to CPU implementations, showing an improvement factor of up to two orders of magnitude. We illustrate the performance of our GPU-based solver on random SAT problems and a notoriously difficult graph coloring problem, the Ramsey number problem R(3,3,3,3), and compare it with the state-of-the-art SAT solver MiniSAT’s performances on CPUs.
ISSN:0010-4655
1879-2944
DOI:10.1016/j.cpc.2020.107469