FenixEdu™

Dissertação

{pt_PT=Algorithms for Maximum Satisfiability using GPU} {} EVALUATED

Detalhes: {pt=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., en=Interest in algorithms for solving Maximum Satisfiability (MaxSAT) has been increasing greatly in the last few years. However, there seems to exist a great lack in the use of the power available in GPUs. For this work we presented a proposal to harness the GPU and its great parallel computing power, integrating it into an approach that solves MaxSAT instances. We reviewed some of the current state of MaxSAT solver algorithms in order to explore the direction of our approach. Starting with development of a base version that utilizes the GPU, and a variation that uses only the CPU we were able to compare each other early on to see where we stood. Focusing on the use of a Genetic Algorithm in this base version in order to improve the quality of results by our approach. Further variations of our approach were developed, introducing algorithms that could improve the quality of the results obtained by the MaxSAT solver that represents our approach. Through testing we could conclude that the current state of the art solvers are extremely advanced and hard to compete against on a level playing field, being difficult to achieve the same quality of results in the same span of time. Due to the vastness of possibilities to use GPU for MaxSAT solving we conclude that we have not explored all options within the domain of use of GPU and there is still room to explore.}
Keywords: {pt=MaxSAT, SAT, GPU, CUDA, en=MaxSAT, SAT, GPU, CUDA}

Discussão: junho 8, 2017, 14:30