@MASTERSTHESIS{ 2019:114357637,
 	title = {Uma abordagem de otimiza??o guiada por contraexemplos usando solucionadores SAT e SMT},
 	year = {2019},
 	url = "https://tede.ufam.edu.br/handle/tede/7096",
 	abstract = "O processo de otimiza??o exige uma formula??o matem?tica do sistema ou problema a
 ser otimizado, e considerando que os m?todos formais s?o t?cnicas baseadas nos formalismos
 matem?ticos usados para a especifica??o, desenvolvimento e verifica??o de sistemas, busca-se
 usar m?todos formais para a otimiza??o de fun??es matem?ticas.
 Este trabalho apresenta o desenvolvimento da ferramenta de otimiza??o guiada por
 contraexemplos OptCE, assim como os algoritmos de otimiza??o indutiva guiada por
 contraexemplos (CEGIO). Busca-se estabelecer o uso da verifica??o de modelos limitados
 para a otimiza??o em fun??es convexas e n?o convexas, encapsulando a metodologia em uma
 ferramenta, permitindo uma otimiza??o guiada a partir de contraexemplos dos solucionadores
 de Satisfatibilidade Booleana (Boolean Satisfiability - SAT) e Teoria do M?dulo de
 Satisfatibilidade (Satisfiability Modulo Theories - SMT).
 Durante o trabalho ? detalhado a metodologia e exemplo para uma otimiza??o guiada
 por contraexemplos, assim como os algoritmos CEGIO, que t?m como objetivo a localiza??o
 do m?nimo global em uma fun??o.
 Tamb?m s?o apresentados o desenvolvimento,
 funcionalidades e avalia??o da ferramenta de otimiza??o OptCE. O usu?rio fornece um arquivo
 com a modelagem da fun??o e suas restri??es, e o OptCE usa as informa??es para implementar
 os algoritmos CEGIO, inserir propriedades, aplicar verificadores de programas para checar
 propriedades, gerar contraexemplos SAT e SMT, executando de forma automatizada as etapas
 de especifica??o e verifica??o sucessivas vezes em busca do ponto ?timo da fun??o.
 A avalia??o do OptCE foi realizada a partir de fun??es de otimiza??o obtidas da
 literatura, e foram comparadas com outras t?cnicas tradicionais. Os experimentos utilizaram
 40 fun??es (convexas e n?o convexas) onde os resultados obtidos mostram sua capacidade de
 otimiza??o, tendo melhor taxa de acerto quando comparada com as t?cnicas.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Engenharia El?trica},
 	note = {Faculdade de Tecnologia}
}