Generalized Optimization Modulo Theories
Nestan Tsiskaridze Clark Barrett Cesare Tinelli





Generalized Optimization Modulo Theories







N. Tsiskaridze et al.



Stanford University,
  Stanford, California, USA

{nestan,barrett}@cs.stanford.edu


The University of Iowa,
   Iowa City, Iowa, USA

cesare-tinelli@uiowa.edu



Generalized Optimization Modulo Theories
    Nestan Tsiskaridze10000-0002-4729-9770
Clark Barrett10000-0002-9522-3084
Cesare Tinelli20000-0002-6726-775X
    
===============================================================================================================




Optimization Modulo Theories (OMT) has emerged as an important extension of the highly successful Satisfiability Modulo Theories (SMT) paradigm.  The OMT problem requires solving an SMT problem with the restriction that the solution must be optimal with respect to a given objective function.
We introduce a generalization of the OMT problem where, in particular, objective functions can range
over partially ordered sets.
We provide a formalization of and an abstract calculus for the generalized OMT problem and prove their key correctness properties. Generalized OMT extends previous work on OMT in several ways. First, in contrast to many current OMT solvers, our calculus is theory-agnostic, enabling the optimization of queries over any theories or combinations thereof. Second, our formalization unifies both single- and multi-objective optimization problems, allowing us to study them both in a single framework and facilitating the use of objective functions that are not supported by existing OMT approaches. Finally, our calculus is sufficiently general to fully capture a wide variety of current OMT approaches (each of which can be realized as a specific strategy for rule application in the calculus) and to support the exploration of new search strategies. Much like the original abstract DPLL(T) calculus for SMT, our Generalized OMT calculus is designed to establish a theoretical foundation for understanding and research and to serve as a framework for studying variations of and extensions to existing OMT methodologies.











§ INTRODUCTION


Over the past decade, the field of Optimization Modulo Theories (OMT) has emerged, inspiring the interest of researchers and practitioners alike. OMT builds on the highly successful Satisfiability Modulo Theories (SMT) <cit.> paradigm and extends it: while the latter focuses solely on finding a theory model for a first-order formula, the former adds an objective term that must be optimized with respect to some total ordering over the term's domain.

The development of OMT solvers has fostered research across an expanding spectrum of applications, including scheduling and planning with resources <cit.>,

formal verification and model checking <cit.>, program analysis <cit.>, 
requirements engineering and specification synthe­sis <cit.>, 
security analysis <cit.>, 

system design and configuration <cit.>, 


machine learning <cit.>, and quantum annealing <cit.>. 

Various OMT procedures have been developed for different types of optimization objectives (e.g., single- and multi-objective problems), underlying theories (e.g., arithmetic and bitvectors), and search strategies (e.g., linear and binary search). 
We provide an overview of established OMT techniques in Section <ref>.
An extensive survey can be found in Trentin <cit.>. 


We introduce a proper generalization of the OMT problem and
describe a novel abstract calculus for this generalization whose main goal is similar to that of the DPLL(T) calculus for SMT <cit.>: to provide both a foundation for theoretical understanding and research and a blueprint for practical implementations. 
The calculus is general in several ways. 
First, in contrast to previous work in OMT, it is parameterized by the optimization order, which does not need to be total, and it is not specific to any theory or optimization technique, making the calculus easily applicable to new theories or objective functions.
Second, it encompasses both single- and multi-objective optimization problems, allowing us to study them in a single, unified framework and enabling combinations of objectives not covered in previous work. 
Third, it captures a wide variety of current OMT approaches, 
which can be realized as instances of the calculus together with specific strategies for rule application.  
Finally, it provides a framework for the exploration of new optimization strategies.



  
Contributions
To summarize, our contributions include:


    
  * a formalization of a generalization of OMT to partial orders that unifies traditional single- and multi-objective optimization problems;
    
  * a theory-agnostic abstract calculus for generalized OMT that can also be used to describe and study previous OMT approaches; 
    
    
  * a framework for understanding and exploring search strategies for OMT; and
    
  * proofs of correctness for important properties of the calculus.


The rest of the paper is organized as follows. Section <ref> introduces background and notation. Section <ref> defines the Generalized OMT problem. Section <ref> presents the calculus, provides an illustrative example of its use and addresses its correctness[
Full proofs and an additional example are provided in Appendix <ref> and Appendix <ref>.
Full proofs and an additional example are provided in a tech report <cit.>.
].
Finally, Section <ref> discusses related work, and Section <ref> concludes.







§ BACKGROUND





We assume the standard many-sorted first-order logic setting for SMT, with the usual
notions of signature, term, formula, and interpretation.
We write ϕ to mean that formula ϕ holds in or is satisfied by an interpretation . 
A theory is a pair = (Σ, ), where
Σ is a signature and   is a class of Σ-interpretations.
We call the elements of  -interpretations.
We write Γ_ϕ, where Γ is a formula (or a set of formulas), 
to mean that Γ -entails ϕ, 
i.e., every -interpretation that satisfies (each formula in) Γ 
satisfies ϕ as well.

For convenience, for the rest of the paper, 
we fix a background theory  with equality and with signature Σ.
We also fix an infinite set 𝒳 of sorted variables with sorts from Σ and assume ≺_𝒳 is some total order on 𝒳.
We assume that all terms and formulas are Σ-terms and Σ-formulas with free variables from 𝒳.
Since the theory  is fixed, we will often abbreviate _ as  and consider only interpretations 
that are -interpretations assigning a value to every variable in 𝒳.  
At various places in the paper, we use sorts and operators from standard SMT-LIB
theories such as integers, bitvectors, strings,[For simplicity,
we assume strings are over characters ranging only from  to
.] or data types <cit.>.
We assume that every -interpretation interprets them in the same (standard) way.  Table <ref> lists theory symbols used in this paper and their meanings.








A Σ-formula ϕ is
satisfiable (resp., unsatisfiable) in 
if it is satisfied by some (resp., no) -interpretation.




Let s be a Σ-term. We denote by s^ the value of s in an interpretation , defined as usual by recursively determining the values of sub-terms. 
We denote by (s) the set of all variables occurring in s. 
Similarly, we write (ϕ) to denote the set of all the free variables occurring in a formula ϕ.
If (ϕ) = {v_1,…,v_n}, where for each i∈[1,n), v_i ≺_𝒳 v_i+1, then the relation defined by ϕ (in ) is
{(v_1^,…,v_n^) |ϕ for some -interpretation }.
A relation is definable in  if there is some formula 
that defines it.

