Uma abordagem de otimização guiada por contraexemplos usando solucionadores SAT e SMT

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.