1 Introduction

The last two decades have witnessed the rise of Satisfiability Modulo Theories (SMT) [12] as efficient tool for dealing with several applications of industrial interest, in particular in the contexts of Formal Verification (FV). SMT is the problem of finding value assignments satisfying some formula in first-order logic wrt. some background theory. Optimization Modulo Theories (\(\text {OMT}\)) [15, 33, 34, 36, 39, 42, 53, 56] is a more-recent extension of SMT searching for the optimal value assignment(s) w.r.t. some objective function(s), by means of a combination of SMT and optimization procedures. (Since \(\text {OMT}\) extends SMT, hereafter we often simply say “\(\text {OMT}\)” for both SMT and \(\text {OMT}\).)

Several distinctive traits of \(\text {OMT}\) solvers –like, e.g., the efficient combination of Boolean and arithmetical reasoning, incrementality, the availability of decision procedures for infinite-precision arithmetic and the ability to produce conflict explanations– are a direct consequence of their tight relationship with the FV domain and its practical needs. On the whole, it appears that \(\text {OMT}\) can be a potentially interesting and efficient technology for dealing with Constraint Programming (CP) problems as well. At the same time, modeling CP problems for \(\text {OMT}\) solvers requires a higher-level of expertise, because the same CP instance can have many possible alternative formulations, s.t. the performance of SMT solvers on each encoding are hardly predictable [26, 28, 29].

On the other hand, the availability, efficiency and expressiveness of CP tools makes them of potential interest as backend engines also for FV applications (e.g., [22, 23, 31]), in particular with SW verification, where currently SMT is the dominating backend technology, s.t. a large amount of SMT-encoded FV problems are available [11].

In this paper we aim at bridging the gap between CP and \(\text {OMT}\), in both directions.

In the CP-to-\(\text {OMT}\) direction, we have extended the state-of-the-art \(\text {OMT}\) solver OptiMathSAT [58] with a FlatZinc interface (namely “fzn2omt”). In combination with the standard mzn2fzn encoder [38], this new interface can be used to either (i) solve CP models with OptiMathSAT directly or (ii) generate \(\text {OMT}\) formulas encoded in the SMT-LIB [25] format with optimization extensions, to be fed to other \(\text {OMT}\) solvers, such as bclt [16] and Z3 [15]. This allows state-of-the-art \(\text {OMT}\) technology to be used on MiniZinc problems coming from the CP community.

In the \(\text {OMT}\)-to-CP direction, we have introduced a tool for translating SMT and \(\text {OMT}\) problems on the theories of linear arithmetic over the integers and rational (\(\mathcal {LIRA}\)) and bit-vector (\(\mathcal {BV}\)) into MiniZinc models (hereafter “omt2mzn”). This allows MiniZinc solvers to be used on \(\text {OMT}\) problems, giving them access to a large amount of \(\text {OMT}\) problems, mostly coming from formal verification.

With both directions, we first present and discuss the challenges we encountered and the solutions we adopted to address the differences between the two formalisms. Then we present an extensive empirical evaluation comparing three \(\text {OMT}\) tools with many state-of-the-art CP tools on (i) CP problems coming from the MiniZinc challenge, and (ii) \(\text {OMT}\) problems coming mostly from formal verification. This analysis allowed us to identify some criticalities, in terms of efficiency and correctness, one has to cope with when addressing CP problems with \(\text {OMT}\) tools, and vice versa.

Overall, our new compilers fzn2omt and omt2mzn in combination with the standard compiler mzn2fzn [38] provide a framework for translating problems encoded in the SMT-LIB or the MiniZinc format in either direction. This framework enables also for a comparison between \(\text {OMT}\) solvers and CP tools on problems that do not belong to their original application domain. To the best of our knowledge, this is the first time that such a framework has been proposed, and that the \(\text {OMT}\) and CP technologies have been extensively compared on problems coming from both fields.

Related Work. The tight connection between SMT and Constraint Programming (CP) has been known for a relatively long period of time [43] and it has previously been subject to investigation. Some works considered a direct encoding of CP [28, 29] and weighted CP [8] into SMT and MaxSMT, or an automatic framework for translating MiniZinc –a standard CP modeling language [40]– into SMT-LIB –the standard SMT format– [17, 18]. Other works explored the integration of typical SAT and SMT techniques within CP solvers [27, 45]. Nowadays, several MiniZinc solvers –like, e.g., HaifaCSP [61] and Picat [62]– are at least partially based on SAT technology.