Let v be a tuple of variables (v_1,…,v_n), and let t=(t_1,…,t_n) be a tuple of Σ-terms, such that t_i and v_i are of the same sort for i∈ [1,n]; then, we denote by s[vt] 
the term obtained from s by simultaneously replacing each occurrence of variable v_i 
in s with the term t_i. 





If S is a finite sequence (s_1,…,s_n),  we write (S) to denote, s_1, the first element of S in S;  we write (S) to denote the subsequence (s_2,…,s_n) of S.  We use ∅ to denote both the empty set and the empty sequence.  We write s∈ S to mean that s occurs in the sequence S, and write S ∘ S' for the sequence obtained by appending S' at the end of S.



We adopt the standard notion of strict partial order ≺ 
on a set A, that is,
a relation in A × A that is irreflexive, asymmetric, and transitive.
The relation ≺ is a strict total order if, in addition, 
a_1 ≺ a_2 or a_2 ≺ a_1 for every pair a_1, a_2 of distinct elements of A.
As usual, we will call ≺ well-founded over a subset A' of A
if A' contains no infinite descending chains.
An element m ∈ A is minimal (with respect to ≺)
if there is no a ∈ A such that a ≺ m.  If A has a unique minimal element, it is called a minimum.



§ GENERALIZED OPTIMIZATION MODULO THEORIES






We introduce a formalization of the Generalized Optimization Modulo Theories problem which unifies single- and multi-objective optimization problems and lays the groundwork for the calculus presented in Section <ref>. 
 


 §.§ Formalization
 

For the rest of the paper, we fix a theory  with some signature Σ.



A Generalized Optimization Modulo Theories problem is a tuple := ⟨ t, ≺, ϕ⟩, where:


    
  * t, a Σ-term of some sort σ, is an objective term to optimize;

    
  * ≺ is a strict partial order definable in , whose defining formula has two free variables, each of sort σ; and

    
  * ϕ is a Σ-formula.







For any problem and -interpretations  and ', we say that:
 is -consistent if ϕ;  -dominates ', denoted by <_', if  and ' are -consistent
    
    and t^≺  t^'; and  is a -solution if  is -consistent and no -interpretation -dominates .


Informally, the term t
represents the objective function, whose value we want to optimize.
The order ≺ is used to compare values of t,
with a value a being considered better than a value a' if a ≺ a'. Finally, the formula ϕ imposes constraints on the values that t can take.
It is easy to see that the value of t^ assigned by a
-solution  is always minimal.  As a special case, if
≺ is a total order, then t^ is also unique (i.e., it is a minimum).
Once we have fixed a problem , we will informally refer 
to a -consistent interpretation as a solution (of ϕ)
and to a -solution as an optimal solution.








Our notion of Generalized OMT is closely related to one by Bigarrella et al. <cit.>, which defines a notion of OMT for a generic background theory using a predicate that corresponds to a total order in that theory.
Definition <ref> generalizes this in two ways.  First, we allow partial orders, with total orders being a special case. 
One useful application of this generalization is the ability to model multi-objective problems as single-objective problems over a suitable partial order, as we explain below. 
Second, we do not restrict ≺ to correspond to a predicate symbol in the theory.  Instead, any partial order definable in the theory can be used. This general framework captures a large class of optimization problems.
 




Suppose  is the theory of real arithmetic with the usual signature.
Let := ⟨ x+y, ≺, 0 < x ∧ xy=1
⟩, where x and y are variables of sort  and
≺ is defined by the formula v_1 <_ v_2 (where v_1
≺_𝒳 v_2). A -solution is any interpretation that interprets x and y as 1.




With  now being the theory of integer arithmetic,
let = ⟨ x, ≺, x^2 < 20 ⟩, where x is of sort
, and ≺ is defined by v_1 >_ v_2 (where v_1
≺_𝒳 v_2).  A -solution must interpret x as the maximum integer satisfying x^2 < 20 (i.e., x must have value 4).

 

The examples above are both instances of what previous work refers to
  as single-objective optimization problems <cit.>, with
  the first example being a minimization and the second a maximization
  problem.  The next example illustrates a less conventional ordering.

Note that from
now on, to keep the exposition simple, we define partial orders ≺
appearing in problems only semantically, i.e., formally, but
without giving a specific defining formula.  However, it is easy to check that
all orders used in this paper are, in fact, definable in a suitable .



Let = ⟨ x, ≺, x^2 < 20 ⟩ be a variation of Example <ref>, where now a ≺ b iff |b| ≺_ |a|.  A -solution can interpret x either as 4 or -4.  Neither solution dominates the other since their absolute values are equal.


We next show how multi-objective problems are also instances of Definition <ref>.



 §.§ Multi-Objective Optimization



We use the term multi-objective optimization to refer to an optimization problem consisting of several sub-problems, each of which is also an optimization problem.  A multi-objective optimization may also require specific interrelations among its sub-problems.  In this section, we define several varieties of multi-objective optimization problems and show how each can be realized using Definition <ref>.  For each, we also state a correctness proposition which follows straightforwardly from the definitions.

In the following, given a strict ordering ≺, we will denote its reflexive closure by ≼. 
We start with a multi-objective optimization problem which requires that the sub-problems be prioritized in lexicographical order <cit.>.


A lexicographic optimization problem is a sequence of problems ℒ𝒪=(_1,…,_n), where _i := ⟨ t_i, ≺_i, ϕ_i⟩ for i ∈ [1,n]. 
For -interpretations  and ', we say that:


    ℒ𝒪-dominates ', denoted by <_ℒ𝒪',  if  
 and ' are _i-consistent for each i∈[1,n],
and for some j ∈ [1,n]:
(i)  t_i^ = t_i^' for all i∈[1,j); and
        (ii)  t_j^ ≺_j t_j^'.


    is a solution to ℒ𝒪 iff  is _i-consistent for each i and no -interpretation ℒ𝒪-dominates .



