Dissertação

Algorithms for Maximum Satisfiability using GPU EVALUATED

O interesse em algoritmos para resolver Maximum Satisfiability (MaxSAT) tem vindo a aumentar de forma elevada nos últimos anos. Contudo, parece existir uma grande falta de uso do poder disponível nos GPUs. Neste trabalho apresentamos uma proposta para utilizar o GPU e a sua grande capacidade de processamento paralelo, integrando-o numa abordagem que resolve instâncias MaxSAT. Revemos o estado da arte actual de algoritmos de solvers MaxSAT de forma a explorar a direção a tomar com a nossa abordagem. Começando o desenvolvimento com uma versão base que utiliza GPU e uma variação que utiliza apenas CPU, conseguimos compará-las numa fase inicial do desenvolvimento para perceber o nível de ambas. Focámo-nos na utilização de um Algoritmo Genético para esta versão base de forma a melhorar a progressão da qualidade dos resultados da abordagem. Foram desenvolvidas mais variações da nossa abordagem, introduzindo algoritmos que poderiam melhorar a qualidade dos resultados obtidos pelo solver MaxSAT que representa a nossa abordagem. Através de testes conseguimos concluir que os solvers que representam o actual estado da arte são extremamente avançados e competir com os mesmos é difícil, sendo árduo de atingir a mesma qualidade de resultados no mesmo espaço de tempo. Devido às vastas possibilidades de utilização de GPU para resolver MaxSAT, concluimos que não explorámos todas as opções dentro do domínio de uso de GPU e ainda há espaço a explorar.
MaxSAT, SAT, GPU, CUDA

Junho 8, 2017, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Luís Jorge Brás Monteiro Guerra e Silva

Departamento de Engenharia Informática (DEI)

Professor Auxiliar

ORIENTADOR

Vasco Miguel Gomes Nunes Manquinho

Departamento de Engenharia Informática (DEI)

Professor Associado