Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories

TL;DR

This work analyzes how truth-assignment enumeration in Optimization Modulo Theories (OMT) can be improved by using partial assignments rather than only total ones. It introduces assignment-reduction techniques that prune the search space in a cost-guided manner and demonstrates their integration in OptiMathSAT, showing improved solving times and better anytime solutions across $OMT(\mathcal{LRA})$, $OMT(\mathcal{LIRA})$, and $OMT(\mathcal{LRA} \cup AR)$ benchmarks. The results indicate that partial-assignment reduction yields substantial speedups and higher-quality upper bounds within time limits, highlighting practical benefits for industrial OMT tasks. The approach leverages incremental SMT solving and theory minimization, offering a path to generalize partial-assignment strategies to additional theories and objectives. Overall, the paper advances practical OMT solving by marrying partial-assignment reasoning with traditional bound-tightening techniques.

Abstract

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 assignment-reduction techniques for exploiting partial-assignment enumeration within the OMT context. We implemented these techniques in the OptiMathSAT solver, and conducted an experimental evaluation on OMT benchmarks. The results confirm the improvement in both the efficiency of optimal solving and the quality of the obtained solutions for anytime solving.