.png){kind=icon}
.png){kind=icon}
Return
Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
.png){kind=icon}
OA
AI
DOI：10.1007/978-3-032-04167-8_7.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
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.
Journal
F
IF:
0
Papers:
21
Citations:
0