The parallel computing power offered by graphic processing units (GPUs) has been recently exploited to support general purpose applications - by exploiting the availability of general API and the single-instruction multiple-thread-style parallelism present in several classes of problems (e.g. numerical simulations and matrix manipulations) - where relatively simple computations need to be applied to all items in large sets of data. This paper investigates the use of GPUs in parallelising a class of search problems, where the combinatorial nature leads to large parallel tasks and relatively less natural symmetries. Specifically, the investigation focuses on the well-known satisfiability testing (SAT) problem and on the use of the NVIDIA compute unified device architecture, one of the most popular platforms for GPU computing. The paper explores ways to identify strong sources of GPU-style parallelism from SAT solving. The paper describes experiments with different design choices and evaluates the results. The outcomes demonstrate the potential for this approach, leading to one order of magnitude of speedup using a simple NVIDIA platform.

CUD@SAT: SAT solving on GPUs / DAL PALU', Alessandro; Dovier, Agostino; Formisano, Andrea; Pontelli, Enrico. - In: JOURNAL OF EXPERIMENTAL & THEORETICAL ARTIFICIAL INTELLIGENCE. - ISSN 0952-813X. - 27:3(2015), pp. 293-316. [10.1080/0952813X.2014.954274]

CUD@SAT: SAT solving on GPUs

DAL PALU', Alessandro;
2015-01-01

Abstract

The parallel computing power offered by graphic processing units (GPUs) has been recently exploited to support general purpose applications - by exploiting the availability of general API and the single-instruction multiple-thread-style parallelism present in several classes of problems (e.g. numerical simulations and matrix manipulations) - where relatively simple computations need to be applied to all items in large sets of data. This paper investigates the use of GPUs in parallelising a class of search problems, where the combinatorial nature leads to large parallel tasks and relatively less natural symmetries. Specifically, the investigation focuses on the well-known satisfiability testing (SAT) problem and on the use of the NVIDIA compute unified device architecture, one of the most popular platforms for GPU computing. The paper explores ways to identify strong sources of GPU-style parallelism from SAT solving. The paper describes experiments with different design choices and evaluates the results. The outcomes demonstrate the potential for this approach, leading to one order of magnitude of speedup using a simple NVIDIA platform.
2015
CUD@SAT: SAT solving on GPUs / DAL PALU', Alessandro; Dovier, Agostino; Formisano, Andrea; Pontelli, Enrico. - In: JOURNAL OF EXPERIMENTAL & THEORETICAL ARTIFICIAL INTELLIGENCE. - ISSN 0952-813X. - 27:3(2015), pp. 293-316. [10.1080/0952813X.2014.954274]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2815931
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 42
  • ???jsp.display-item.citation.isi??? 24
social impact