Manyopt：一个通过SMT求解混合非线性优化的可扩展工具
Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving
摘要：
混合非线性规划（MINLP）的优化支持化学过程工程等应用中的重要决策。但目前的求解器具有有限的能力，演绎推理或使用特定领域的理论，和完整性约束的管理还没有利用自动推理工具，如SMT求解器。这似乎限制了这些工具在实践中的可扩展性和范围。因此，我们提出了一个工具，ManyOpt，MINLP优化，使实验减少技术转换的MINLP问题的可行性检查实现的SMT求解器。ManyOpt类似于SAT求解器ManySAT，因为它并行运行指定数量的此类约简技术，以获得给定MINLP问题的最强结果。该工具是分层实现的，我们可以将其视为特征，其中约简技术是特征向量。这些特征中的一些特征受到已知MINLP技术的启发，而另一些特征是新颖的并且特定于SMT。我们在标准基准上的实验结果证明了这种方法的好处。该工具支持各种SMT求解器，并且由于其分层结构，可以轻松扩展新功能。例如，很容易添加用于演绎推理的逻辑公式，以进一步约束感兴趣的MINLP问题的优化。
英文摘要：
Optimization of Mixed-Integer Non-Linear Programming (MINLP) supports important decisions in applications such as Chemical Process Engineering. But current solvers have limited ability for deductive reasoning or the use of domain-specific theories, and the management of integrality constraints does not yet exploit automated reasoning tools such as SMT solvers. This seems to limit both scalability and reach of such tools in practice. We therefore present a tool, ManyOpt, for MINLP optimization that enables experimentation with reduction techniques which transform a MINLP problem to feasibility checking realized by an SMT solver. ManyOpt is similar to the SAT solver ManySAT in that it runs a specified number of such reduction techniques in parallel to get the strongest result on a given MINLP problem. The tool is implemented in layers, which we may see as features and where reduction techniques are feature vectors. Some of these features are inspired by known MINLP techniques whereas others are novel and specific to SMT. Our experimental results on standard benchmarks demonstrate the benefits of this approach. The tool supports a variety of SMT solvers and is easily extensible with new features, courtesy of its layered structure. For example, logical formulas for deductive reasoning are easily added to constrain further the optimization of a MINLP problem of interest.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
