Submitted by Marcos Roberto Gomes (mrobertosg@gmail.com) on 2017-06-22T15:28:21Z
No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-06-23T14:38:14Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-06-23T14:44:39Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) / Made available in DSpace on 2017-06-23T14:44:39Z (GMT). No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5)
Previous issue date: 2017-03-30 / 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. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/5715 |
| Date | 30 March 2017 |
| Creators | Araújo, Rodrigo Farias |
| Contributors | Chaves Filho, João Edgar, Lucena Júnior, Vicente Ferreira |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Engenharia Elétrica, UFAM, Brasil, Faculdade de Tecnologia |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFAM, instname:Universidade Federal do Amazonas, instacron:UFAM |
| Rights | http://creativecommons.org/licenses/by-nc-nd/4.0/, info:eu-repo/semantics/openAccess |
| Relation | -5930111888266832212, 500 |
Page generated in 0.0027 seconds