Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories

TL;DR

This paper improves Optimization Modulo Theories (OMT) solving by using partial truth assignments instead of total ones, leading to more efficient and higher-quality solutions, demonstrated through implementation and experiments.

Contribution

It introduces assignment-reduction techniques that leverage partial assignments in OMT, enhancing solver efficiency and solution quality.

Findings

Improved efficiency in optimal solving.

Enhanced solution quality for anytime solving.

Partial assignment enumeration outperforms total assignments.

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.