Towards Automatic Linearization via SMT Solving
Jian Cao, Liyong Lin, Lele Li
TL;DR
This work addresses automatic verification and synthesis of reductions to enable linearization of nonlinear optimization models, reducing reliance on error-prone manual transformations. It formalizes reductions as an $\exists^* \forall^*$ synthesis problem and solves it with an SMT-based counter-example guided inductive synthesis (CEGIS) loop under bounded synthesis, introducing an $ (l,k) $-linearization with coefficient matrix $X$. Motivating examples, such as $c=\max\{a,b\}$ and $c=ab$, illustrate how nonlinear predicates can be represented via linear inequalities and auxiliary Booleans, with correctness framed as SMT-verifiable conditions. The main contributions include reducing bounded verification to SMT, applying CEGIS to synthesize optimal reductions, and discussing practical limitations and future work toward approximate synthesis for larger nonlinear models. Overall, the approach promises more reliable automated linearization of nonlinear models for solvers that require linear or piecewise-linear representations, with potential impact on optimization workflows in engineering and operations research.
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).