Towards Automatic Linearization via SMT Solving

TL;DR

This paper proposes an SMT-based approach to automatically verify and synthesize linearizations of nonlinear optimization models, reducing manual effort and error in model transformation.

Contribution

It introduces a novel SMT formulation for synthesizing reductions that enable automatic linearization of nonlinear models, leveraging CEGIS for solution.

Findings

SMT solver effectively synthesizes reductions for linearization.

Automated approach reduces manual transformation errors.

Potential to improve optimization workflow automation.

Abstract

Mathematical optimization is ubiquitous in modern applications. However, in practice, we often need to use nonlinear optimization models, for which the existing optimization tools such as Cplex or Gurobi may not be directly applicable and an (error-prone) manual transformation often has to be done. Thus, to address this issue, in this paper we investigate the problem of automatically verifying and synthesizing reductions, the solution of which may allow an automatic linearization of nonlinear models. We show that the synthesis of reductions can be formulated as an $\exists^* \forall^*$ synthesis problem, which can be solved by an SMT solver via the counter-example guided inductive synthesis approach (CEGIS).