论文标题
Optirica：迈向有效的优化喇叭求解器
OptiRica: Towards an Efficient Optimizing Horn Solver
论文作者
论文摘要
本文介绍了持续的努力，以开发Eldarica Horn求解器的优化版本。这项工作始于观察到的许多优化问题，尤其是MaxSat/SMT问题，可以看作是晶格上的搜索问题。该论文提供了一个Scala库，该库通过定义，操纵和系统地探索具有相关目标功能的晶格，从而提供了特定于领域的语言（DSL），以统一地模拟此类问题。可以实例化该框架以获得优化的号角求解器。作为例证，描述了优化求解器在修复软件定义网络中的应用。
This paper describes an ongoing effort to develop an optimizing version of the Eldarica Horn solver. The work starts from the observation that many kinds of optimization problems, and in particular the MaxSAT/SMT problem, can be seen as search problems on lattices. The paper presents a Scala library providing a domain-specific language (DSL) to uniformly model optimization problems of this kind, by defining, manipulating, and systematically exploring lattices with associated objective functions. The framework can be instantiated to obtain an optimizing Horn solver. As an illustration, the application of an optimizing solver for repairing software-defined networks is described.
