Dissertação

MPBO: a Distributed Pseudo-Boolean Optimization Solver EVALUATED

A computação paralela tem sido alvo de grande investigação na última década e é cada vez mais escolhida como uma solução para o desenvolvimento de aplicações que exigem um grande poder computacional, como o caso dos problemas de Satisfação Booleana (SAT) e Optimização Pseudo-Booleana (PBO). A investigação nos SAT solvers tem obtido resultados relevantes nos últimos anos, alcançando reduções significativas nos seus tempos de execução. Infelizmente, instâncias mais difíceis do problema SAT requerem um grande poder computacional e até mesmo os SAT solvers mais eficientes obtêm tempos de execução enormes para encontrar a sua solução. Portanto, adaptações dos SAT solvers que tiram partido de sistemas de computação paralela começaram a ser foco de grande investigação e já existem várias versões distribuídas de SAT solvers populares. No entanto, a ausência de solvers distribuídos para o problema de optimização Pseudo-Boolean é notória. Este trabalho pretende contribuir e incentivar a investigação de soluções distribuídas para resolver o problema PBO. O objectivo deste trabalho é propor um solver distribuído para resolver o problema de optimização Pseudo-Booleana, chamado de MPBO solver, baseado em MPI (Message Passing Interface) e focado numa partição eficiente do espaço de procura, mais especificamente na partição do espaço de optimização do problema. O solver proposto conseguiu reduções significativas no tempo para resolver instâncias difíceis do problema, quando comparado com os solvers Minisat+ e pwbo.
Optimização Pseudo-Booleana (PBO), Satisfiabilidade Booleana (SAT), Message Passing Interface (MPI), Sistemas Distribuídos (GRID).

Maio 27, 2013, 9:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

CO-ORIENTADOR

José Carlos Alves Pereira Monteiro

Departamento de Engenharia Informática (DEI)

Professor Associado

ORIENTADOR

Paulo Ferreira Godinho Flores

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

Professor Auxiliar