@MASTERSTHESIS{ 2017:2134073275,
 	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}
}