Publicado em: 20/03/2014

Dissertação de Mestrado em Sistemas Embarcados

UNIVERSIDADE FEDERAL DO RIO GRANDE DO SUL
INSTITUTO DE INFORMÁTICA
PROGRAMA DE PÓS-GRADUAÇÃO EM COMPUTAÇÃO
———————————————————
DEFESA DE DISSERTAÇÃO DE MESTRADO

Aluno: Jaime Kirch da Silveira
Orientador: Prof. Dr. Luigi Carro

Título: Parallel SAT Solvers and Their Application in Automatic Parallelization.
Linha de Pesquisa: Sistemas Embarcados

Data: 28/03/2014
Hora: 15:00h
Local: Prédio 43413 – Auditório Inferior, Instituto de Informática

Banca Examinadora:
Prof. Dr. Álvaro Freitas Moreira (UFRGS)
Prof. Dr. Nicolas Bruno Maillard (UFRGS)
Prof. Dr. Rodrigo Machado (UFRGS)

Presidente da Banca: Prof. Dr. Luigi Carro

Resumo:
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, SAT-PaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.

Palavras-chave: Parallel SAT Solver, Automatic Parallelization, RePaSAT, SAT-PaDdlinG.