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 |
| id |
oai:https:--tede.ufam.edu.br-handle-:tede-5715 |
|---|---|
| recordtype |
dspace |
| spelling |
oai:https:--tede.ufam.edu.br-handle-:tede-57152018-08-16T18:08:54Z Um novo método de otimização baseado em teorias de satisfatibilidade Araújo, Rodrigo Farias Chaves Filho, João Edgar http://lattes.cnpq.br/2107906714409879 http://lattes.cnpq.br/2956430211742934 Lucena Júnior, Vicente Ferreira http://lattes.cnpq.br/6820830740393500 Otimização Satisfabilidade Teoria do Módulo de Satisfabilidade Planejamento de caminho Optimization Satisfiability Satisfiability Modulo Theory Path planning ENGENHARIAS: ENGENHARIA ELÉTRICA 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. 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. 2017-06-23T14:44:39Z 2017-03-30 Dissertaçã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. http://tede.ufam.edu.br/handle/tede/5715 por Acesso Aberto http://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica |
| institution |
TEDE - Universidade Federal do Amazonas |
| collection |
TEDE-UFAM |
| language |
por |
| topic |
Otimização Satisfabilidade Teoria do Módulo de Satisfabilidade Planejamento de caminho Optimization Satisfiability Satisfiability Modulo Theory Path planning ENGENHARIAS: ENGENHARIA ELÉTRICA |
| spellingShingle |
Otimização Satisfabilidade Teoria do Módulo de Satisfabilidade Planejamento de caminho Optimization Satisfiability Satisfiability Modulo Theory Path planning ENGENHARIAS: ENGENHARIA ELÉTRICA Araújo, Rodrigo Farias Um novo método de otimização baseado em teorias de satisfatibilidade |
| topic_facet |
Otimização Satisfabilidade Teoria do Módulo de Satisfabilidade Planejamento de caminho Optimization Satisfiability Satisfiability Modulo Theory Path planning ENGENHARIAS: ENGENHARIA ELÉTRICA |
| description |
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. |
| author_additional |
Chaves Filho, João Edgar |
| author_additionalStr |
Chaves Filho, João Edgar |
| format |
Dissertação |
| author |
Araújo, Rodrigo Farias |
| author2 |
http://lattes.cnpq.br/2107906714409879 |
| author2Str |
http://lattes.cnpq.br/2107906714409879 |
| title |
Um novo método de otimização baseado em teorias de satisfatibilidade |
| title_short |
Um novo método de otimização baseado em teorias de satisfatibilidade |
| title_full |
Um novo método de otimização baseado em teorias de satisfatibilidade |
| title_fullStr |
Um novo método de otimização baseado em teorias de satisfatibilidade |
| title_full_unstemmed |
Um novo método de otimização baseado em teorias de satisfatibilidade |
| title_sort |
um novo método de otimização baseado em teorias de satisfatibilidade |
| publisher |
Universidade Federal do Amazonas |
| publishDate |
2017 |
| url |
http://tede.ufam.edu.br/handle/tede/5715 |
| _version_ |
1831969506058043392 |
| score |
11.753735 |