To this extent, our first contribution fzn2omt also obviates the loss, due to obsolescence, of the fzn2smt compiler proposed by Bofill et al. in [17, 18]. fzn2smt is not compatible with the changes that have been introduced to the MiniZinc and FlatZinc standards starting from version 2.0 of the MiniZinc distribution. Since some of these changes are not backward compatible, it is also not possible to use fzn2smt in conjunction with an older version of the mzn2fzn compiler when dealing with recent MiniZinc models. Furthermore, fzn2smt translates satisfaction problems into the Version 1 of the SMT-LIB standard and produces no SMT-LIB output in the case of optimization problems, that are solved directly. However, the optimization interface of modern \(\text {OMT}\) solvers is based on the Version 2 of the SMT-LIB standard. This makes it difficult to use it together with \(\text {OMT}\) solvers. Unfortunately, the fzn2smt compiler is closed source, with only the binaries being freely distributed, and seemingly no longer maintained. This made it necessary to provide a new alternative solution to fzn2smt. To this extent, our new FlatZinc interface of OptiMathSAT, fzn2omt, translates both satisfaction and optimization problems in the Version 2 of the SMT-LIB standard enriched with the optimization extensions for \(\text {OMT}\) described in [58].

Content. The rest of the paper is organized as follows. In Sect. 2 we provide some background on \(\text {OMT}\), MiniZinc and FlatZinc. In Sect. 3 we describe the process from MiniZinc to \(\text {OMT}\). In Sect. 4 we describe the process from \(\text {OMT}\) to MiniZinc. In Sect. 5 we describe an empirical evaluation comparing a \(\text {OMT}\)-based tool with many state-of-the-art CP tools. Finally, in Sect. 6 we conclude and point out some further research directions.

A longer and more detailed version of this paper is publicly available as [24].

2 Background

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula \(\varphi \) with respect to a combination of decidable first-order theories. Typical theories of SMT interest are (the theory of) linear arithmetic over the rationals (\(\mathcal {LRA}\)), the integers (\(\mathcal {LIA}\)) or their combination (\(\mathcal {LIRA}\)), non-linear arithmetic over the rationals (\(\mathcal {NLRA}\)) or the integers (\(\mathcal {NLIA}\)), arrays (\(\mathcal {AR}\)), bit-vectors (\(\mathcal {BV}\)), floating-point arithmetic (\(\mathcal {FP}\)), and their combinations thereof. (See [12, 44, 52] for an overview.). The last two decades have witnessed the development of very efficient SMT solvers based on the so-called lazy-SMT schema [12, 52]. This has brought previously-intractable problems to the reach of state-of-the-art SMT solvers.

Optimization Modulo Theories (\(\text {OMT}\)), [15, 34, 36, 39, 42, 53, 56, 60], is an extension to SMT that allows for finding a model of a first-order formula \(\varphi \) that is optimal with respect to some objective function expressed in some background theory, by means of a combination of SMT and optimization procedures. State-of-the art OMT tools allow optimization in a variety of theories, including linear arithmetic over the rationals (\(\text {OMT}(\mathcal {LRA})\)) [53] and the integers (\(\text {OMT}(\mathcal {LIA})\)) [15, 56], bit-vectors (\(\text {OMT}(\mathcal {BV})\)) [39] and floating-point numbers (\(\text {OMT}\)(\(\mathcal {FP}\))) [60].

A relevant strict subcase of \(\text {OMT}(\mathcal {LRA})\) is \(\text {OMT}\) with Pseudo-Boolean objective functions (\(\text {OMT}(\mathcal {PB})\)) in the form \(\sum _i w_i A_i\) s.t. \(w_i\) are rational values and \(A_i\) are Boolean variables whose values are interpreted as \(\{{0,1}\}\). Notice that \(\text {OMT}(\mathcal {PB})\) is also equivalent to (partial weighted) MaxSMT, the SMT extension of MaxSAT, and that \(\text {OMT}(\mathcal {PB})\) and MaxSMT can be encoded into \(\text {OMT}(\mathcal {LRA})\) but not vice versa [54]. Encoding \(\text {OMT}(\mathcal {PB})\)/MaxSMT into \(\text {OMT}(\mathcal {LRA})\), however, is not the most efficient way to solve them, so that modern \(\text {OMT}\) solvers such as bclt [16], OptiMathSAT [58] and Z3 [15] implement specialized \(\text {OMT}(\mathcal {PB})\)/MaxSMT procedures which are much more efficient than general-purpose \(\text {OMT}(\mathcal {LRA})\) ones [15, 57, 58].

We stress the fact that —unlike with purely-combinatorial problems, which are encoded into SAT or MaxSAT and are thus solved by purely-Boolean search– typically \(\text {OMT}\) problems involve the interleaving of both Boolean and arithmetical search: search not only for the best truth-value assignment to the atomic subformulae, but also for the best values to the numerical variables compatible with such truth-value assignment [54].

To this date, few \(\text {OMT}\) solvers exist, namely bclt [16], Cegio [9], Hazel [39], OptiMathSAT [58], Puli [33], Symba [36] and Z3 [15]. To this aim, we observe that (i) some of these solvers are quite recent, (ii) most of these solvers focus on different, partially overlapping, niche subsets of Optimization Modulo Theories, and (iii) the lack of an official Input/Output interface for \(\text {OMT}\) makes it hard to compare some of these tools with one another. \(\text {OMT}\) finds applications in the context of static analysis [19, 32], formal verification and model checking [37, 48], scheduling and planning with resources [33, 35, 46, 50], software security and requirements engineering [41], workflow analysis [13], machine learning [59], and quantum computing [14].

