Optimization Modulo Theories (OMT) is an extension of SMT, which allows for finding models that make a given objective optimal through a combination of SMT and optimization procedures [18,11,12,20,21,14,15,9,10,23,22]. Latest advancements in OMT have further broadened its horizon by making it incremental [9,23] and by supporting objectives defined in other theories than linear arithmetic (e.g. Bit-Vectors) [9,10,16]. Moreover, OMT has been extended with the capability of handling multiple objectives at the same time either independently or through their linear, min-max/max-min, lexicographic or Pareto combination [9,10,23].
An important sub-case of OMT is (partial weighted1 ) MAXSMT-or alternatively OMT with Pseudo-Boolean objective functions [19]- [18,11,12], which is the problem of finding a model for an input formula which both satisfies all hard clauses and maximizes the cumulative weight of all soft clauses made True by the model.
Two main approaches for MAXSMT have been adopted in the literature.
One approach is to embed some MAXSAT engine within the SMT solver itself, and use it in combination with dedicated T -solvers [4,12,9,10]. Although this approach can be very efficient, it has some limitations that make it an impractical choice in some cases.
The first issue is that, to the best of our knowledge, MAXSAT engines deal with integer weights only. However, some applications, e.g., Learning Modulo Theories [25] -a hybrid Machine Learning approach in which OMT is used as an oracle for Support Vector Machines [25]-may require the weight of soft-constraints to be high-precision rational values. In this context, it is preferable not to round the weights associated with soft-clauses since it affects the accuracy of the Machine Learning approach.
The second drawback is that a MAXSAT engine cannot be used when dealing with an OMT problem with multiple-independent objectives that need to be optimized at the same time, or when the objective function is given by either a linear combination of Pseudo-Boolean and arithmetic terms (like, e.g., for Linear Generalized Disjunctive Programming problems [21]) or a non-trivial combination of several Pseudo-Boolean sums as in [25].
An alternative approach for dealing with MAXSMT is to encode it as a Pseudo-Boolean objective in Optimization Modulo Theories [21] which, for the above reasons, is the approach adopted in OPTI-MATHSAT [1].
We notice that, unfortunately, compared with the use of a dedicated MAXSAT engine, this second approach might result in poor performance when dealing with MAXSMT problems in which a large number of soft-clauses are assigned the same weight. In fact, this situation entails the existence of symmetries in the solution space that might lead to a combinatorial explosion of the partial truth assignments generated by the CDCL engine during the optimization search.
In this paper we analyze the sources of this inefficiency and describe and evaluate a solution based on sorting networks, which we implemented on top of OPTIMATHSAT. The benefits of applying this technique are shown with an experimental evaluation based on two OMT applications, performed on benchmarks sets coming from the Requirement Engineering and Machine Learning domain.
Related Work. The idea of MaxSMT and, more generally, of optimization in SMT was first introduced by Nieuwenhuis & Oliveras [18], who presented a general logical framework of "SMT with progressively stronger theories" (e.g., where the theory is progressively strengthened by every new approximation of the minimum cost), and presented implementations for MaxSMT based on this framework. Cimatti et al. [11] introduced the notion of "Theory of Costs" C to handle Pseudo-Boolean (PB) cost functions and constraints by an ad-hoc and independent "C-solver" in the standard lazy SMT schema, and implemented a variant of MathSAT tool able to handle SMT with PB constraints and to minimize PB cost functions. Ansótegui et al. [4] described the evaluation of an implementation of a MaxSMT procedure based on YICES, although this implementation is not publicly available. Cimatti et al. [12] presented a "modular" approach for MaxSMT, combining a lazy SMT solver with a MaxSAT solver, which can be used as black-boxes, where the SMT solver is used as an oracle generating T -lemmas that are then learned by the MAXSAT solver so as to progressively narrow the search space toward the optimal solution.
Sebastiani and Tomasi [20,21] introduced a wider notion of optimization in SMT, namely Optimization Modulo Theories (OMT) with linear cost functions on the rationals, OMT(LRA∪T ), which allows for finding models minimizing some LRA cost term -T being some (possibly empty) stably-infinite theory s.t. T and LRA are signature-disjoint 2 , and presented novel OMT(LRA ∪ T ) tools which combine standard SMT with LP minimization techniques. Eventually, OMT(LRA ∪ T ) has been extended so that to handle costs on the integers, incremental OMT, multi-objective and lexicographic OMT and Pareto-optimality [15,14,9,23,10,22]. To the best of our knowledge only four OMT solvers are currently implemented: BCLT [14], OPTIMATHSAT [23,22], SYMBA [15] and νZ [9,10]. Remarkably, νZ [9,10] implements specialized procedures for MaxSMT, leveraging to SMT level various state-of-the-art MaxSAT procedures. In addition to it, νZ features a Pseudo-Boolean T -solver which can generate sorting networks on demand for Pseudo-Boolean inequalities featuring sums with small coefficients when a Pseudo-Boolean inequality is used some times for unit propagation/conflicts [10,8].
Importantly, both partial weighted MAXSMT and SMT with PB objectives can be encoded into OMT(LRA ∪ T ), whereas the contrary is not possible [20,21].
Content. The paper is structured as follows. The background and the state of the art are briefly reviewed in section §2, whereas section §3 describes the source of inefficiency arising when partial weighted MAXSMT is encoded in OMT as in [21]. Section §4 illustrates a possible solution based on sorting networks, whereas in §5 we provide empirical evidence of the benefits of this approach on two applications of OMT interest. Section §6 concludes the paper with some considerations on the future work.
Optimization Modulo Theories is an extension of SMT which addresses the problem of finding a model for an input formula ϕ which is optimal wrt. some objective function obj [18].
The basic minimization scheme implemented in state-of-the-art OMT solvers, known as linearsearch scheme [20,21], requires solving an SMT problem with a solution space that is progressively tightened by means of unit linear constraints in the form (obj < ub i ), where ub i is the value of obj that corresponds to the optimum model of the most-recently found truth assignment µ i s.t. µ i |= ϕ. The ub i value is computed by means of a specialized optimization procedure embedded within the T -solver of interest that, taken as input a pair µ, obj , returns the optimal value ub of obj for such µ. The OMT search terminates when the latter procedure finds that obj is unbounded or when the SMT search is UNSAT, in which case the latest value of obj (if any) and its associated model M i is returned as optimal solution value. (Alternatively, binary-search schemes can also be used [20,21].)
An important subcase of OMT is that of MAXSMT, which is a pair ϕ h , ϕ s , where ϕ h denotes the set of "hard" T -clauses, ϕ s is a set of positive-weighted "soft" T -clauses, and the goal is to find the maximum-weight set of [18,11,4,12]. As described in [21], MAXSMT ϕ h , ϕ s can be encoded into a general OMT problem with a Pseudo-Boolean objective. To do so, one first introduces a fresh Boolean variable A i for each soft-constraint
and then encodes the problem into OMT as a pair ϕ, obj where ϕ is defined as
Notice that, although redundant from a logical perspective, the constraints in (3) serve the important purpose of allowing early-pruning calls to the LRA-Solver (see [6]) to detect a possible LRA inconsistency among the current partial truth assignment over variables A i and linear cuts in the form (obj < ub) that are pushed on the formula stack by the OMT solver during the minimization of obj. To this extent, the presence of such constraints improves performance significantly.
Consider first the case of a MAXSMT-derived OMT problem as in equation (1) s.t. all weights are identical, that is: let ϕ, obj be an OMT problem, where obj = i=n−1 i=0
w • A i , A i being Boolean variables, and let µ be a satisfiable truth assignment found by the OMT solver during the minimization of obj.
As described in [20,21], the OMT solver adds a unit clause in the form (obj < ub) in order to (1) remove the current truth assignment µ from the feasible search space and (2) seek for another µ which improves the current upper-bound value ub. Importantly, the unit clause (obj < ub) does not only prune the current truth assignment µ from the feasible search space, but it also makes inconsistent any other possible (partial) truth assignment µ which sets exactly k (or more) A i variables to True. Thus, each new unit clause in this form prunes at least γ = n k truth assignments from the search space, where γ is equal to the cardinality of the set of possible permutations of µ over the variables A i .
However, the inconsistency of a truth assignment µ which sets exactly k variables to True wrt. a unit clause (obj < ub), where ub = w • k, can not be determined by simple Boolean Propagation. In fact, (obj < ub) being a LRA term, the CDCL engine is totally oblivious to this inconsistency until when the T -solver for linear arithmetic is invoked, and a conflict clause is generated. Therefore, since the T -solver for linear arithmetic is more resource demanding than Boolean Propagation and is invoked less often, it is clear that the performance of an OMT solver can be negatively affected when dealing with this kind of objectives.
To conclude, notice that the performance issue identified with the previous case example can be generalized to any objective obj in the form
where the logically-redundant constraints (0 ≤ τ j ) ∧ (τ j ≤ w j • k j ) are added for the same reason as with (3).
A solution for improving search efficiency when dealing with MAXSMT and OMT with Pseudo-Boolean objectives in the form
is to reduce the dependency on the expensive LRA-Solver by better exploiting Boolean Constraint Propagation (BCP) with the aid of sorting networks.
A sorting-network relation, depicted in figure 1, takes A 0 , ..., A n−1 Boolean variables as input and returns out 0 , ..., out n−1 variables as output s.t., if in the current (partial) truth assignment µ, k variables are set to True, n − m variables are set to False and m − k are unassigned, then by Boolean Constraint Propagation out 0 , ..., out k−1 are set to True, out m , ..., out n−1 are set to False and out k , ..., out m−1 are not propagated.
For our purposes, it is important that the implementation of the relation is bidirectional: e.g., if out k−1 is forced to be True (that is, at least k inputs must be True) and n − k inputs A i are False, then by Boolean Propagation all other unassigned A i s are automatically set to True; vice-versa, if out k+1 is forced to be False (that is, at most k inputs can be True) and n − k inputs A i are True, then all other unassigned A i s are automatically set to False.
Given an OMT problem ϕ, obj, , where obj is as in (7), and a sorting network relation encoding C matching the previous definition, we extend ϕ in equation (2) as follows: The benefit of this extension is that now, whenever the optimization search finds a new satisfiable truth assignment µ which sets k variables A i to True, so that a unit clause in the form (obj < k • w) is learned, then as soon as k − 1 inputs A i are assigned to True the remaining n − k + 1 inputs are set to False by BCP. (A dual case occurs when some lower-bound unit clause (obj > k • w) is learned.)
In our work, we have considered two encodings for the sorting network relation: the sequential counter encoding [24] and the cardinality network encoding [3]. Notice that, in contrast with the literature which usually focuses on only one direction of cardinality constraints, in our context we are interested in a bidirectional encoding of sorting circuit so to ensure the correct propagation of the out k values. This is due to the fact that our OMT solver applies this technique to deal not only with MaxSMT problems but also with Pseudo-Boolean objectives that can be either minimized or maximized, and other Pseudo-Boolean sums subject to simple cardinality constraints outside of an optimization context.
The sequential counter encoding LT n,k SEQ for ≤ k(A 0 , ..., A n−1 ) presented in [24] requires O(k • n) clauses and variables to be represented, and is arc-consistent. The circuit is given by the composition of n sub-circuits, each of which computes s i = j=i j=0 A j , represented in unary form with the bits s i,j . The following formula is the original propositional encoding of LT n,k SEQ presented in [24], with k instantiated to n, which was obtained after discarding one direction of the equations for polarity reasons.
We strengthened the original encoding with the following clauses to make it bidirectional:
The cardinality network encoding presented in [13,5,3], based on the underlying sorting scheme of the well-known merge-sort algorithm, has complexity O(n log 2 k) in the number of clauses and variables, and is arc-consistent. Due to space limitations, we refer the reader to [3] for the encoding of cardinality networks we used in our own work. Notice that, differently than in the previous case, this sorting circuit propagates values in both directions and is thus suitable to be used as is within OMT.
Both of the previous encodings are istantiated assuming k = n, since the sorting network is generated prior to starting the search. Therefore, the cardinality network circuit looks more appealing than the sequential counter encoding due to its lower complexity in terms of clauses and variables employed.
To conclude, note that this approach based on sorting networks can also be applied when dealing with more general Pseudo-Boolean objectives as in equations 5, 6. In this case a separate sorting circuit is generated for each term τ j , and some (optional) constraints in the form (obj < w j •i) =⇒ (τ j < w j •i), for i ∈ [0, k j ], can be added to ensure that the circuit is activated by BCP.
As part of our research work, we extended OPTIMATHSAT with a novel preprocessing step for dealing with assert-soft constraints (see [22]) which automatically extends the input formula with a sorting network circuit of choice among the sequential counter and the cardinality network. We recall here that, in OPTIMATHSAT, the assert-soft statement can be used not only to encode MAXSMT problems like in νZ, but also generic Pseudo-Boolean terms that can be linearly combined into other constraints or objective functions.
In the following experiments 3 we evaluate whether the speed-up obtained by extending the input formula with a sorting network during the optimization search can outweigh the cost of its generation step within the OMT solver itself, as opposed to demanding the end-user to do it offline.
Each test was performed on a pair of identical Ubuntu Linux machines featuring 8-core Intel-Xeon@2.20GHz CPU, 64 GB of ram and kernel 3.8-0-29.
In our first experiment, we focused on a benchmark database consisting of 18996 formulas, automatically generated, derived from the problem of computing the optimal realization of a constrained goal model enriched with soft-requirements [17], one of OPTIMATHSAT applications in the context of Requirement Engineering. Each OMT problem contains a combination of up to three MAXSMT objectives sorted with lexicographic priority. In this experiment, we set the timeout at 100 seconds and we verified that all the tested configurations agreed on the optimum value.
As it can be seen in the top table of figure 2, extending the input formula with either of the sorting network circuits increases the number of benchmarks solved within the time-out.
Notably, the cardinality network encoding -which has the lowest complexity-scores the best both in terms of number of solved benchmarks and solving time. On the other hand, the sequential counter circuit is affected by a significant performance hit on a number of benchmarks, as it is witnessed by the bottom-left scatter plot in figure 2. This not only affects unsatisfiable benchmarks, for which using sorting networks appears to be not beneficial in general, but also satisfiable ones.
A possible strategy for overcoming this performance issue is to reduce the memory footprint determined by the generation of the sorting network circuit. This can be easily achieved by splitting each Pseudo-Boolean sum in smaller sized chunks and generating a separate sorting circuit for each splice.
The result of applying this enhancement, using chunks of increasing size, is shown in figure 3. Both the table and the scatter plots suggest that the sequential counter encoding can greatly benefit from this simple heuristic, since both the number of solved benchmarks and the running time improve to levels comparable with that achieved using the cardinality network circuit.
As suggested by one of the reviewers, we extended our experimental evaluation to include νZ. The results are shown in the top table of figure 2. Although νZ is able to solve the whole benchmark set in a very short amount of time using the MaxRes MAXSMT engine, OPTIMATHSAT and νZ disagree on the optimal solution of a number of benchmarks. Further investigation confirmed that in some cases νZ returns an incorrect optimum model when dealing with multiple MAXSMT combined lexicographically. Figure 2: Top: Results on MAXSMT problems using the OMT encoding in [21] (top), paired with the Boolean cardinality constraint encoding in [24] (middle) and in [3] (bottom). Bottom: performance gain obtained by joining the input formula with the sequential counter circuit (left) and the cardinality network encoding (right); brown colour denotes unsatisfiable benchmarks, blue represent satisfiable ones and green represents timeouts.
The second experiment regards a set of problems taken from PYLMT [2], a tool for Structured Learning Modulo Theories [25] which uses OPTIMATHSAT as back-end oracle for performing inference in the context of machine learning in hybrid domains. Starting from the original set of 500 satisfiable formulas, which used a naive encoding of Pseudo-Boolean objectives by default, we generated a new benchmark set which uses the assert-soft statement to encode the following objective function given by a non-trivial combination of several Pseudo-Boolean terms.
We ran both νZ and OPTIMATHSAT over the original set of benchmarks, and compared the following three configurations for OPTIMATHSAT over the assert-soft based benchmark set: orig. enc., which maps the input weighted MAXSMT formula into an OMT problem with no circuit, seq. counter enc., which extends the input formula with the sequential counter encoding, and card. network enc. which uses instead the cardinality network encoding. We imposed a timeout of 600 seconds for both tools, and verified that all solvers and their configurations -when terminating-agreed on the optimal solution values.
The results, depicted in figure 4, show that extending the input problems with sorting network circuits benefits the number of solved benchmarks within the timeout, with the cardinality network encoding performing better by a small margin. As highlighted by the scatter plots in the bottom part of figure 4, generating these circuit on the fly causes a limited overhead on easy benchmarks, whereas it can significantly improve the running time on difficult ones.
MAXSMT is an important sub-case of Optimization Modulo Theories for which specialized algorithms and techniques have been developed over the years. Nonetheless, when dealing with non trivial combination of multiple objectives or problems with fine grained weights over soft-clauses, MAXSMT might require being encoded as a Pseudo-Boolean objective and solved with ordinary OMT techniques.
In this paper we reviewed the encoding of MAXSMT in OMT proposed in [21] and described a possible inefficiency problem that might arise when dealing with problems in which a large number of soft-clauses share the same weight value, due to the resulting symmetries in the solution space. In order to overcome this issue, we proposed a transparent solution based on extending the input problem with two different sorting networks: the sequential counter circuit and the cardinality constraint encoding. The benefits of this technique have been demonstrated through an experimental evaluation on a couple of benchmark sets coming from the domain of Requirement Engineering and Machine Learning.
Albeit of the positive results attained, this is still work in progress, and future work should focus on how to extend this technique to better handle similar performance issues when dealing with more heterogeneous sets of weights values.