An ℒ𝒪 problem can be solved by converting it into an instance of Definition <ref>.



    Given an ℒ𝒪 problem (_1,…,_n), 
    with _i := ⟨ t_i, ≺_i, ϕ_i⟩ for i ∈ [1,n],
    the corresponding instance is defined as 

    
    _ℒ𝒪(_1,…,_n) := ⟨ t, ≺_ℒ𝒪, ϕ⟩, where:
    
        
  * t=(t_1,…,t_n);
            ϕ = ϕ_1∧⋯∧ϕ_n;
        
  * if t is of sort σ, then 
        ≺_ℒ𝒪 is the lexicographic extension of (≺_1, …,≺_n) to σ^:


        
        for (a_1,…,a_n), (b_1,…,b_n)∈σ^,  (a_1,…,a_n) ≺_ℒ𝒪 (b_1,…,b_n) iff:



        for some  j∈[1,n]: (i) a_i  =  b_i  for all
        i ∈ [1,j),  and
        (ii)  a_j  ≺_j  b_j.        



   


  

  



     


Here and in other definitions below, we use the data type theory constructor  to construct the objective term t.  This is a convenient mechanism for keeping an ordered list of the sub-objectives and keeps the overall theoretical framework simple.  In practice, if using a solver that does not support tuples or the theory of data types, other implementation mechanisms could be used.
Note that if each sub-problem uses a total order, then ≺_ℒ𝒪 will also be total.


    Let  be a _ℒ𝒪-solution.  Then  is also a solution to the corresponding ℒ𝒪 problem as defined in Definition <ref>.


[ℒ𝒪] 
Let _1:=⟨ x, ≺_1, ⟩ and _2:=⟨ y 2 z, ≺_2, ⟩, where  x, y, z are variables of sort 2, a ≺_1 b iff a 2 b, and a ≺_2 b iff a 2 b. 
Now, let = _ℒ𝒪(_1,_2) = ⟨ t, ≺_ℒ𝒪, ⟩. Then, t=(x,y2z) and
(a_1,a_2) ≺_ℒ𝒪 (b_1,b_2) iff a_1 2 b_1 or (a_1 = b_1  and  a_2 2 b_2 ).

Now, let , ', and ” be such that: x^=11, y^= 00, z^=10, and t^ :=(11,10); x^'=01, y^'=01, z^'=01, and t^':=(01,10); x^”=01, y^”=01, z^”= 10, and t^”:=(01,11).









Then, ” <_'<_, since (01,11) ≺_ℒ𝒪 (01,10) ≺_ℒ𝒪 (11,10). 



We can also accommodate Pareto optimization <cit.> in our framework.

    

A Pareto optimization problem is a sequence of problems = (_1,…,_n), where _i := ⟨ t_i, ≺_i,
ϕ_i ⟩ for i ∈ [1,n]. For any -interpretations  and ', we say that:

    
    -dominates, or Pareto dominates, ', denoted by <_', if  and ' are -consistent w.r.t. each _i, i∈[1,n],
and: 



  (i) t_i^≼_i t_i^' for all i ∈ [1,n]; and (ii)  for some j ∈ [1,n],
        t_j^≺_j t_j^'. 



 is a solution to iff  is -consistent w.r.t. each _i and no ' -dominates . 
    


 
Given a PO problem = (_1,…,_n), we define _(_1,…,_n) := ⟨ t, ≺_, ϕ⟩, where: 
    
        
  * t=(t_1,…,t_n);    ϕ = ϕ_1∧⋯∧ϕ_n; 
        
  * if t is of sort σ, then ≺_ is the pointwise extension of 
        (≺_1, …,≺_n) to σ^;
        for any (a_1,…,a_n), (b_1,…,b_n) ∈σ^, (a_1,…,a_n) ≺_ (b_1,…,b_n) iff:
        (i) a_i  ≼_i  b_i  for all  i ∈ [1,n],  and
        (ii)  a_j  ≺_j  b_j  for some j∈[1,n]. 
        


        

        

        




    
  


    Let  be a _-solution.  Then  is also a solution to the corresponding problem as defined in Definition <ref>.


Next, consider a example with two sub-problems: one minimizing the length of a string w, and the other maximizing a substring x of w lexicographically.

[]
Let  be the SMT-LIB theory of strings and let
_1:= ⟨(w), ≺_1, (w) < 4 ⟩ and 
_2:= ⟨ x, ≺_2, (w, x)⟩, where  w, x are
  variables of sort , ≺_1 ≡ ≺_, and ≺_2 ≡ ≻_.
Now, let _ =
_(_1, _2)=⟨ t, ≺_, (w)<4 ∧(x, w) ⟩.
Then, t = ((w), x) and
(a_1,a_2) ≺_ (b_1,b_2) iff a_1 ≼_ b_1,   a_2 ≽_ b_2, and (a_1  ≺_ b_1 or a_2 ≻_ b_2). Now, let , ', and ” be such that: :={w ↦aba, x ↦ab} and t^:=(3,ab); ':={w ↦z, x ↦z} and t^':=(1,z); and ”:={w ↦ϵ, x ↦ϵ} and t^:=(0,ϵ).








Then, ' <_, since (1, z) ≺_ (3, ab); but both  and ' are incomparable with ”.  Both ' and ” are optimal solutions.





We can similarly capture the MinMax and MaxMin optimization problems <cit.> as corresponding instances of Definition <ref> as described below.


A MinMax optimization problem is a sequence of problems, ℳℐ𝒩ℳ𝒜𝒳 = (_1,…,_n), where _i := ⟨ t_i, ≺, ϕ_i⟩ for i ∈ [1,n]. For any -interpretations  and ', we say that:

    
    ℳℐ𝒩ℳ𝒜𝒳-dominates ', denoted by <_ℳℐ𝒩ℳ𝒜𝒳',  if  and ' are _i-consistent for each i∈[1,n], and 
    
 t_max^≺ t_max^' where:
 
 
     
  (i) t_max^ = t_i^ for some i ∈ [1,n], t_max^' = t_j^' for some j ∈ [1,n]; and

     
  (ii) t_k^≼ t_max^ and t_k^'≼ t_max^' for all 
 k ∈ [1,n]



    
    is a solution to ℳℐ𝒩ℳ𝒜𝒳 iff  is _i-consistent for each i and no ' ℳℐ𝒩ℳ𝒜𝒳-dominates .