A distinctive trait of SMT (and \(\text {OMT}\)) solvers is the trade-off of speed against the ability to certify the correctness of the result of any computation, which is particularly important in the contexts of Formal Verification (FV) and Model Checking (MC). When dealing with linear arithmetic in particular, SMT solvers employ infinite-precision arithmetic software libraries to avoid numerical errors and overflows.

SMT-LIB [25] is the standard input format by SMT solvers, it provides a standardized definition of the most prominent theories supported by SMT solvers and the corresponding language primitives to use these features. At present, there is no standard input format for modeling optimization problems targeting \(\text {OMT}\) solvers, although there exist only minor syntactical differences between the major \(\text {OMT}\) solvers. The tools presented in this paper conform to the extended SMT-LIB format for \(\text {OMT}\) presented in [58], that includes language primitives for modeling objectives.

OptiMathSAT [53,54,55,56,57,58] is a state-of-the-art \(\text {OMT}\) solver based on the MathSAT5 SMT solver [3, 21]. OptiMathSAT features both single- and multi-objective optimization over arbitrary sets of \(\mathcal {LRA}\), \(\mathcal {LIA}\), \(\mathcal {LIRA}\), \(\mathcal {BV}\), \(\mathcal {FP}\), Pseudo-Boolean (\(\mathcal {PB}\)) and MaxSMT cost functions. Multiple objective functions can be combined with one another into a Lexicographic or a Pareto optimization problem, or independently solved in a single run (for the best efficiency).

MiniZinc [38, 40] is a widely adopted high-level declarative language for modeling Constraint Satisfaction Problems (CSP) and Constraint Optimization Problems (COP). The MiniZinc format defines three scalar types (bool, int and float) and two compound types (sets and fixed-size arrays of some scalar type). The standard provides an extensive list of predefined global constraints, a class of high-level language primitives that allows one to encode complex constraints in a compact way.

FlatZinc is a lower-level language whose purpose is to bridge the gap between the high-level modeling in MiniZinc and the need for a fixed, and easy-to-parse, format that can simplify the implementation of the input interface of MiniZinc solvers. A MiniZinc model is typically flattened into a FlatZinc instance using the mzn2fzn compiler [38], and then solved with some MiniZinc tool.

3 From MiniZinc to \(\text {OMT}\)

We consider the problem of translating MiniZinc models into \(\text {OMT}\) problems first. Similarly to other MiniZinc solvers, we assume that the MiniZinc model is first translated into FlatZinc using the mzn2fzn standard compiler, as depicted in Fig. 1. We describe the main aspects of fzn2omt, focusing on the challenges we have encountered and on the solutions we have adopted.

Fig. 1.
figure 1

Circular translation schema from MiniZinc to SMT-LIB and back, resulting from the composition of mzn2fzn, OptiMathSAT and omt2mzn. In this picture, OptiMathSAT acts both as a FlatZinc/\(\text {OMT}\) solver, and also as a FlatZinc to SMT-LIB compiler.

Full size image

FlatZinc data-types. The first challenge is to find a suitable representation of the data-types supported by FlatZinc in SMT-LIB.

One possible choice for modeling the three basic scalar types of FlatZinc –namely bool, int and float– with SMT-LIB are the Boolean, bit-vector and floating-point theories respectively. However, the decision procedures for the bit-vector and floating-point numbers theories can be significantly more resource demanding than the decision procedure for the linear arithmetic theory (\(\mathcal {LIRA}\)), in particular when dealing with a substantial amount of arithmetic computations. For this reason, we have opted to model FlatZinc int and float data-types with the SMT-LIB integer and rational types respectively, by default. For the case in which no substantial linear arithmetic computation is performed, we also optionally allow for encoding the FlatZinc int data-type as a SMT-LIB bit-vector.

For what concerns the two compound types of FlatZinc, that is the set and array data-types, we have chosen to proceed as follows. Given that OptiMathSAT lacks a decision procedure for the theory of finite sets [7], we model a set using the Boolean and integer theories, similarly to what has been done in [17]. The basic idea is to introduce a fresh Boolean variable for each element in the domain of a set, and use such variable as a placeholder for the membership of an integer element to the set instance. Differently from [17], we make an extensive use of cardinality networks [10] to encode constraints over the sets because they are handled more efficiently, for their nice arc-consistency properties. No action is required to encode a FlatZinc array into SMT-LIB, because it is used only as a container for other variables.

Floating-Point Precision. A consequence of encoding the FlatZinc int and float data-types with the linear arithmetic theory is that all of our computation is performed with infinite-precision arithmetic. This can result in a performance disadvantage wrt. other MiniZinc solvers using finite-precision arithmetic, due to the increased cost of each operation, but it has the benefit of guaranteeing the correctness of the final result of the computation.

