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

翻译：数学优化在现代应用中无处不在。然而，实践中我们常常需要使用非线性优化模型，而现有优化工具（如Cplex或Gurobi）可能无法直接处理这类模型，通常需要进行（易出错的）人工转换。为解决这一问题，本文研究自动验证与综合归约方法的问题，其解决方案有望实现非线性模型的自动线性化。我们证明归约综合可表述为$\exists^* \forall^*$综合问题，该问题可通过反例引导的归纳综合方法（CEGIS）借助SMT求解器进行求解。