Learning to Select Partial Assignments for Optimization Modulo Theories

Many applications built on satisfiability modulo theories (SMT) need optimal solutions under their existing logical constraints. Optimization Modulo Theories (OMT) provides this capability by optimizing numerical objectives over the formula's satisfying assignments. Its solvers must resolve logical alternatives while finding and establishing the best objective value permitted by the formula. We present NeurOMT, a framework for guiding OMT over linear integer arithmetic by selecting candidate partial assignments. Each candidate assigns truth values to a subset of arithmetic predicates, restricting the search while leaving numerical values open. We train a graph neural network to select among these candidates using the total solver cost of restricted optimization and subsequent exact search. The network scores each candidate from its assigned atoms, their truth values, and the formula representation. The selected assignment guides optimization to obtain an objective bound, followed by exact continuation under the original constraints. Experiments show reductions in total solver-stage time relative to direct Z3 on OMT benchmarks including knapsack and resource-constrained scheduling, with ratios from 11.4% to 94.4%.