Currently, the MiniZinc language does not allow one to express a certain quantity as an infinite-precision fraction between two constant numbers. Instead, the mzn2fzn compiler computes on-the-fly the result of any division operation between two constant integers or floating-point numbers applying the rules corresponding to the type of the operands. However, there are some instances in which we really need to be able to both express quantities and perform computation with infinite-precision arithmetic. One of such situations is to double-check the correctness of the MiniZinc models generated by the omt2mzn compiler described in Sect. 4 (we have done this for the experimental evaluations in Sect. 5.2). In order to get around this limitation we developed a simple wrapper around the mzn2fzn compiler, called emzn2fzn  [5], that replaces any fraction among two constant floats with a fresh variable and, after the basic mzn2fzn compiler generated the FlatZinc model, the emzn2fzn wrapper restores the original fractional values using the FlatZinc constraint float_div().

FlatZinc Constraints. The SMT-LIB encoding of the majority of FlatZinc constraints in OptiMathSAT follows their definition in the FlatZinc Standard, with the exception of Pseudo-Boolean constraints, which we examine in detail later on. Several global constraints are also supported in the same way, because the \(\text {OMT}\)-solver currently lacks ad hoc and efficient decision procedures for dealing with them. Constant values and alias variables (e.g. those arising from the definition of some arrays) are propagated through the formula, so as to keep the set of problem variables as compact as possible. Those constraints requiring non-linear arithmetic –like, e.g., trigonometric, logarithmic and exponential functions– are currently not supported; this situation may change soon due to the recent extension of MathSAT5 with a procedure for it [20].

Pseudo-Boolean Constraints. When dealing with Pseudo-Boolean sums of the form \(\sum _{i=1}^{i=N}A_i \cdot w_i\), where \(A_i\) is a Boolean variable and \(w_i\) is a numerical weight, the mzn2fzn compiler associates a fresh 0/1 integer variable \(x_i\) to each \(A_i\), and encodes the sum as \(\sum _{i=1}^{i=N}x_i \cdot w_i\). Notice that the original \(A_i\)s may not be eliminated from the FlatZinc model, because they typically occur elsewhere in the problem, i.e. as part of a Boolean formula. From our own experience, this situation arises frequently, because Pseudo-Boolean sums are typically used to express cardinality constraints that have a variety of uses. As described in [57], one limitation of this naive approach is that SMTand \(\text {OMT}\)solvers do not typically handle this encoding efficiently. The main reason is that the pruning power of the conflict clause resulting from a conflicting assignment is typically limited to one specific Boolean assignment at a time, meaning that a large number of conflict clauses (possibly exponential) has to be generated along the search. As shown in [57], SMTand \(\text {OMT}\)solvers can benefit from encoding Pseudo-Boolean constraints with cardinality networks.

fzn2omt goes through some effort in order to recognize Pseudo-Boolean sums over the integers, and replace the naive encoding with one based on cardinality networks. We note that using this technique generally results in a trade-off between solving time and the overhead of generating cardinality networks prior to starting the search, especially when dealing with a large number of variables.

Multi-objective Optimization. fzn2omt allows for multiple optimization goals, of heterogeneous type, being defined within the same FlatZinc model. This is a non-standard extension to the FlatZinc format. Multiple objectives can be solved independently from one another, or combined into a Lexicographic or Pareto optimization goal. We refer the reader to [58] for details on the input encoding and the solver configuration.

Functionality. Given a satisfiability or optimization problem encoded in the FlatZinc format, OptiMathSAT can be used in the following ways (Fig. 1):

  • to directly solve the problem, optionally enumerating any sub-optimal solution found during the search or all possible solutions with the same optimal value;

  • to produce an \(\text {OMT}\)problem encoded with the extended SMT-LIB format described in [58]. This problem can be directly solved with OptiMathSAT or, with minor transformationsFootnote 1, fed as input to other \(\text {OMT}\) solvers such as bclt and Z3.

4 From \(\text {OMT}\) to MiniZinc

In this section, we consider the problem of translating \(\text {OMT}\) formulas, encoded in the optimization-extended SMT-LIB format of [58], into MiniZinc models. Hereafter, we describe the main challenges we have faced and the solutions we have adopted. Further details about this conversion are available in [4].

General Translation Approach. The main challenge is to design an encoding from \(\text {OMT}\) to MiniZinc that is correct (i.e., it preserves in full the semantics of the input \(\text {OMT}\) problems), effective (i.e., it produces as output MiniZinc models which are as compact and easy-to-solve as possible), and efficient (i.e. it does it with the least consumption of time and memory). To this extent, one critical design choice is the way in which the internal representation of the input \(\text {OMT}\) formula is organized and converted in terms of MiniZinc primitives. After a preliminar experimental evaluation we determined that the sweet-spot, in terms of compactness and easiness to solve of the resulting MiniZinc model, is to adopt what we call “\(\ge \)2-father DAG-ification”: a Directed-Acyclic-Graph (DAG) internal representation of the formula where a fresh label is associated to all and only DAG nodes with at least two fathers, inlining all other nodes (see [24] for details).

