Dissertação

Distributed Solver for Maximum Satisfiability EVALUATED

Satisfação Máxima (MaxSAT) é uma versão de optimização do problema de Satisfação Booleana (SAT). Muitos problemas do mundo real podem ser reduzidos a resolver uma instância de MaxSAT, incluindo problemas de interesse industrial. Portanto, MaxSAT é um problema importante para se resolver e, nos anos mais recentes, muitos algoritmos eficientes têm sido desenvolvidos, com o propósito de resolver este problema, e analisados. Alguns destes algoritmos são paralelos, mas nenhum algoritmo distribuído foi desenvolvido até agora. Esta dissertação analiza as abordagens existentes para resolver MaxSAT e propõe dois algoritmos distribuídos para um aglomerado de processadores sobre o controlo do utilizador. Estes dois algoritmos foram implementados e depois testados, estudados e comparados com um dos solvers sequenciais de MaxSAT mais eficazes que existem na actualidade. O primeiro algoritmo é muito semelhante a um algoritmo paralelo de sucesso já existente para MaxSAT, e o segundo é uma adaptação de uma abordagem que mostrou ser bastante eficaz na resolução sequencial, paralela e distribuída de SAT.
Satisfação Booleana (SAT), Boolean Optimization, Satisfação Máxima (MaxSAT), Procura Distribuída, Divisão do Espaço de Procura, Caminhos Norteadores com Lookahead

Outubro 28, 2014, 16:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

CO-ORIENTADOR

Maria Inês Camarate de Campos Lynce de Faria

Departamento de Engenharia Informática (DEI)

Professor Associado

ORIENTADOR

Vasco Miguel Gomes Nunes Manquinho

Departamento de Engenharia Informática (DEI)

Professor Auxiliar