Parallelization of SAT Algorithms on GPU EVALUATED

Detalhes: O Problema de Satisfação Booleana (SAT) é um problema NP-Completo muito importante. No entanto, recentemente, a performance dos SAT solvers tem vindo a abrandar, o que levou à realização de trabalho na área da paralelização de SAT solvers para que estes pudessem tirar partido de sistemas multi-core. Entretanto, os GPUs deixaram de servir apenas para processamento gráfico, para passarem a servir para fazer qualquer tipo de processamento. Apesar disso, só recentemente é que começou a haver trabalho no sentido de se utilizar GPUs para resolver SAT. No entanto, as técnicas aplicadas não utilizam todo o potencial do GPU e por isso, limitam a sua aplicabilidade. Isto acontece porque estes trabalhos utilizam a escalabilidade do GPU para conseguirem acomodar problemas cada vez maiores, no entanto, quando os problemas atingem um certo tamanho, o GPU deixa de conseguir processá-lo da melhor forma. Nesta tese apresentamos uma nova abordagem à utilização do GPU, que, pelo facto de escolhermos cuidadosamente o trabalho que este tem que fazer, permite ao GPU conseguir fazer com poucos recursos, o que em outras abordagens só seria possível com todo o GPU. Esta abordagem permite-nos ter um portfolio de procura, que consegue escalar melhor e permite ao GPU resolver problemas de qualquer tamanho, o que não era possível anteriormente.

Discussão: junho 3, 2014, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

AUTOR

Carlos Filipe da Silva Portinha e Costa (ist158403)

CO-ORIENTADOR

Paulo Ferreira Godinho Flores

Departamento de Engenharia Electrotécnica e de Computadores (DEEC)

Professor Auxiliar

ORIENTADOR

Luís Jorge Brás Monteiro Guerra e Silva

Departamento de Engenharia Informática (DEI)

Professor Auxiliar