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.
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