Theories Restriction. The SMT-LIB standard describes a wide number of SMTtheories, most of which have no direct counterpart in MiniZinc due to the few data-types supported (see Sect. 2)). Hence, of linear rational and integer arithmetic, and their combination. On this regard, we note that even though omt2mzn can also handle the theory of bit-vectors, we do not cover it here because it is not used in the experimental evaluation in Sect. 5 (We cover it in the long version of this paper [24]). We leave the handling of other SMT theories to future work.

Linear Arithmetic Theory. On the surface, encoding linear arithmetic constraints coming from \(\text {OMT}\) in MiniZinc, using the int and float data-types, looks like a trivial task. In reality, this poses several challenges and it is subject to several limitations, due to a couple of facts.

First, in SMT-LIB the linear arithmetic theory requires the capability to perform infinite-precision computations. Unfortunately, to the best of our knowledge, no MiniZinc solver provides infinite-precision arithmetic reasoning, and the mzn2fzn compiler itself prevents representing arbitrarily-large and arbitrarily-precise quantities (e.g. the fine-grained decimal weights of the machine learning application in [59]).

Second, in \(\text {OMT}\) linear arithmetic variables are not required to be bounded and have quite often no explicit domain (i.e. they lack a lower-bound, an upper-bound or both), because it is not necessary for the problem at hand or it is implied by other constraints. This is in contrast with MiniZinc, whereby linear arithmetic variables are expected to have a finite domain and, when they lack one, their domain appears to be capped with some solver-dependent pair of values.

These restrictions are currently part of the MiniZinc language and the target application domain, and we do not see any obvious work-around solving them. We note that although there exist methods for bounding all variables in a given LP problem (e.g. [47]), these have been deemed too impractical at this stage of our investigation. Nonetheless, we have chosen to translate SMT-LIB linear arithmetic constraints with a corresponding MiniZinc encoding based on the int and float data-types. Although the encoding is not always applicable, it does still allow one to correctly translate a number of interesting \(\text {OMT}\) problems into MiniZinc, as witnessed by our experimental evaluation in Sect. 5.2. More in detail, the translation is done as follows. We declare each integer variable as unbounded, and then extend the MiniZinc model with the appropriate constraints bounding its domain when the input \(\text {OMT}\) formula contains any such information. Our empirical observation is that MiniZinc models generated in this way are correctly handed by all MiniZinc solvers which we have tried, with the exception of Gurobi, which returns an “unsupported” message. Floating-Point variables, instead, are always declared with a user-defined domain. This is because all of the MiniZinc solvers we have tried, among those that can handle floating-point constraints, require such information.

Other \(\text {OMT}\) Functionalities. Several problems of \(\text {OMT}\) interest require the capability of dealing with soft-constraints (i.e. Weighted MaxSMT) and also with multiple objectives, that are either considered independent goals or combined in a Lexicographic or Pareto-like fashion. To the best of our knowledge, the MiniZinc standard does not allow for an explicit encoding of soft-constraints, nor to deal with more than one objective function at a time.

We encode (weighted) MaxSMT problems using a standard Pseudo-Boolean encoding, such as the one used in [53]. When dealing with \(\text {OMT}\) problems that contain N goals \(\mathsf{obj} _1, ..., \mathsf{obj} _N\), for \(N > 1\), we use the following approach. If these objectives are independent targets, we generate N MiniZinc models, each with a different goal \(\mathsf{obj} _i\), and separately solve each model. If instead the multiple objectives belong to a Lexicographic \(\text {OMT}\) problem, then we generate a unique MiniZinc model that leverages the lexicographic-optimization functionality provided by MiniSearch [49]. (In all other cases, MiniSearch is not used). We do not have any encoding for dealing with Pareto-optimization, yet.

5 Experimental Evaluations

In this section we present an extensive empirical evaluation comparing \(\text {OMT}\) tools with many state-of-the-art CP tools on CP problems coming from the MiniZinc challenge (Sect. 5.1), and on \(\text {OMT}\) problems coming mostly from formal verification (Sect. 5.2).

The \(\text {OMT}\) solvers under evaluation are bclt, OptiMathSAT (v. 1.6.0) and Z3 (v. 4.8.5). These are compared with some of the top-scoring solvers that participated at recent editions of the MiniZinc challenge, including Choco (v. 4.0.4), Chuffed, G12(fd) (v. 1.6.0), Gecode (v. 6.0.1), Gurobi (v. 8.0.1), HaifaCSP (v. 1.3.0), JaCoP (v. 4.5.0), iZplus (v. 3.5.0), OR-Tools (v. 6.7.4981) and Picat (v. 2.4).

Remark 1

We could not include fzn2smt [17, 18] in our experimental evaluation because it is not compatible with the features of MiniZinc that have been added since version 2.0.

