Counterexample Guided Inductive Optimization

TL;DR

This paper introduces three variants of a counterexample guided inductive optimization approach using SMT solvers, effectively solving complex non-linear and non-convex optimization problems by leveraging counterexamples to guide the search.

Contribution

The paper presents novel CEGIO algorithms that utilize counterexamples from SMT solvers to improve optimization of complex functions, outperforming traditional methods.

Findings

Successfully optimized a wide range of functions including non-linear and non-convex problems.

Found optimal solutions in all evaluated benchmarks, avoiding local minima.

Demonstrated efficiency and effectiveness over traditional optimization techniques.

Abstract

This paper describes three variants of a counterexample guided inductive optimization (CEGIO) approach based on Satisfiability Modulo Theories (SMT) solvers. In particular, CEGIO relies on iterative executions to constrain a verification procedure, in order to perform inductive generalization, based on counterexamples extracted from SMT solvers. CEGIO is able to successfully optimize a wide range of functions, including non-linear and non-convex optimization problems based on SMT solvers, in which data provided by counterexamples are employed to guide the verification engine, thus reducing the optimization domain. The present algorithms are evaluated using a large set of benchmarks typically employed for evaluating optimization techniques. Experimental results show the efficiency and effectiveness of the proposed algorithms, which find the optimal solution in all evaluated benchmarks, while traditional techniques are usually trapped by local minima.