@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} }