@MASTERSTHESIS{ 2017:1040763736,
 	title = {Um novo método de otimização baseado em teorias de satisfatibilidade},
 	year = {2017},
 	url = "http://tede.ufam.edu.br/handle/tede/5715",
 	abstract = "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.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de Pós-graduação em Engenharia Elétrica},
 	note = {Faculdade de Tecnologia}
}