通过SMT求解实现自动线性化
Towards Automatic Linearization via SMT Solving
AI总结：
本文研究自动验证与合成归约以实现非线性模型自动线性化的问题，证明该问题可表述为 $\exists^* \forall^*$ 合成问题，并通过SMT求解器结合CEGIS方法求解。
摘要：
数学优化在现代应用中无处不在。然而在实践中，我们常需使用非线性优化模型，现有的优化工具如Cplex或Gurobi可能无法直接适用，往往必须进行（易出错的）手动转换。因此，为解决此问题，本文研究了自动验证与合成归约的问题，其解决方案有望实现非线性模型的自动线性化。我们证明，归约的合成可被表述为 $\exists^* \forall^*$ 合成问题，该问题可通过反例引导归纳合成方法（CEGIS），由SMT求解器求解。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