We run all these experimental evaluations on two identical 8-core 2.20 Ghz Xeon machines with 64 GB of RAM and running Ubuntu Linux. All the benchmark-sets, the tools and the scripts used to run these experiments, and some of the plots for the results in Tables 1, 2 and 3 which could not fit into this paper, can be downloaded from [2].

We stress the fact that the goal of these experiments is not to establish a winner among \(\text {OMT}\) and MiniZinc tools; rather, it is to assess the correctness, effectiveness and efficiency of our \(\text {OMT}\)-to-CP and CP-to-\(\text {OMT}\) encoders and, more generally, to investigate the feasibility of solving MiniZinc problems with \(\text {OMT}\) tools and vice versa, and to identify the criticalities in terms of efficiency and correctness in these processes.

5.1 Evaluation on MiniZinc Benchmark Sets

We consider the benchmark-sets used at the MiniZinc Challenge of 2016 (MC16) and 2019 (MC19), each comprised by 100 instances. For compatibility reasons, the version of mzn2fzn used to convert the problems to the FlatZinc format differs between the two benchmark-sets. We use version 2.2.1 and 2.3.2 (with patches) for the problems in MC16 and MC19 respectively. Due to recent changes in the FlatZinc format that affect the benchmarks in MC19, the version of some MiniZinc tools differs from what described in Sect. 5 (see Table 1). In some cases, we had to download and compile the latest source available for the tool, i.e. the “nightly” version.

We run each MiniZinc solver with the corresponding directory of global constraints, and we run each MiniZinc and \(\text {OMT}\) tool with the default options. We consider two \(\text {OMT}\) encodings of the original FlatZinc problems, la and bv. The first encodes the FlatZinc int type with the theory of linear integer arithmetic, whereas the second is based on the theory of bit-vectors. We evaluate each \(\text {OMT}\) solver on both SMT-LIB encodings, except for bclt that has no support for bit-vector optimization. For uniformity reasons with the other \(\text {OMT}\) solvers, we evaluate OptiMathSAT using its SMT-LIB interface only, using thus its fzn2omt interface as an external tool, like with the other \(\text {OMT}\)solvers. We note that the solving time for all \(\text {OMT}\) solvers includes the time required for translating the formula from the FlatZinc to the SMT-LIB format. Each solver, either \(\text {OMT}\) or MiniZinc, is given up to 1200s. to solve each problem, not including the time taken by mzn2fzn to flatten it.

We verify the correctness of the results by automatically checking that all terminating solvers agree on the (possibly optimal) solution and, when this is not the case, we manually investigate the inconsistency.

Table 1. MiniZinc Challenge formulas. The columns list the total number of instances (inst.), of timeouts (timeout), of run-time errors (error), of unsupported problems (unsup.), of incorrectly solved instances (incor.), of correctly solved instances (correct), the total solving time for all solved instances (time), the number of instances solved in the shortest time within the same category (BT1) and those solved in the shortest time considering all tools (BT2).
Full size table

Experiment Results. The results of this experiment are shown in Table 1, with separate numbers for satisfiability (s) and optimization (o) instances in each benchmark-set. Using the experimental data, we separately computed the virtual best configuration among all MiniZinc solvers (i.e. virtual best(MiniZinc)), all \(\text {OMT}\) solvers (i.e. virtual best(\(\text {OMT}\))), and also the virtual best among all tools considered in the experiment (i.e. virtual best(all)). The last two columns in the table list the number of problems solved by the given configuration in the same amount of time as the virtual best() of each group (col. BT1) and as the virtual best(all) (col. BT2).

We start by looking at the MiniZinc solvers in Table 1. The performance ladder is dominated by OR-Tools(sat) and Picat(sat), closely followed by Gurobi, HaifaCSP and Chuffed (in MC19). By looking at column BT1, we observe that the top-performing MiniZinc solvers tend to dominate over all the others. Looking at the results of the MC19 experiment, we notice a significant increase in the number of errors with respect to the benchmark-set of the MC16 edition, as well as a handful of problems solved incorrectly. In the case of Gurobi and Picat(sat), the mzn2fzn compiler encountered an error over a few instances. As a consequence, the total number of problems is smaller than 100 for both tools. After taking a closer look, we ascribe this phenomenon to the recent changes in the MiniZinc/FlatZinc format, that has created some minor issues with some tools that have not been adequately updated.

Looking at the \(\text {OMT}\) tools only, we observe that Z3 has leading performance over the other solvers. When compared to the MiniZinc solvers, the \(\text {OMT}\) solvers place themselves in the middle of the rank on both benchmark-sets. Given the fact that none of the \(\text {OMT}\) solvers has specialized procedures or encodings for dealing with global constraints, we consider this an interesting result.

5.2 Evaluation on \(\text {OMT}\) Benchmark Sets