Given a ℳℐ𝒩ℳ𝒜𝒳 problem (_1,…,_n), we define
 _ℳℐ𝒩ℳ𝒜𝒳(_1,…,_n) := ⟨ t, ≺_ℳ𝒩ℳ𝒳, ϕ⟩, where:
    
        
  * t =  (t_1,…,t_n);    ϕ = ϕ_1 ∧…∧ϕ_n;

        
  * if t is of sort σ, then for any (a_1,…,a_n),(b_1,…,b_n)∈σ^, 

        (a_1,…,a_n) ≺_ℳ𝒩ℳ𝒳 (b_1,…,b_n) iff:



        for some i,j∈[1,n]: (i) a_k ≼a_i and b_k ≼ b_j  for all  k ∈ [1,n],  and  (ii)  a_i ≺ b_j.







    
    


    Let  be a _ℳℐ𝒩ℳ𝒜𝒳-solution.  Then  is also a solution to the corresponding ℳℐ𝒩ℳ𝒜𝒳 problem as defined in Definition <ref>.


[ℳℐ𝒩ℳ𝒜𝒳] Let _1:=⟨ a+b+c, ≺_, a < b + c⟩ and _2:= ⟨ abc, ≺_, 0 ≤ abc ⟩, where  a, b, c are variables of sort .
Now, let _3=_ℳℐ𝒩ℳ𝒜𝒳(_1,_2) = ⟨ t, ≺_ℳ𝒩ℳ𝒳, a < b + c ∧ 0 ≤ abc  ⟩, where t := (a+b+c, abc) and (a_1, a_2)≺_ℳ𝒩ℳ𝒳(b_1, b_2) iff max(a_1,a_2) ≺_max(b_1,b_2). Let , ', and ” be such that:
:={a ↦ 2, b ↦ 1, c ↦ 3} and t^:=(6, 6);
':={a ↦ 1, b ↦ 0, c ↦ 4} and t^':=(5, 0); and
”:={a ↦ 0, b ↦ 1, c ↦ 4} and t^”:=(5, 0).








Then, ' and ” both ℳℐ𝒩ℳ𝒜𝒳-dominate  , since (5,0) ≺_ℳ𝒩ℳ𝒳 (6,6).  But neither ' nor ” ℳℐ𝒩ℳ𝒜𝒳-dominates the other.

The ℳ𝒜𝒳ℳℐ𝒩 optimization problem is the dual of ℳℐ𝒩ℳ𝒜𝒳, and it can be defined in a similar way. 


A MaxMin optimization problem is a sequence of problems, ℳ𝒜𝒳ℳℐ𝒩 = (_1,…,_n), where _i := ⟨ t_i, ≺, ϕ_i⟩ for i ∈ [1,n]. For any -interpretations  and ', we say that:

    
    ℳ𝒜𝒳ℳℐ𝒩-dominates ', denoted by <_ℳ𝒜𝒳ℳℐ𝒩',  if  and ' are _i-consistent for each i∈[1,n], and 
    t_min^'≺ t_min^ where:

 
    
  (i) t_min^ = t_i^ for some i ∈ [1,n], t_min^' = t_j^' for some j ∈ [1,n]; and

    
  (ii) t_min^≼ t_k^ and t_min^'≼ t_k^' for all k ∈ [1,n]; 

    
 
 


    is a solution to ℳ𝒜𝒳ℳℐ𝒩 iff  is _i-consistent for each i and no ' ℳ𝒜𝒳ℳℐ𝒩-dominates .




 Given a ℳ𝒜𝒳ℳℐ𝒩 problem (_1,…,_n), we define 
_ℳ𝒜𝒳ℳℐ𝒩(_1,…,_n) := 
⟨ t, ≺_ℳ𝒳ℳ𝒩, ϕ⟩, where:
    
        
  * t=(t_1,…,t_n);   ϕ = ϕ_1,…,ϕ_n;
        
  * if t is of sort σ, then for any (a_1,…,a_n),(b_1,…,b_n)∈σ^, 

        (a_1,…,a_n) ≺_ℳ𝒳ℳ𝒩 (b_1,…,b_n) iff:


        
        for some i,j∈[1,n]: (i)   a_i ≼a_k  and  b_j ≼b_k   for all  k ∈ [1,n],  and (ii)   b_j ≺ a_i.  
    
 


    Let  be a _ℳ𝒜𝒳ℳℐ𝒩-solution.  Then  is also a solution to the corresponding ℳ𝒜𝒳ℳℐ𝒩 problem as defined in Definition <ref>.


[ℳ𝒜𝒳ℳℐ𝒩] Let _1:=⟨ a+b+c, ≺_, a < b + c⟩ and _2:= ⟨ abc, ≺_, 0 ≤ abc ⟩, where  a, b, c are variables of sort .
Now, let _3=_ℳ𝒜𝒳ℳℐ𝒩(_1,_2) = ⟨ t, ≺_ℳ𝒳ℳ𝒩, a < b + c ∧ 0 ≤ abc  ⟩, where t := (a+b+c, abc) and (a_1, a_2)≺_ℳ𝒳ℳ𝒩(b_1, b_2) iff min(b_1,b_2) ≺_min(a_1,a_2). Let , ', and ” be such that:
:={a ↦ 2, b ↦ 1, c ↦ 3} and t^:=(6, 6);
':={a ↦ 1, b ↦ 0, c ↦ 4} and t^':=(5, 0); and
”:={a ↦ 0, b ↦ 1, c ↦ 4} and t^”:=(5, 0).
Then,  ℳ𝒜𝒳ℳℐ𝒩-dominates both ' and ”, since (6,6) ≺_ℳ𝒳ℳ𝒩 (5,0).  But neither ' nor ” ℳ𝒜𝒳ℳℐ𝒩-dominates the other.


Though we omit them for space reasons, we can similarly capture the MinMax and MaxMin optimization problems <cit.> as corresponding _ℳℐ𝒩ℳ𝒜𝒳 and _ℳ𝒜𝒳ℳℐ𝒩 instances of Definition <ref>.[


Details of these formulations can be found in the longer version of this paper <cit.>.
]





Note that except for degenerate cases, the orders ≺_ℳ𝒩ℳ𝒳, ≺_ℳ𝒳ℳ𝒩, as well as the order ≺_ above, are always partial orders.  
Note that except for degenerate cases, the orders used for MinMax and MaxMin, as well as the order ≺_ above, are always  partial orders.  
Being able to
model these multi-objective optimization problems in a clean and simple way is
a main motivation for using a partial instead of a total order in Definition <ref>.

Another problem in the literature is the multiple-independent (or boxed) optimization problem <cit.>.  It simultaneously solves several independent problems.  We show how to realize this as a single instance.

 
    A boxed optimization problem is a sequence of problems, = (_1,…,_n), where _i := ⟨ t_i, ≺_i,
