???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/5715
Tipo do documento: Dissertação
Título: Um novo método de otimização baseado em teorias de satisfatibilidade
Autor: Araújo, Rodrigo Farias 
Primeiro orientador: Chaves Filho, João Edgar
Primeiro membro da banca: Lucena Júnior, Vicente Ferreira
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.
Abstract: This work presents a new method of optimization applied to different classes of problems, such as non-convex and convex. The methodology consists in the use the counterexample generated from the model checking technique based on Boolean satisfiability theory (SAT) and satisfiability modulo theory (SMT), to guide the optimization process. Three algorithms of optimization are developed: Generic Algorithm, applied to any class of optimization problem, it will be used in the optimization of non-convex functions, Simplified Algorithm, used in the optimization of functions in which there is some previous knowledge, e. g., semi-defined or defined positive functions and Fast Algorithm, used to optimize convex functions. In addition, convergence proofs are provided for the respective algorithms. The algorithms are implemented using two model verifiers, CBMC which uses the SAT-based MiniSAT solver as back-end, and the ESBMC, which supports SMT-based solvers, such as Z3, Boolector and MathSAT. For perfomance evaluation, the algorithms are applied to a set of thirty functions taken from the literature and used to test optimization algorithms, they are also compared with traditional optimization algorithms usually used in solving non-convex optimization problems, such as genetic algorithm, particle swarm, pattern search, simulated annealing and nonlinear programming. Through the analysis of the results it can be concluded that the developed algorithms are suitable the classes of functions for which they were developed and have a higher rate of success in the search for the optimal value in comparison with the other algorithms. Finally, the developed methodology is applied to solve optimization problems in the context of the two-dimensional path planning for autonomous mobile robots.
Palavras-chave: Otimização
Satisfabilidade
Teoria do Módulo de Satisfabilidade
Planejamento de caminho
Optimization
Satisfiability
Satisfiability Modulo Theory
Path planning
Área(s) do CNPq: ENGENHARIAS: ENGENHARIA ELÉTRICA
Idioma: por
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Faculdade de Tecnologia
Programa: Programa de Pós-graduação em Engenharia Elétrica
Citação: ARAÚJO, Rodrigo Farias. Um novo método de otimização baseado em teorias de satisfatibilidade. 2017. 82 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2017.
Tipo de acesso: Acesso Aberto
Endereço da licença: http://creativecommons.org/licenses/by-nc-nd/4.0/
URI: http://tede.ufam.edu.br/handle/tede/5715
Data de defesa: 30-Mar-2017
Appears in Collections:Mestrado em Engenharia Elétrica

Files in This Item:
File Description SizeFormat 
Dissertacao_Rodrigo F. Araujo.pdf2,38 MBAdobe PDFThumbnail

Download/Open Preview


This item is licensed under a Creative Commons License Creative Commons