Parallel SAT solvers and their application in automatic parallelization
Universidade Federal do Rio Grande do Sul, Instituto de Informatica
Universidade Federal do Rio Grande do Sul, 2014
@article{silveira2014parallel,
title={Parallel SAT solvers and their application in automatic parallelization},
author={Silveira, Jaime Kirch da},
year={2014}
}
Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.
May 31, 2014 by hgpu