ϕ_i⟩ for i ∈ [1,n]. We say that:



    
   A sequence of interpretations (_1,…,_n) -dominates ('_1,…,'_n), denoted by (_1,…,_n) <_ ('_1,…,'_n), if _i and '_i are _i-consistent or each i∈[1,n],
and:











(i) t_i^_i≼_i t_i^'_i for all i ∈ [1,n];  and  
(ii) for some j ∈ [1,n],
        t_j^_j≺_j t_j^'_j.


(_1,…,_n) is a solution to iff _i is _i-consistent for each i∈[1,n] and no ('_1,…,'_n) -dominates (_1,…,_n).
        



Note that in previous work, there is an additional assumption that ϕ_i =
ϕ_j for all i,j∈[1,n].  Below, we show how to solve the more general case without this assumption.
We first observe that the above definition closely resembles
Definition <ref> for Pareto optimization (PO) problems.
Leveraging this similarity, we show
how to transform an instance of a BO problem into a PO problem.


    (_) 
Let = (_1,…,_n), where
_i := ⟨ t_i, ≺_i, ϕ_i⟩ for i ∈ [1,n].
Let V_i be the set of all free variables in the
i^th sub-problem that also appear in at least one other sub-problem:

    V_i = ((t_i)∪(ϕ_i))  ∩⋃_j∈[1,n],j ≠ i(t_j)∪(ϕ_j).

