OptiRica：迈向高效优化型 Horn 求解器
计算机科学中的逻辑
2022-11-23 v1 软件工程
摘要
本文描述了一项正在进行的努力，即开发 Eldarica Horn 求解器的优化版本。该工作始于如下观察：许多种类的优化问题，特别是 MaxSAT/SMT 问题，可被视为格上的搜索问题。本文提出一个 Scala 库，提供领域特定语言（DSL）以通过定义、操纵和系统性探索带关联目标函数的格，来统一建模此类优化问题。该框架可被实例化以获得一个优化型 Horn 求解器。作为示例，描述了优化求解器在修复软件定义网络中的应用。
引用
@article{arxiv.2211.12229,
title = {OptiRica: Towards an Efficient Optimizing Horn Solver},
author = {Hossein Hojjat and Philipp Rümmer},
journal= {arXiv preprint arXiv:2211.12229},
year = {2022}
}
备注
In Proceedings HCVS/VPT 2022, arXiv:2211.10675