On Optimization Modulo Theories, MaxSMT and Sorting Networks

Abstract

Optimization Modulo Theories $$\text {OMT}$$ is an extension of SMT which allows for finding models that optimize given objectives. Partial weighted MaxSMT---or equivalently $$\text {OMT}$$ with Pseudo-Boolean objective functions, $$\text {OMT+PB}$$ --- is a very-relevant strict subcase of $$\text {OMT}$$. We classify existing approaches for MaxSMT or $$\text {OMT+PB}$$ in two groups: MaxSAT-based approaches exploit the efficiency of state-of-the-art MaxSAT solvers, but they are specific-purpose and not always applicable; OMT-based approaches are general-purpose, but they suffer from intrinsic inefficiencies on MaxSMT/$$\text {OMT+PB}$$ problems. We identify a major source of such inefficiencies, and we address it by enhancing $$\text {OMT}$$ by means of bidirectional sorting networks. We implemented this idea on top of the OptiMathSAT $$\text {OMT}$$ solver. We run an extensive empirical evaluation on a variety of problems, comparing MaxSAT-based and $$\text {OMT}$$-based techniques, with and without sorting networks, implemented on top of OptiMathSAT and [InlineEquation not available: see fulltext.]. The results support the effectiveness of this idea, and provide interesting insights about the different approaches.