In this experimental evaluation we use \(\text {OMT}\) formulas taken from well-known, publicly available, repositories. We characterize these benchmark-sets as follows:

  • SAL [integers]: 66 SMT-based Bounded Model Checking and K-Induction parametric problems created with the SAL model checker [6];

  • SAL [rationals]: as above, with problems on the rationals;

  • Symba [rationals]: 2632 boundedFootnote 2 software verification instances derived from a set of C programs used in the Software Verification Competition of 2013 [36];

  • Jobshop and Strip Packing [rationals]: 190 problems taken from [51, 53];

  • Machine Learning [rationals]: 510 \(\text {OMT}\)instances generated with the pyLMT tool based on Machine Learning Modulo Theories [59].

The first benchmark-set is on the integers, whereas the other four are on the rationals. We stress the fact that all formulas contained in all benchmark-sets are satisfiable.

Remark 2

Although there exists a repository of multi-objective \(\text {OMT}\) formulas (e.g. [36, 56]), we have chosen to not include these in our experimental evaluation. The reason for this is twofold. First, such comparison would likely be unfair wrt. CP tools because that the workaround for dealing with multi-independent \(\text {OMT}\) formulas described in Sect. 4 is not competitive with the integrated optimization schema provided by \(\text {OMT}\) solvers [36, 56]. In fact, the experimental evidence in [36, 56] collected on a group of \(\text {OMT}\) solvers indicates that the latter approach can be an order of magnitude faster than the former one. Second, the workaround for dealing with lexicographic-optimization is limited by the fact that MiniSearch is not fully compatible with recent versions of MiniZinc, and it only works with a restricted set of tools.

We have used the omt2mzn tool described in Sect. 4 to translate each \(\text {OMT}\) formula to the MiniZinc format. omt2mzn is written in Python and it is built on top of pySMT [30], a general-purpose Python library for solving SMT problems, and it is available at [4]. During this step, it has been necessary to impose a finite domain to any unconstrained SMT-LIB rational variable, because otherwise none of the MiniZinc solvers would have been able to deal with them. We have experimented with two different domains: the largest feasible domain for floating-point variables of 32 bits (i.e. \(\pm 3.402823e+38\)) for the first two benchmark-sets, and the largest feasible domain for integer variables (i.e. \(\pm 2^{31}\)) for the last two.

We consider two OptiMathSAT configurations: OptiMathSAT (smt), solving the original \(\text {OMT}\)formulas, and OptiMathSAT (fzn), executed on the generated MiniZinc instances. The benefits of this choice is two-fold. First, we can double-check the correctness of such encoding, by comparing the optimum models generated in the two cases. Second, we can verify whether there is any performance loss caused by the encoding of the formula.

Only four of the MiniZinc solvers listed in Sect. 5 support floating-point reasoning. This limited the number of tools that could be used with some \(\text {OMT}\) benchmark-sets. The running-time of each MiniZinc solver reported in these experiments (including OptiMathSAT (fzn)) is comprehensive of the time taken by the mzn2fzn compiler, because the latter can sometime solve the input formulas on its own. The overall timeout is set to 600 s.

Notice that the optimal solutions found by OptiMathSAT (smt) have been previously independently verified with a third-party SMT tool as reported in previous publications [55,56,57].Footnote 3 Therefore, we verify the correctness of the results found by any other configuration by comparing them with those found by OptiMathSAT (smt), and otherwise mark the result as “unverified”.

Table 2. SAL over integers. A sat result is marked as correct when the objective value matches the reference solution provided by OptiMathSAT (smt) (when run without a timeout), as incorrect otherwise.
Full size table
Table 3. \(\text {OMT}\) Problems defined over the rationals. A sat result is marked as correct when the objective value matches the reference solution provided by OptiMathSAT (smt) with an absolute error \(\varDelta < 10^{-6}\). A result is marked as unverified when we have no reference solution and incorrect if neither of the previous two conditions apply.
Full size table

Experimental Results over the Integers. In this experiment, we evaluate the SAL (over integers) benchmark-set. The results are collected in Table 2.

We notice first that OptiMathSAT (fzn) always produces correct results and it shows comparable performances in terms on number of problems solved wrt. the baseline OptiMathSAT (smt), solving even 4 problems more. (We conjecture that the latter fact should be attributed to the limited, but effective, deduction capabilities of the mzn2fzn compiler, that may have helped OptiMathSAT in solving the input formulas.) This suggests that, at least on problems on the integers, omt2mzn is efficient and effective and does not affect correctness.

In general, MiniZinc solvers do not seem to deal efficiently with this benchmark-set. Some tools have experienced some internal error (e.g. dumped-core, segmentation fault), some others have been killed to a high memory consumption (over 32GB), whereas the majority of the remaining tools had a timeout.

We explain this behavior with the fact that the given benchmark set is characterized by the presence of a heavy Boolean structure combined with arithmetical constraints, which requires the efficient combination of strong Boolean-reasoning capabilities (e.g., efficiently handling chains of unit propagations) with strong arithmetical-solving&optimization capabilities, which is a typical feature of \(\text {OMT}\) solvers.

