On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT

Optimization Modulo Theories (OMT) is an extension of SMT, which combines SMT with optimization, findingmodels that make given objectives optimal. OMT has been extended to be incremental and to handle multiple objective functions either independently or with their linear, lexicographic, Pareto, min-max/max-min combinations.OMT applications can be found not only in the domains of Formal Verification, Automated Reasoning and Planningwith Resources, but also Machine Learning and Requirement Engineering.(Partial weighted) MAXSMT–or, alternatively, OMT with Pseudo-Boolean objective functions– is a very-relevantsubcase of OMT. Unfortunately, using general OMT algorithm for MAXSMT suffers from some intrinsic inefficiencies in some cases. In this paper we identify the sources of such inefficiencies and address them by enhancinggeneral OMT by means of sorting networks. We implemented this idea on top of the OPTIMATHSAT OMT solverand evaluated them empirically on problems coming from Machine Learning and Requirement Engineering. Theempirical results support the effectiveness of this idea.