/img alt="Imagem da capa" class="recordcover" src="""/>
Dissertação
Um novo método de otimização baseado em teorias de satisfatibilidade
Este trabalho apresenta um novo método de otimização aplicado a diferentes classes de problemas, como não-convexos e convexos. A metodologia consiste na utilização do contraexemplo gerado a partir da técnica de verificação de modelos, baseada na teoria de satisfatibilidade booleana (SAT) ou na te...
Autor principal: | Araújo, Rodrigo Farias |
---|---|
Outros Autores: | http://lattes.cnpq.br/2107906714409879 |
Grau: | Dissertação |
Idioma: | por |
Publicado em: |
Universidade Federal do Amazonas
2017
|
Assuntos: | |
Acesso em linha: |
http://tede.ufam.edu.br/handle/tede/5715 |
Resumo: |
---|
Este trabalho apresenta um novo método de otimização aplicado a diferentes classes de
problemas, como não-convexos e convexos. A metodologia consiste na utilização do contraexemplo
gerado a partir da técnica de verificação de modelos, baseada na teoria de satisfatibilidade
booleana (SAT) ou na teoria do módulo de satisfatibilidade (SMT), para guiar o processo
de otimização. São desenvolvidos três algoritmos de otimização, são eles: Algoritmo Genérico,
aplicado a qualquer classe de problema de otimização, neste será utilizado na otimização de
funções não-convexas, Algoritmo Simplificado, empregado na otimização de funções nas quais
tem-se algum conhecimento prévio, por exemplo, funções semi-definidas ou definidas positivas
e Algoritmo Rápido, utilizado para otimização de funções convexas. Adicionalmente, são
fornecidas as provas de convergência para os respectivos algoritmos. Os algoritmos são implementados
utilizando dois verificadores de modelos, o CBMC que utiliza como back-end o
solucionador MiniSAT baseado em SAT, e o ESBMC, que tem suporte aos solucionadores baseados
em SMT, como: Z3, Boolector e MathSAT. Para avaliação de desempenho, os algoritmos
são aplicados a um conjunto de trinta funções retiradas da literatura e utilizadas para teste de
algoritmos de otimização, os mesmos também são comparados com algoritmos de otimização
tradicionais usualmente empregados na resolução de problemas de otimização não-convexa,
como: algoritmo genético, enxame de partícula, busca de padrões, recozimento simulado e
programação não-linear. Através da análise dos resultados pode-se concluir que os algoritmos
desenvolvidos são adequados as classes de funções para os quais foram desenvolvidos e possuem
maior taxa de acerto na busca pelo valor ótimo em comparação com os outros algoritmos.
Finalmente a metodologia desenvolvida é aplicada para resolver problemas de otimização no
contexto de planejamento de caminhos bidimensionais para robô móveis autônomos. |