Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by enabling solvers to find optimal solutions based on a defined objective function after verifying formula satisfiability. Adding OMT capabilities to the library would significantly enhance its ability to solve optimization problems directly.
I have implemented a prototype using Z3’s APIs. The solution is functional but hacky. I’m unsure if it’s the correct approach and it is inefficient because it copies all constraints to the optimizer. I’m also uncertain whether other SMT solvers support OMT, as my experience with SMT is limited.
data class MinimizingSolverZ3(val impl: KZ3Solver) : MinimizingSolver<KZ3SolverConfiguration>,
KSolver<KZ3SolverConfiguration> by impl {
val z3Ctx: KZ3Context =
impl::class.java.getDeclaredField("z3Ctx").apply { isAccessible = true }.get(impl) as KZ3Context
val exprInternalizer = impl::class.java.getDeclaredMethod("getExprInternalizer")
.apply { isAccessible = true }.invoke(impl) as KZ3ExprInternalizer
val exprCreate = Expr::class.java.getDeclaredMethod("create", Context::class.java, Long::class.java)
.apply { isAccessible = true } as Method
override fun <K : KArithSort> modelMinimizing(
expr: KExpr<K>,
maxIterations: Int,
timeout: Duration,
): KModel {
// Sadly, we need to create an Optimize object and copy all Solver constraints to it
val opt: Optimize = z3Ctx.nativeContext.mkOptimize()
applyTimeout(opt, timeout)
for (c in impl.nativeSolver().assertions) opt.Assert(c)
// Add the expression to minimize
val exprId = with(exprInternalizer) { expr.internalizeExpr() }
val convertedExpr = exprCreate.invoke(null, z3Ctx.nativeContext, exprId) as Expr<*>
opt.MkMinimize(convertedExpr)
// Normal check, but using the optimizer
opt.Check()
// Extract the model and return it
return KZ3Model(opt.model, expr.ctx, z3Ctx, exprInternalizer)
}
private fun applyTimeout(opt: Optimize, timeout: Duration) {
val z3Timeout = if (timeout == Duration.INFINITE) UInt.MAX_VALUE.toInt()
else timeout.toInt(DurationUnit.MILLISECONDS)
opt.setParameters(z3Ctx.nativeContext.mkParams().apply { add("timeout", z3Timeout) })
}
}
Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by enabling solvers to find optimal solutions based on a defined objective function after verifying formula satisfiability. Adding OMT capabilities to the library would significantly enhance its ability to solve optimization problems directly.
I have implemented a prototype using Z3’s APIs. The solution is functional but hacky. I’m unsure if it’s the correct approach and it is inefficient because it copies all constraints to the optimizer. I’m also uncertain whether other SMT solvers support OMT, as my experience with SMT is limited.