Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) with the task of optimizing some objective function(s). In OMT solvers, a CDCL-based SMT solver enumerates theory-satisfiable total truth assignments, and a theory-specific procedure finds an optimum model for each of them; the current optimum is then used to tighten the search space for the next assignments, until no better solution is found. In this paper, we analyze the role of truth-assignment enumeration in OMT. First, we spotlight that the enumeration of total truth assignments is suboptimal, since they may over-restrict the search space for the optimization procedure, whereas using partial truth assignments instead can improve the effectiveness of the optimization. Second, we propose some reduction techniques for better exploiting partial assignments in the OMT context. We implemented these techniques in the OPTIMATHSAT solver, and conducted an experimental evaluation on OMT(LRA) benchmarks. The results support the efficiency and effectiveness of our approach.

翻译：理论模优化（OMT）在可满足性模理论（SMT）的基础上扩展了优化目标函数的功能。在OMT求解器中，基于冲突驱动子句学习的SMT求解器枚举理论可满足的完全真值赋值，并由特定理论过程为每个赋值寻找最优模型；当前最优解随后被用于收紧后续赋值的搜索空间，直至无法找到更优解。本文分析了真值赋值枚举在OMT中的作用。首先，我们指出完全真值赋值的枚举存在次优性，因为它们可能过度限制优化过程的搜索空间，而使用部分真值赋值反而能提升优化效率。其次，我们提出了若干约简技术，以在OMT框架中更有效地利用部分赋值。我们在OPTIMATHSAT求解器中实现了这些技术，并在OMT(LRA)基准测试上进行了实验评估。结果验证了我们方法的效率与有效性。