None of the input formulas was initially supported by Gurobi. After restricting the bound of every integer variable to \(\pm 10^6\), Gurobi(l) was able to solve 3 instances within the timeout. Among the MiniZinc solvers, the best result is obtained by Picat(sat), that solved 4 problems out of 66.

Experimental Results Over the Rationals. We consider first the first three benchmark-sets over the rationals: SAL over rationals, Symba, JobShop&Strip-Packing. (Separate tables for the four benchmarks are reported in the extended version of this paper [24].) Of all MiniZinc solvers we have tried, only three are able to deal with floating-point constraints. The results are shown in Table 3. Since each of the input formulas is satisfiable, we consider a result incorrect either when it is equal to unsat, or when the relative error \(\varDelta \) exceeds \(10^{-6}\), s.t.: , \(o_{smt}\) and \(o_{fzn}\) being the optimal value found by OptiMathSAT (smt) and the optimal value found by the MiniZinc solver under test respectively. (Recall that the former was previously checked to be correct.)

Similarly to the previous experiment on the integers, OptiMathSAT (fzn) always produces correct results, and display comparable performance wrt. OptiMathSAT (omt) in terms of number of instances being solved, solving somewhat fewer problems. This is not the case of the other three MiniZinc solvers. Among these, Gecode experienced a timeout on the majority of the formulas being considered, G12(mip) returned mostly incorrect answers, whereas Gurobi seems to have the best performance, in particular on the third benchmark-set.

We attribute the large number of incorrect results returned by all three MiniZinc solvers to the fact that these tools use finite-precision floating-point arithmetic internally. The incorrect behavior of some of these solvers (e.g. Gurobi) can also be partially explained with the large domain of floating-point variables in these problems. However, given the nature of these input instances, it was not possible for us to assign a smaller domain to each variable in the problem a priori.

We analyze separately the results for the last benchmark-set reported in Table 3. The peculiar aspect of the Machine Learning benchmark-set [59] is that it is characterized by Pseudo-Boolean sums over rational weights, and by very fine-grained rational valuesFootnote 4. Unfortunately, these fine-grained rational values are rounded by the standard mzn2fzn compiler, which causes the incorrect results even of OptiMathSAT (fzn) in Table 3, despite the fact that OptiMathSAT uses infinite-precision arithmetic.

In order to overcome this issue, we leverage the emzn2fzn compiler described in Sect. 3 so that the original fractional values are preserved in the resulting FlatZincmodel, and show that with this approach OptiMathSAT does not produce incorrect results any longer (configuration OptiMathSAT (fzn+e) in Table 3), solving correctly 152 problems more than OptiMathSAT (fzn).

Overall, since there are at least 237 formulas affected by the above issue with the mzn2fzn compiler, we avoid an in-depth discussion of the results obtained by the other MiniZinc solvers. However, at a first glance the situation does not seem to differ from the other benchmark-sets over the rationals.

5.3 Discussion

On the whole, from our experiments, \(\text {OMT}\) tools appear to be still at some disadvantage when dealing with MiniZinc problems wrt. specific tools, and vice versa.

On the one hand, \(\text {OMT}\) solvers seem to be penalized by their lack of efficient ad hoc decision procedures for dealing with global constraints. Moreover, the approach taken by the mzn2fzn compiler, that creates lots of alias Boolean, integer and floating-point variables for dealing with Pseudo-Boolean constraints, is particularly challenging to deal with efficiently by an \(\text {OMT}\)solver.

On the other hand, MiniZinc solvers seem to suffer with problems needing an arithmetic-reasoning component combined with heavy Boolean-reasoning component. Even more importantly, the lack of infinite-precision linear arithmetic procedures causes a number of incorrect results when dealing with \(\text {OMT}\) problems over the rationals. Both of these points need to be addressed in order to deal with the vast number of Formal Verification and Model Checking applications in the SMT/\(\text {OMT}\) domain.

6 Conclusions and Future Work

In this paper we have taken a first step forward towards bridging the MiniZinc and the \(\text {OMT}\) communities. The ultimate goal is to obtain a correct, effective and efficient fully-automated system for translating problems from one community to the other, so as to extend the application domain of both communities. With our experimental evaluation, we have identified some criticalities that need to be addressed by each community in order to solidify this union.

We plan to push this investigation forward as follows. In the short term, we plan to address the inefficient handling of Pseudo-Boolean constraints over the rationals revealed by the experimental evaluation in Sect. 5.2. In order to deal with those FlatZinc constraints that require non-linear arithmetic, we envisage an opportunity to either extend OptiMathSAT with proper handling of the non-linear arithmetic theory [20] or to experiment with an encoding based on the floating-point theory [60]. This objective goes hand in hand with the extension of omt2mzn to deal with other SMT theories. In the long term, \(\text {OMT}\) solving may also benefit from adopting efficient ad hoc decision procedures for frequently used global constraints. Finally, we plan to broaden the scope of our investigation and include other \(\text {OMT}\) solvers in our study.