???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/7096
Tipo do documento: Dissertação
Título: Uma abordagem de otimização guiada por contraexemplos usando solucionadores SAT e SMT
Autor: Albuquerque, Higo Ferreira 
Primeiro orientador: Cordeiro, Lucas Carvalho
Primeiro coorientador: Lima Filho, Eddie Batista de
Primeiro membro da banca: Barreto, Raimundo da Silva
Segundo membro da banca: Medeiros, Renan Landau Paiva de
Resumo: 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.
Abstract: The optimization process requires a mathematical formulation of the system or problem to be optimized, and considering that the formal methods are techniques based on the mathematical formalisms used for the specification, development and verification of systems, we try to use formal methods to optimize mathematical functions. This qualification presents the contributions to the development of the Counterexample Guided Inductive Optimization Algorithms (CEGIO) and the OptCE optimization tool. The goal is to establish the use of Bounded Model Checker for the optimization in convex and non- convex functions, encapsulating the methodology in a tool, allowing a counterexample guided optimization of the solvers Boolean Satisfiability and Satisfiability Modulo Theories. During the work, the methodology and example for an optimization guided by counterexamples are detailed, as well as the algorithms developed CEGIO, whose goal is to locate the global minimum of a function. The development, functionalities and experimental evaluation of the OptCE optimization tool are also presented. The user provides a file with the modeling of the optimization function and its constraints, and OptCE uses the information entered to implement the CEGIO algorithms as well as to insert properties, make use of program verifiers to check properties, generate counterexamples SAT and SMT, executing in an automated way the steps of specification and verification successive times, looking for the optimal point of the function. The experimental evaluations of the OptCE were performed from optimization functions obtained from the literature, and were compared with other traditional techniques. The experiments use 40 functions (convex and non-convex), where the results obtained, it is demonstrated their ability to optimization, having better-hit rate compared to other traditional techniques.
Palavras-chave: Verificadores de programas
Otimização
OptCE
Algoritmo CEGIO
Área(s) do CNPq: ENGENHARIAS: ENGENHARIA ELÉTRICA
Idioma: por
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Faculdade de Tecnologia
Programa: Programa de Pós-graduação em Engenharia Elétrica
Citação: ALBUQUERQUE, Higo Ferreira. Uma abordagem de otimização guiada por contraexemplos usando solucionadores SAT e SMT. 2019. 100 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2019.
Tipo de acesso: Acesso Aberto
Endereço da licença: http://creativecommons.org/licenses/by-nc-nd/4.0/
URI: https://tede.ufam.edu.br/handle/tede/7096
Data de defesa: 27-Mar-2019
Appears in Collections:Mestrado em Engenharia Elétrica

Files in This Item:
File Description SizeFormat 
Dissertação_HigoAlbuquerque_PPGEE.pdf1,7 MBAdobe PDFThumbnail

Download/Open Preview


This item is licensed under a Creative Commons License Creative Commons