Let
v_i=(v_i,1,…,v_i,m) be some ordering of the variables in V_i
(say, by ≺_𝒳), and for each j∈[1,m], let v'_i,j be a
fresh variable of the same sort as v_i,j, and let
v'_i=(v'_i,1,…,v'_i,m).  Then, let t'_i =
t_i[v_iv'_i], ϕ'_i =
ϕ_i[v_iv'_i], and '_i =
⟨ t'_i, ≺_i, ϕ'_i⟩.  Then we define
_:=_('_1,
…,'_n).





    Let  be a solution to _ as defined in Definition <ref>.  Then (_1,…,_n) is a solution to the corresponding problem as defined in Definition <ref>, where for each i∈[1,n], _i is the same as  except that each variable v_i,j∈ V_i is interpreted as (v'_i,j)^.


In practice, solvers for BO
problems can be implemented without variable renaming (see, e.g.,
<cit.>).  Variable renaming, while a useful
theoretical construct, also adds generality to our definition of .  An interesting direction for future experimental work would
be to compare the two approaches in practice.




Compositional Optimization   


problems can also be combined through functional composition of multiple objective terms, possibly of different sorts, yielding compositional optimization problems <cit.>.
  Our framework handles them naturally by simply constructing an objective term capturing the desired compositional
relationship.

For example, compositional objectives can address the (partial) MaxSMT problem <cit.>, where some formulas are hard constraints and others are soft constraints.  The goal is to satisfy all hard constraints and as many soft constraints as possible.  The next example is inspired by Cimatti et al. <cit.> and Teso et al. <cit.>.



[MaxSMT]
Let x  ≥ 0 and y ≥ 0 be hard constraints and
4x+y-4  ≥  0 and 2x+3y-6  ≥ 0 soft constraints. We can formalize this as _=⟨ t, ≺, ϕ⟩, where: t=(4x+y-4 ≥ 0,0,1) + (2x+3y-6 ≥  0,0,1),   ≺ ≡ ≺_, and ϕ = x  ≥  0 ∧ y ≥ 0. An optimal solution must satisfy both hard constraints and, by minimizing the objective term t, as many soft constraints as possible.



MaxSMT has various variants including generalized, partial, weighted, and partial weighted MaxSMT <cit.>, all of which our framework can handle similarly.




Next, we show a different compositional example that combines two different orders, one on strings and the other on integers.

[Composition of  and ]
Let  be again the theory of strings[The SMT-LIB theory of strings includes the theory of integers to support constraints over string length.] 
Let _ = ⟨(x,(x)), ≺, (x, a) ∧(x)>1⟩, where x is of sort  and 
(a_1,b_1) ≺ (a_2,b_2) iff b_1 ≺_ b_2 or (b_1 = b_2 and a_1 ≻_ a_2). ≺ prioritizes minimizing the length, but then maximizes the string with respect to lexicographic order. An optimal solution must interpret x as the string za of length 2 since x must be of length at least 2 and contain a, making za the largest string of minimum length.




Based on the definitions given in this section, we see that our
formalism can capture any combination of 
 (including compositional), _ℒ𝒪, _,
_ℳℐ𝒩ℳ𝒜𝒳, _ℳ𝒜𝒳ℳℐ𝒩, and
_ problems.  And note that the last four all make use of the partial order feature of Definition <ref>.








§ THE CALCULUS




We introduce a calculus for solving the problem, presented 
as a set of derivation rules. 
We fix a problem = ⟨ t, ≺, ϕ⟩
where ϕ is satisfiable (optimizing does not make sense otherwise).
We start with a few definitions.

A state is a tuple Ψ = ⟨, Δ, τ⟩, where  is an interpretation,  Δ is a formula, and τ is a sequence of formulas.




The set of all states forms the state space for the problem. 
Intuitively, the proof procedure of the calculus is a search procedure over this state space
which maintains at all times a current state  
⟨, Δ, τ⟩ storing a candidate solution and
additional search information.
In the current state,

 is the best solution found so far in the search;  
Δ is a formula describing the remaining, yet unexplored, part of the state space, 
where a better solution might exist; and
τ contains formulas that divide up the search space described by Δ
into branches represented by the individual formulas in τ,
maintaining the invariant that 
the disjunction of all the formulas τ_1, …, τ_p 
in τ is equivalent to Δ modulo ϕ, 
that is, ϕ (⋁_i=1^p τ_i Δ). 






Note that states contain -interpretations,
which are possibly infinite mathematical structures.  This is useful to keep the calculus simple. 
In practice,
it is enough just to keep track of the interpretations of the (finitely-many)
symbols without fixed meanings (variables and uninterpreted functions and sorts) appearing in the state, much as SMT solvers do in order to produce models. 









 Solve is a function that takes a formula and returns a satisfying interpretation if the formula is satisfiable and a distinguished value  otherwise.



_ is a function that takes a -consistent interpretation  and returns a formula _() with the property that for every -consistent interpretation ',


    ' _()  iff  ' <_.






The function above is specific to the given optimization problem or, put differently, is parametrized by t, ≺, and ϕ.
When is clear, however, we simply write , 
for conciseness.



The calculus relies on the existence and computability 
of Solve and .  Solve can be realized by any standard SMT solver.   relies on a defining formula for ≺ as discussed below. We note that intuitively, () is simply a (possibly unsatisfiable) formula characterizing the solutions of ϕ that are better than .  Assuming α_≺ is the formula defining ≺, with free variables v_1 ≺_𝒳 v_2, if the value t^ can be represented by some constant c (e.g., if t^ is a rational number), then () = α_≺[(v_1,v_2)(t,c)] satisfies Definition <ref>.  On the other hand, it could be that t^ is not representable as a constant (e.g., it could be an algebraic real number); then, a more sophisticated formula (involving, say, a polynomial and an interval specifying a particular root) may be required.




The initial  state of the problem 
= ⟨ t, ≺, ϕ⟩ is 
⟨_0, Δ_0, τ_0⟩, where _0 = Solve(ϕ), Δ_0 = (_0), τ_0 = (Δ_0).




Note that _0 ≠ since we assume that ϕ is satisfiable.
The search for an optimal solution to the problem in our calculus starts
with an arbitrary solution of the constraint ϕ and continues until
it finds an optimal one.






 §.§ Derivation Rules
 


Figure <ref> presents the derivation rules of the calculus.  The rules are given in guarded assignment form, where the rule premises describe the conditions on the current state that must hold for the rule to apply, and the conclusion describes the resulting modifications to the state.
State components not mentioned in the conclusion of a rule are unchanged.

A derivation rule applies to a state if 
(i) the conditions in the premise are satisfied by the state and
(ii) the resulting state is different.
A state is saturated if no rules apply to it.
A -derivation is a sequence of states, possibly infinite, where the first state is the initial state of the problem , and each state in the sequence is obtained by applying one of the rules to the previous state.  The solution sequence of a derivation is the sequence made up of the solutions (i.e., the interpretations) in each state of the derivation. 



The calculus starts with a solution for ϕ
and improves on it until an optimal solution is found.
During a derivation, the best solution found so far is maintained
in the  component of the current state.
A search for a better solution can be organized into branches through the use of the F-Split rule.
Progress toward a better solution is enforced by the formula Δ 
which, by construction, is falsified by all the solutions found so far.

We elaborate on the individual rules next.


F-Split  
F-Split divides the branch of the search space represented 
by the top formula ψ = Top(τ) in τ 
into k sub-branches (ψ_1, …,ψ_k), ensuring their disjunction is equivalent to ψ modulo the constraint ϕ: 
ϕψ⋁_j=1^k ψ_j.
The rest of the state remains unchanged. F-Split 
is applicable whenever τ is non-empty.
The rule does not specify how the formulas ψ_1, …, ψ_k are chosen. 
However, a pragmatic implementation should aim to generate them so that 
they are irredundant
in the sense that no formula is entailed 
modulo ϕ by the (disjunction of the) other formulas.
This way, 
each branch potentially contains a solution that the others do not.
Note, however, that this is not a requirement.

F-Sat  The F-Sat rule applies when there is a solution in the branch represented by the top formula ψ in τ. 
The rule selects a solution ' = Solve(ϕ∧ψ) from that branch. One can prove that, by the way the formulas in τ are generated in the calculus, ' necessarily improves on the current solution ,
moving the search closer to an optimal solution.[
See Lemma <ref> in Appendix <ref>.
See Lemma 6 in Appendix B of the tech report <cit.>.
] 
Thus, F-Sat switches to the new solution (with :=') and 
directs the search 
to seek an even better solution 
by updating Δ to Δ' = Δ ∧ Better(').

Note that F-Sat
resets τ to the singleton sequence (Δ'), 
discarding any formulas in τ.
This is justified, as any discarded better solutions must also be in the space defined by Δ'.



F-Close  

The F-Close rule eliminates the first element ψ of a non-empty τ
if the corresponding branch contains
no solutions (i.e., Solve(ϕ∧ψ) =).

The rule further updates the state by adding the negation of ψ to Δ 
as a way to eliminate from further consideration the interpretations satisfying ψ.


Note that rules F-Sat and F-Close both update Δ to reflect the remaining search space, whereas F-Split refines the division of the current search space.




 §.§ Search strategies



The calculus provides the flexibility 
to support different search strategies.
Here, we briefly discuss a few of them.


Linear search:
A linear search strategy is obtained by never using the F-Split rule. Instead, the F-Sat rule is applied to completion
(that is, repeatedly until it no longer applies).

This may lead the strategy to diverge if an optimal solution does not exist
or, more generally, if there is a Zeno-style <cit.> infinite chain 
of increasingly better solutions, all dominated by an optimal one, 
and Solve returns one element along that chain at each call.
As we show later (see Theorem <ref>), in the absence of Zeno chains, τ eventually becomes empty, terminating the search.
At that point,  is guaranteed to be an optimal solution.


Binary search: 
A binary search strategy is achieved by using 
the F-Split rule to split the search space represented 
by ψ = Top(τ) into two subspaces, 
represented by two formulas ψ_1 and ψ_2, 
with ϕψ (ψ_1 ∨ψ_2).
In a strict binary search strategy, ψ_1 and ψ_2 should be chosen so that the two subspaces are disjoint and, to the extent possible, of equal size.







A typical binary strategy alternates applications of F-Split
with applications of either F-Sat or F-Close
until τ becomes empty,
at which point  is guaranteed to be an optimal solution.
A smart strategy would aim to find an optimal solution as soon as possible by arranging for solutions in ψ_1 (which will be checked first) to be better than solutions in ψ_2, if this is easy to determine.
Note that an unfortunate choice of ψ_1 by F-Split,
containing no solutions at all, is quickly remedied by an application
of F-Close which removes ψ_1, allowing ψ_2 to be considered next.


Multi-directional exploration: For multi-objective optimization problems, a search strategy can be defined to simultaneously direct the search space towards any or all objectives. Formally, if n is the number of objectives, then the F-Split rule can be instantiated in such a way that ψ_j = ⋀_i=1^n ψ_ji, where  ψ_ji is a formula describing a part of the search space for the i^th objective term in the j^th branch.



Search order: We formalize τ as a sequence to enforce exploring the branches in τ in a specific order, assuming such an order can be determined at the time of applying F-Split. Often, this is the case. For example, in binary search, it is typically best to explore the section of the search space with better objective values first. If a solution is found in this section, a larger portion of the search space is pruned. Conversely, if the branches are explored in another order, even finding a solution necessitates continued exploration of the space corresponding to the remaining branches.

Alternatively, τ can be implemented as a set, by redefining the Top and Pop functions accordingly to select and remove a desired element in τ. With τ defined as a set, additional search strategies are possibile, including parallel exploration of the search space and the ability to arbitrarily switch between branches.








Hybrid search: 
For some objectives and orders, there exist off-the-shelf external optimization procedures (e.g., Simplex for linear real arithmetic). One way to integrate such a procedure into our calculus is 
to replace a call to the Solve function in F-Sat
with a call to an external optimization procedure 
Optimize that is sort- and order-compatible with the problem.
We pass to Optimize as parameters the constraint
ϕ∧Top(τ) and the objective t



and obtain an optimal solution in the current branch 
Top(τ).[This assumes there exists an optimal solution in the current branch.  If not (i.e., if the problem is unbounded), a suitable error can be raised and the search terminated.]
The call can be viewed as an accelerator for a linear search 
on the current branch.
This approach incorporates theory-specific optimization solvers in much the same way as is done in the OMT literature. However, our calculus extends previous approaches with the ability to blend theory-specific optimization with theory-agnostic optimization 
by interleaving applications of F-Sat using Solve 
with applications using Optimize.
For example, we may want to alternate
between expensive calls to an external optimization solver and calls to a standard solver that are guided by a custom branching heuristic.






Other strategies: 
The calculus enables us to mix and match the above strategies arbitrarily, as well as to model other notable search techniques like cutting planes <cit.> by integrating a cut formula into . And, of course, one advantage of an abstract calculus is that its generality provides a framework for the exploration of new strategies. Such an exploration is a promising direction for future work.





 §.§ New Applications



A key feature of our framework is that it is theory-agnostic, that is, it can be used with any SMT theory or combination of theories.  This is in contrast to most of the literature in which a specific theory is targeted.  It also fully supports arbitrary composition of problems using the multi-objective approaches described in Section <ref>.  Thus, our framework enables to be extended to new application areas requiring either combinations of theories or multi-objective formulations that are unsupported by previous approaches.
We illustrate this (and the calculus itself) using
a Pareto optimization problem over the theories of strings and integers (a combination of theories and objectives unsupported by any existing OMT approach or solver).

[_𝒫𝒪]
Let _1:= ⟨(w), ≺_1, (s) < (w) ⟩ and 
_2:= ⟨ x, ≺_2, x = s · w · s⟩, where w, x, s are of sort , (w) and (s) are of sort , ≺_1  ≡ ≺_, and ≺_2  ≡ ≻_;. 
Then, let _𝒫𝒪(_1,_2):=⟨ t,
 ≺_𝒫𝒪, ϕ⟩, where t is ((w), x), ϕ is x = s · w · s  ∧ (s) < (w), and (a_1,a_2)  ≺_𝒫𝒪  (b_1,b_2) iff a_1  ≼_1  b_1,   a_2  ≼_2  b_2, and either a_1 
  ≺_1  b_1 or a_2  ≺_2  b_2 or both.

Suppose initially:


    [                                             _0                                              =     {x ↦aabaa, s ↦a, w ↦aba, },  τ_0 =  (Δ_0),;                                            Δ_0                                              = ((w) ≤ 3 ∧ x >_aabaa) ∨ ((w) < 3 ∧ x ≥_aabaa). ]


The initial objective term value is (3,aabaa).



  * We can first apply F-Split to split the top-level disjunction in τ.  And suppose we want to work on the second disjunct first.  This results in:



    [                                        τ_1                                          = ( (w) < 3 ∧ x ≥_aabaa,(w) ≤ 3 ∧ x >_aabaa) ]


while the other elements of the state are unchanged.


  * Now, suppose we want to do binary search on the length objective.  This can be done by again applying the F-Split rule 

with the disjunction 
((w) < 2 ∧ x ≥_aabaa) 
   
  (2 ≤(w) < 3 ∧ x ≥_aabaa)

to get:



    [                                          τ_2                                            = ( (w) < 2 ∧ x ≥_aabaa,2≤(w) < 3 ∧ x ≥_aabaa,;                                                                     (w) ≤ 3 ∧ x >_aabaa). ]






  * Both F-Split and F-Sat are applicable, but we follow the strategy of applying F-Sat after a split.  Suppose we get the new solution ' = {x ↦b, s ↦ϵ, w ↦b}.  Then we have:



    [                                      _3                                       =      {x ↦b, s ↦ϵ, w ↦b},  τ_3  = (Δ_3),;                                     Δ_3                                       = ((w) ≤ 1 ∧ x >_b)  ∨ ((w) < 1 ∧ x ≥_b). ]




  * Both F-Split and F-Sat are again applicable. Suppose that we switch now to linear search and thus again apply F-Sat, and suppose the new solution is ' = {x ↦z, s ↦ϵ, w ↦z}.  This brings us to the state:


    [                                      _4                                       =      {x ↦z, s ↦ϵ, w ↦z},  τ_4  = (Δ_4),;                                     Δ_4                                       = ((w) ≤ 1 ∧ x >_z)  ∨ ((w) < 1 ∧ x ≥_z). ]



    
  * Now, Solve(ϕ∧ (((w) ≤ 1 ∧ x >_z) ∨ ((w) < 1 ∧ x ≥_z))) =. Indeed, (w) ≠ 0, since 0 ≤ (s) < (w);
    
    if (w) = 1, then (s) = 0 and (x) = 1, thus, x ≯_z. Now F-Close can derive the state:
    
    ⟨_5, Δ_5, τ_5⟩ = ⟨_4, Δ_4 ∧Δ_4, ∅⟩

    


  * We have reached a saturated state, and _5 is
  a Pareto optimal solution. 
  



Optimization of objectives involving strings and integers (or strings and bitvectors) could be especially useful in security applications such as those mentioned in <cit.>.  Optimization could be used in such applications to ensure that a counter-example is as simple as possible, for example.

Examples of multi-objective problems unsupported by existing solvers include multiple Pareto problems with a single min/max query, Pareto-lexicographic multi-objective optimization, and single Pareto queries involving MinMax and MaxMin optimization (see, for example,  <cit.>). Our framework offers immediate solutions to these problems.

As has repeatedly been the case in SMT research, when new capabilities are introduced, new applications emerge. We expect that will be the case also for the new capabilities introduced in this paper. One possible application is the optimization of emerging technology circuit designs <cit.>.




 §.§ Correctness



In this section, we establish correctness properties for -derivations. 
Initially, we demonstrate that upon reaching a saturated state, 
the interpretation  in that state is optimal.

[Full proofs for the theorems in this section are available in Appendix <ref>. 
Full proofs for the theorems in this section are available in the appendix of the tech report <cit.>.
]


 (Solution Soundness) 

Let ⟨, Δ, τ⟩ be a saturated state 
in a derivation for a problem .
Then,  is an optimal solution to .


(Sketch)
We show that in a saturated state τ = ∅, and when τ = ∅, ϕΔ. Then, we establish that  is -consistent, and that for any -consistent -interpretation 𝒥,
𝒥Δ  iff  𝒥 <_. This implies there is no 𝒥 s.t. 𝒥ϕ and 𝒥 <_, confirming  as an optimal solution to .



In general, the calculus does not always have complete derivation strategies, for a variety of reasons.  It could be that the problem is unbounded, i.e., no optimal solutions exist along some branch.  Another possibility is that the order is not well-founded, and thus, an infinite sequence of improving solutions can be generated without ever reaching an optimal solution.

For the former, various checks for unboundedness can be used.  These are beyond the scope of this work, but some approaches are discussed in <cit.>.  The latter can be overcome using a hybrid strategy when an optimization procedure exists (see Theorem <ref>).

It is also worth observing that any derivation strategy 
is in effect an anytime procedure:
forcibly stopping a derivation at any point  

yields (in the final state) the best solution found so far.  When an optimal solution exists and is unique, stopping early provides the best approximation up to that point of the optimal solution.

There are also fairly general conditions under which 
solution complete derivation strategies do exist.
We present them next.



A derivation strategy is progressive if it (i) never halts in a non-saturated state and (ii) only uses F-Split a finite number of times in any derivation.


Let us again fix a problem = ⟨ t, ≺, ϕ⟩.
Consider the set 
A_t = { t^ |  is -consistent},
collecting all values of t in interpretations satisfying ϕ.


 (Termination)
If ≺ is well-founded over A_t,
any progressive strategy reaches a saturated state.


(Sketch)
We show that any derivation using a progressive strategy terminates when ≺ is well-founded. Subsequently, based on the definition of progressive, the final state must be saturated. 





 (Solution Completeness)
If ≺ is well-founded over A_t and has one or more optimal solutions,
every derivation generated by a progressive derivation strategy ends
with a saturated state containing one of them.



    The proof is a direct consequence of Theorem <ref> and Theorem <ref>.


Solution completeness can also be achieved using an appropriate hybrid strategy.



 
If has one or more optimal solutions and is not unbounded along any branch, then every derivation generated by a progressive hybrid strategy, where Solve is replaced by Optimize in F-Sat, ends with a saturated state containing one of them.


(Sketch)
If D is such a derivation, we note that F-Split can only be applied a finite number of times in D and consider the suffix of D after the last application of F-Split.  
In that suffix, F-Close can only be applied a finite number of times in a row, after which F-Sat must be applied.  We then show that due to the properties of Optimize, this must be followed by either an application of F-Close or a single application of F-Sat followed by F-Close. Both cases result in saturated states.  The theorem then follows from Theorem <ref>. 










§ RELATED WORK


Various approaches for solving the OMT problem have been proposed. We summarize the key ideas below and refer the reader to Trentin <cit.> for a more thorough survey.



The offline schema employs an SMT solver as a black box for optimization search through incremental calls <cit.>, following linear- or binary-search strategies. Initial bounds on the objective function are given and  iteratively tightened after each call to the SMT solver.
In contrast, the inline schema conducts the optimization search within the SMT solver itself <cit.>, integrating the optimization criteria into its internal algorithm. While the inline schema can be more efficient than the offline counterpart, it necessitates invasive changes to the solver and may not be possible for every theory.



Symbolic Optimization optimizes multiple independent linear arithmetic objectives simultaneously <cit.>, seeking optimal solutions for each corresponding objective. This approach improves performance by sharing SMT search effort. It exists in both offline and inline versions, with the latter demonstrating superior performance.




Other arithmetic schemas 

combine simplex, branch-and-bound, and cutting-plane techniques within SMT solvers <cit.>. A polynomial constraint extension has also been introduced <cit.>.

Theory-specific techniques address objectives involving pseudo-Booleans <cit.>, bitvectors <cit.>, bitvectors combined with floating-point arithmetic <cit.>, and nonlinear arithmetic <cit.>.

Other related work includes techniques for lexicographic optimization <cit.>, Pareto optimization <cit.>, and MaxSMT <cit.>.


Our calculus is designed to capture all of these variations.  It directly corresponds to the offline schema, can handle both single- and multi-objective problems, and can 

integrate solvers with inline capabilities (including theory-specific ones) using the hybrid solving strategy. Efficient MaxSMT approaches <cit.> can also be mimicked in our calculus. These approaches systematically explore the search space by iteratively processing segments derived from unsat cores. Our calculus can instantiate these branches using the F-Split rule, by first capturing unsat cores from calls to F-Close, and then using these cores to direct the search in the F-Split rule.  



§ CONCLUSION AND FUTURE WORK



This paper introduces the Generalized OMT problem, a proper extension of the OMT problem.
It also provides a general setting for formalizing various approaches
for solving the problem in terms of a novel calculus for and proves its key correctness properties.
As with previous work on abstract transition systems for SMT <cit.>,
this work establishes a framework for both theoretical exploration and 
practical implementations. 
The framework is general in several aspects: 
(i) it unifies single- and multi-objective optimization problems in a single definition;
(ii) it is theory-agnostic, making it applicable to any theory or combination of theories; and
(iii) it provides a formal basis for understanding and exploring search strategies for .



In future work, we plan to explore an extension of the calculus to the All-problem which requires the computation of all optimal solutions.
We also plan to develop a concrete implementation of the calculus
in a state-of-the-art SMT solver and evaluate it experimentally against 
current OMT solvers.











splncs04





