Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories

Gabriele Masina

doi:10.1007/978-3-032-04167-8_7

Return

Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories

2026-01-01

Gabriele Masina

Roberto Sebastiani *

DOI：10.1007/978-3-032-04167-8_7

Original

Save

View PDF

Abstract

En 中文

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 we 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.

Keywords:

Optimization Modulo Theories

Enumeration

Partial Assignments

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.