Counterexample guided inductive optimization based on satisfiability modulo theories

Rodrigo F. Araújo; Higo F. Albuquerque; Iury V. De Bessa; Lucas C. Cordeiro; João E. Chaves Filho

doi:10.1016/j.scico.2017.10.004

Counterexample guided inductive optimization based on satisfiability modulo theories

Rodrigo F. Araújo, Higo F. Albuquerque, Iury V. De Bessa, Lucas C. Cordeiro, João E. Chaves Filho

Formal Methods

Research output: Contribution to journal › Article › peer-review

298 Downloads (Pure)

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.

Original language	English
Pages (from-to)	3-23
Number of pages	20
Journal	Science of Computer Programming
Volume	165
Early online date	18 Oct 2017
DOIs	https://doi.org/10.1016/j.scico.2017.10.004
Publication status	Published - 1 Nov 2018

Access to Document

10.1016/j.scico.2017.10.004

jscp2017_2Accepted author manuscript, 516 KB

https://linkinghub.elsevier.com/retrieve/pii/S0167642317302162

Cite this

@article{2a22d3a17a574fd4833bbcbfd19c82ab,

title = "Counterexample guided inductive optimization based on satisfiability modulo theories",

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.",

author = "Ara{\'u}jo, {Rodrigo F.} and Albuquerque, {Higo F.} and {De Bessa}, {Iury V.} and Cordeiro, {Lucas C.} and {Chaves Filho}, {Jo{\~a}o E.}",

year = "2018",

month = nov,

day = "1",

doi = "10.1016/j.scico.2017.10.004",

language = "English",

volume = "165",

pages = "3--23",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Counterexample guided inductive optimization based on satisfiability modulo theories

AU - Araújo, Rodrigo F.

AU - Albuquerque, Higo F.

AU - De Bessa, Iury V.

AU - Cordeiro, Lucas C.

AU - Chaves Filho, João E.

PY - 2018/11/1

Y1 - 2018/11/1

N2 - 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.

AB - 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.

U2 - 10.1016/j.scico.2017.10.004

DO - 10.1016/j.scico.2017.10.004

M3 - Article

SN - 0167-6423

VL - 165

SP - 3

EP - 23

JO - Science of Computer Programming

JF - Science of Computer Programming

ER -

Counterexample guided inductive optimization based on satisfiability modulo theories

Abstract

Access to Document

Fingerprint

Cite this