关于最优化模理论、MaxSMT和排序网络
On Optimization Modulo Theories, MaxSMT and Sorting Networks
摘要：
优化模理论（OMT）是SMT的扩展，它允许找到优化给定目标的模型。（部分加权）MaxSMT -或等效的OMT与伪布尔目标函数，OMT+PB-是OMT的一个非常相关的严格子情况。我们将现有的MaxSMT或OMT+PB方法分为两组：基于MaxSAT的方法利用了最先进的MAXSAT求解器的效率，但它们是专用的，并不总是适用的;基于OMT的方法是通用的，但它们在MaxSMT/OMT+PB问题上存在固有的效率低下。我们确定了这种低效率的一个主要来源，我们解决它通过增强OMT的双向排序网络。我们在OptiMathSAT OMT求解器上实现了这个想法。我们对各种问题进行了广泛的实证评估，比较了基于MaxSAT和基于OMT的技术，使用和不使用排序网络，在OptiMathSAT和νZ上实现。结果支持这一想法的有效性，并提供了有关不同方法的有趣见解。
英文摘要：
Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. (Partial weighted) MaxSMT --or equivalently OMT with Pseudo-Boolean objective functions, OMT+PB-- is a very-relevant strict subcase of OMT. We classify existing approaches for MaxSMT or OMT+PB in two groups: MaxSAT-based approaches exploit the efficiency of state-of-the-art MAXSAT solvers, but they are specific-purpose and not always applicable; OMT-based approaches are general-purpose, but they suffer from intrinsic inefficiencies on MaxSMT/OMT+PB problems. We identify a major source of such inefficiencies, and we address it by enhancing OMT by means of bidirectional sorting networks. We implemented this idea on top of the OptiMathSAT OMT solver. We run an extensive empirical evaluation on a variety of problems, comparing MaxSAT-based and OMT-based techniques, with and without sorting networks, implemented on top of OptiMathSAT and νZ. The results support the effectiveness of this idea, and provide interesting insights about the different approaches.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
