Optimization Modulo Theories (OMT) has emerged as a prominent extension of the Satisfiability Modulo Theories (SMT) paradigm, bringing optimization objectives into first-order logic constraint solving. Unlike SMT, which focuses solely on satisfiability with respect to a given theory, OMT additionally seeks to optimize a specified objective function. Several state-of-the-art SMT solvers have integrated OMT capabilities. However, no oficial SMT-LIB extension has yet been adopted for OMT. As a result, OMT benchmarks lack standardization, which hinders broader adoption and progress in the field. In this paper, we propose an extension to SMT-LIB that supports all of the diferent flavors of OMT found in the literature. Our goal is to foster the development of OMT solvers and applications, to enable more robust, reusable, and comparable OMT solutions, and to promote the creation of standardized OMT benchmarks in SMT-LIB format for systematic and meaningful evaluation.
Optimization Modulo Theories (OMT) builds on the highly successful Satisfiability Modulo Theories
(SMT) [
This added expressiveness has established OMT as a powerful tool fueling progress across a wide
range of applications. These include formal verification and model checking [
To address the wide range of optimization goals and underlying theories encountered in practice,
the OMT community has developed specialized procedures for various theories, such as arithmetic
and bitvectors, diferent types of optimization—including single- and multi-objective optimization, and
specific search strategies including linear, binary, and hybrid approaches. The result is a fragmented
landscape of theory-specific solutions, each tailored to particular combinations of goals and theories.
Our goal in this work is to start a discussion with the aim of eventually achieving consensus in the
community around an SMT-LIB standard extension that provides a uniform interface for representing a
large class of OMT problems. We draw inspiration from extensive previous work on OMT and OMT
extensions to SMT-LIB (e.g., [
The rest of the paper is organized as follows. After an overview of related work, below, we introduce the necessary formal preliminaries in Section 2 followed by our proposed SMT-LIB extension in Section 3. We provide an extensive set of examples in Section 4 and conclude in Section 5. Related Work Domain-specific OMT solving techniques have been developed based on the SMT-LIB theories and objective types of optimization problems involved.
The OMT problem was first introduced in [
Theory-specific OMT techniques address objectives involving linear real arithmetic [
Objective-specific techniques were developed for lexicographic optimization [
A recent orthogonal approach [
On the SMT-LIB syntax side, several SMT solvers have extended the SMT-LIB language to support
OMT, although no oficial standard has yet been adopted. Notably, OptiMathSAT [
Eforts have been made to integrate modeling languages with OMT to bridge the gap between
highlevel problem formulations and advanced solver capabilities. Notably, [
These eforts seek to provide interfaces for formulating and solving optimization problems with OMT solvers. However, the lack of a general SMT-LIB standard for OMT continues to limit the broader adoption and seamless integration of OMT across tools and solvers in the community. This lack of standardization hampers collaboration, makes it dificult to share benchmarks and tools, and is an obstacle to building a comprehensive OMT benchmark library.
We work within the standard many-sorted first-order logic setting for SMT, with the usual notions of signatures, terms, and interpretations. A formula is a term of sort Bool. We write ℐ |= to mean that formula holds in or is satisfied by an interpretation ℐ. A theory is a pair = (Σ , I), where Σ is a signature and I is a class of Σ -interpretations. We call the elements of I -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. A Σ -formula is satisfiable (resp., unsatisfiable ) in if it is satisfied by some (resp., no) -interpretation. For convenience, for the rest of the paper, we assume an arbitrary but fixed 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 all terms and formulas are Σ -terms and Σ -formulas with free variables from . Since is ifxed, we will often abbreviate | as |= and consider only interpretations that are -interpretations = assigning a value to every variable in .
Let be a Σ -term. We denote by ℐ the value of in an interpretation ℐ, defined as usual by recursively determining the values of sub-terms. We denote by FV () the set of all variables occurring in . Similarly, we write FV () to denote the set of all the free variables occurring in a formula . If FV () = {1, . . . , }, where for each ∈ [1, ), ≺ +1, then the relation defined by (in ) is {(1ℐ , . . . , ℐ ) | ℐ |= for some -interpretation ℐ}. A relation is definable in if there is some formula that defines it.
We adopt the standard notion of strict partial order ≺ on a set , that is, a relation in × that is irreflexive, asymmetric, and transitive. The relation ≺ is a strict total order if, in addition, 1 ≺ 2 or 2 ≺ 1 for every pair 1, 2 of distinct elements of . As usual, we call ≺ well-founded over a subset ′ of if ′ contains no infinite descending chains. An element ∈ is minimal (with respect to ≺ ) if there is no ∈ such that ≺ . If has a unique minimal element, it is called a minimum.
We rely on the Generalized Optimization Modulo Theories framework, which conveniently unifies many
OMT variants under a single umbrella. The definition and explanation below are taken from [
For any GOMT problem and -interpretations ℐ and ℐ′, we say that: • ℐ is -consistent if ℐ |= ; • ℐ -dominates ℐ′, denoted by ℐ < ℐ′, if ℐ and ℐ′ are -consistent and ℐ ≺ ℐ′ ; and • ℐ is a -solution if ℐ is -consistent and no -interpretation -dominates ℐ. Informally, the term represents the objective function, whose value we want to optimize. The order ≺ is used to compare values of , with a value being considered better than a value ′ if ≺ ′. Finally, the formula imposes constraints on the values that can take. It is easy to see that the value of ℐ assigned by a -solution ℐ is always minimal. As a special case, if ≺ is a total order, then ℐ is also unique (i.e., it is a minimum). Once we have fixed a GOMT problem , we will informally refer to a -consistent interpretation as a solution (of ) and to a -solution as an optimal solution.
This section introduces an extension to SMT-LIB v2.7 [
We also provide special syntax for specific OMT subproblems, for convenience. For example, though it can be encoded using GOMT, we include specific commands for the MaxSMT problem. Namely, following previous work, we provide commands for asserting soft constraints with assigned weights, the goal being to satisfy all hard (i.e., non-soft) constraints while maximizing the total weight of the satisfied soft ones.
Figure 1 shows the proposed extensions to the grammar of SMT-LIBv2.7. It should be understood in
the context of the grammar in the SMT-LIB v2.7 reference document [
We first note that in our proposal, OMT capabilities are not enabled by default. To enable them, the :enable-omt option must be set to true. In other words, the SMT-LIB script must include the line: (set-option :enable-omt true). We now explain the remainder of Figure 1. We focus on the new commands, explaining the other pieces as they become relevant for understanding the commands.
Command names:
⟨objective-kind⟩ ⟨m-objective-kind⟩ ⟨strategy⟩ Attributes ⟨strategy_attribute⟩ ⟨order _attribute⟩ ⟨bound_attribute⟩ ⟨assumption_attribute⟩ ⟨objective_attribute⟩ ⟨assert_attribute⟩
⟨info_flag⟩
⟨option⟩ Commands ⟨command⟩ ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= | | | | | | | | define-objective define-multi-objective define-maxsmt-objective assert-soft optimize-sat optimize-sat-next OBJECTIVE_MIN | OBJECTIVE_MAX OBJECTIVE_LEX | OBJECTIVE_PARETO | OBJECTIVE_BOX | OBJECTIVE_MINMAX | OBJECTIVE_MAXMIN STRATEGY_LINEAR | STRATEGY_BINARY :strategy ⟨strategy⟩ | ⟨attribute⟩ :order ⟨symbol⟩ :lower ⟨term⟩ | :upper ⟨term⟩ :assumption ⟨term⟩ ⟨strategy_attribute⟩ | ⟨order _attribute⟩ | ⟨bound_attribute⟩ | ⟨assumption_attribute⟩ :objective ⟨symbol⟩ | :weight ⟨term⟩ ::= :limit-optimal | :unbounded :enable-omt ⟨b_value⟩ ( define-objective ⟨symbol⟩ ⟨objective-kind⟩ ⟨term⟩ ⟨objective_attribute⟩* ) ( define-multi-objective ⟨symbol⟩ ⟨m-objective-kind⟩ ⟨symbol⟩+ ⟨attribute⟩* ) ( define-maxsmt-objective ⟨symbol⟩ ⟨strategy_attribute⟩* ) ( assert-soft ⟨term⟩ ⟨assert_attribute⟩+ ) ( optimize-sat ⟨symbol⟩ ⟨assumption_attribute⟩* ⟨attribute⟩* ) ( optimize-sat-next ) ( get-value ( ⟨symbol⟩+ ) ) ( get-model ) ( get-info ⟨symbol⟩? ⟨info_flag⟩ ) optimal | limit-optimal | non-optimal | unbounded | unsat | unknown ⟨optimize_sat_response⟩ ( ⟨info_response⟩+ ) :limit-optimal ⟨term⟩ | :unbounded ⟨term⟩
⟨optimize_sat_response⟩ ::= ⟨optimize_sat_next_response⟩ ::= ⟨get_info_response⟩ ::= ⟨info_response⟩ ::=
We start by describing two commands, define-objective and define-multi-objective, which enable the definition of single- and multi-objective optimization problems, respectively. Single Objective The define-objective command defines a single objective by specifying a name for the objective, the kind of the objective, either OBJECTIVE_MIN or OBJECTIVE_MAX, the objective term to be optimized, and one or more optional instances of objective_attribute. The objective_attribute list can include at most one :strategy attribute, any number of arbitrary attributes, at most one of each of the :order, :lower, and :upper attributes, and zero or more :assumption attributes.
Lower and upper bounds for the objective can be specified using the :lower and :upper attributes. The provided term must have the same sort as the objective term, and it must denote a value for that sort. Bounds are inclusive and are used to inform certain strategies (see below). The :assumption attribute can be followed by any arbitrary formula. Bounds and assumptions are required to be satisfied by any solution found for the objective. As with check-sat-assuming, assumptions are local to queries involving their accompanying objective (i.e., they are pushed into the context when optimizing the corresponding objective and popped once that optimization completes). This mechanism is particularly useful when working with multiple objectives, each with their own relevant assumptions.
If an order _attribute is given, it must be a function symbol that takes two arguments of sort and returns Bool, where is the sort of the objective term. The function should either be a built-in symbol or have been defined using define-fun, and the term ( ), for variables and of sort , must define a strict partial order. If the :order attribute is omitted, then for the following sorts, a default is used. The standard arithmetic less-than operator < is the default for Int or Real sorts, the bvult operator for bitvector sorts, fp.lt for floating-point sorts, and str.< for string sorts. For other sorts, if no order is provided, solvers may either use a solver-specific default or respond with unsupported.
Finally, a strategy _attribute can be specified. Strategies include STRATEGY_LINEAR and STRATEGY_BINARY. The first instructs the solver to use a linear strategy, meaning that it repeatedly tries to improve the value of the objective term simply by adding a constraint that it be better than the previous value. The binary strategy uses a binary search, which can be more eficient than linear search in some cases. If upper and lower bounds are not provided, the solver can use any method to establish a starting point for the search. Solver-specific strategy attributes are also allowed.
This command defines a GOMT problem ⟨, ≺ , ⟩, where is the given objective term, ≺ is the given or default order, if the kind is OBJECTIVE_MIN, and the converse of the given or default order, if the kind is OBJECTIVE_MAX. The constraint is the conjunction of all bounds and assumptions.. Example 1. Suppose we want to find the maximum value that an unsigned 8-bit bitvector can take, subject to the constraint that its value must be even—that is, its least significant bit must be 0—and its most significant bit must be 1.
We present three solutions. The first version includes the evenness constraint as part of the objective, uses a define-fun command to define the order, and specifies that a binary search should be used. It enforces that the most significant bit must be 1 by specifying lower and upper bounds for the search. (declare-const bv_var (_ BitVec 8)) (define-fun ord ((x (_ BitVec 8)) (y (_ BitVec 8))) Bool
(bvult x y))
(define-objective obj1a OBJECTIVE_MAX bv_var
:order ord
:assumption (= (bvand bv_var #b00000001) #b00000000)
:strategy STRATEGY_BINARY
:lower #b10000000
:upper #b11111111)
The second version uses a linear strategy, specifically specifies that
and moves all constraints to background assertions.
(define-objective obj1b OBJECTIVE_MAX bv_var
:order bvult
:strategy STRATEGY_LINEAR)
bvult is to be used for the order,
The final version is the same as the previous one, except that we don’t specify the order at all. The
solver uses bvult for the order since that is the default for bitvector sorts.
Example 2. Consider a single-objective optimization problem using linear real arithmetic: given the line
3 + 5 + 1 = 0 and an interval constraint ∈ [
We can encode the example as follows. Again, no order is specified, so the solver uses the arithmetic less-than operator. We also do not specify a strategy, so the solver will use its default strategy. (declare-const x () Real) (declare-const y () Real) (assert (= (+ (* 3 x) (* 5 y) 1) 0)) (assert (and (>= x (- 3)) (<= x 3))) (define-objective obj2 OBJECTIVE_MIN y) Multi-Objective The define-multi-objective command defines a multi-objective optimization problem. The arguments are: a name for the objective, a multi-objective kind, and a sequence of previously declared objectives. Solver-specific attributes can also be optionally supplied as arguments.
This command also defines a GOMT problem ⟨, ≺ , ⟩, formed by composing the objectives provided
according to the multi-objective kind. A full description of how this is done is given in [
Example 3. Let obj3str and obj3lia be two single objectives over the theories of strings and linear integer arithmetic, respectively. The objective obj3str maximizes the string s according to the lexicographic order using the linear search strategy, while the objective obj3lia minimizes the integer int_ub_len_s using the binary search strategy with an upper bound of 3. We also wish for the integer variable int_ub_len_s to serve as an upper bound on the length of the string s. For simplicity, assume that strings are over characters ranging only from ’a’ to ’z’.
We can encode the problem of finding a Pareto-optimal value for the two objectives as follows. (declare-const s String) (declare-const int_ub_len_s Int) Note that we provide an upper bound for the first objective but no lower bound. In such cases, the solver can either infer a lower bound (in this case, a lower bound of 1 can be inferred from the first assertion), use heuristics to attempt to guess and check a lower bound, or use a diferent search strategy. There are three Pareto-optimal solutions to this problem: {int_ub_len_s → 1, s → ""}, {int_ub_len_s → 2, s → "z"}, and {int_ub_len_s → 3, s → "zz"}.
We next encode the problem of finding a lexicographically minimal solution. The order in which we provide the objectives in the define-multi-objective command determines the lexicographic order used when optimizing. The unique solution to this problem is {s → "", int_ub_len_s → 1}.
Box optimization can be used to solve obj3lia and obj3str independently as follows. (declare-const s String) (declare-const int_ub_len_s Int) (assert (< (str.len s) int_ub_len_s)) Here, obj3str is unbounded, meaning that for every string , there is a larger string satisfying all constraints. This is possible because the upper bound constraint :upper 3 applies only to obj3lia, meaning it does not have to be satisfied when optimizing obj3str, since with box optimization, each objective is optimized completely independently. On the other hand, obj3lia has a unique optimal solution: {int_ub_len_s → 1, s → ""}.
Example 4. Given two lines + + 1 = 0 and − + 2 = 0 and a circle 2 + 2 = 1, find a point (, ) on the circle that is as far as possible from the closer of the two lines.
We can encode this as a MaxMin problem as follows. To simplify the objective terms, we use the squared distance from the point (, ) to each line as the optimization objective. (declare-const x Real) (declare-const y Real) (define-objective obj4a OBJECTIVE_MIN (/ (* (+ x y 1) (+ x y 1)) 2)) (define-multi-objective obj4 OBJECTIVE_MAXMIN obj4a obj4b) The exact optimal solution to this problem is at the point (, ) = (√3/2, 1/2). The value of obj4 at this point is 1/2+3√3/4. Since these are irrational values, they cannot be exactly represented using rational constants. However, an approximation can be computed and returned—this is discussed further in Section 4, which covers examples of various OMT command responses.
Note that define-multi-objective does not permit the inclusion of an objective_attribute. Strategies and assumptions can only be provided at the single objective level. However, solver-specific extensions can provide additional attributes at the multi-objective definition stage.
MaxSMT The define-maxsmt-objective command initiates the definition of a MaxSMT objective by assigning it a name. The semantics is that a hidden GOMT objective ⟨, ≺ , ⟩ is created, where ≺ is arithmetic greater-than, >, and is True. Initially, is set to 0.0. However, it changes every time an assert-soft command is issued.
We adopt the assert-soft command from the OptiMathSAT OMT syntax extension [
It is important to note that the objective term in a MaxSMT objective is not explicitly shown but is implicitly associated with obj and internally constructed by the solver. A MaxSMT definition may also include strategy attributes, which are applied as usual, but to the hidden GOMT objective. Example 5. Consider a MaxSMT example with ≥ 0 and ≥ 0 as hard constraints and 4 + − 4 ≥ 0 and 2 + 3 − 6 ≥ 0 as soft constraints, with the weights 2.0 and 1.0, respectively.
Recall that the goal is to satisfy all hard constraints and as many soft constraints as possible. The problem can be encoded as follows. (declare-const x Int) (declare-const y Int) (assert (>= x 0) (assert (>= y 0) (define-maxsmt-objective obj5) (assert-soft (>= (- (+ (* 4 x) y) 4) 0) :objective obj5 :weight 2.0) (assert-soft (>= (- (+ (* 2 x) (* 3 y)) 6) 0) :objective obj5) A solution to this problem is the point (, ) = (1, 2), which satisfies both soft constraints. The hidden objective thus has the maximum possible value of 3. There are infinitely many solutions which achieve this optimal value.
The dual of MaxSMT is MinSMT, in which we want to satisfy as few soft assertions as possible. We do not explicitly support MinSMT objectives. However, a MinSMT problem can easily be converted into a MaxSMT problem simply by negating all of the soft assertions.
The optimize-sat command takes as an argument the name of an objective and instructs the solver to ifnd an optimal solution for that objective. Zero or more instances of assumption_attribute provide additional assumptions that must be satisfied by any solution. Additional solver-specific attributes may also be provided. The solver should aim to compute an optimal solution for the GOMT problem associated with the objective name that also satisfies all assertions currently in the context as well as any bounds and assumptions associated with the objective or assumptions provided as arguments to the optimize-sat command. If one or more search strategies is associated with the objective, the solver should follow those strategies during its search for an optimal solution if possible.
There are several possible responses to an optimize-sat command: • optimal indicates that the solver has found an optimal solution to the GOMT problem for the specified objective. • limit-optimal indicates that the solver has found a solution to the GOMT problem. The solution found is not optimal, but () no optimal solution exists; and () the amount that the found solution can be improved is bounded. • unbounded indicates that the solver has found a solution and also determined that for every solution to the given problem, a solution exists that is better by more than any bounded amount. • non-optimal indicates that the solver found a solution but not an optimal solution, and the solver was not able to determine the problem to be in either the limit-optimal or unbounded categories. • unsat indicates that the constraints of the problem alone (without considering optimization) are unsatisfiable • unknown indicates that the solver is unable to find a solution, is unable to determine that the problem is unsat, and is unable to further categorize the problem.
If the most recent optimized objective is of kind OBJECTIVE_BOX, then instead of returning a single response, the solver returns a list of responses, one for each boxed objective.
The optimize-sat-next command is available immediately after a successful (response of optimal) call to optimize-sat or optimize-sat-next. It instructs the solver to attempt to find an optimal solution to the same problem it just solved (with the same constraints) that is diferent from those computed so far, if any. If there are no additional optimal solutions, it returns unsat. Otherwise, the set of possible responses are the same as above.
Anytime Optimization The optimize-sat command can, optionally, respect SMT-LIB’s resource limiting options, such as :reproducible-resource-limit. If the solver’s optimization routine supports this option, setting it to 0 disables it. Setting it to a non-zero numeral , causes the optimize-sat command to terminate within a bounded amount of time dependent on . As in SMT solving, the internal implementation of the :reproducible-resource-limit option and its relation to run time or other concrete resources can be solver-specific. However, if the solver cannot find an optimal solution within the resource limit and cannot determine whether the problem is unsatisfiable, unbounded, or limit-optimal, then optimize-sat must return either unknown or non-optimal. It returns unknown if no solution (even a non-optimal one) has been found, and returns non-optimal if some solution has been found. In the latter case, the best solution found so far can be retrieved upon request. This behavior is in line with both standard SMT solving with resource limits and MaxSAT anytime solving.
We propose adding or modifying the three get commands described below.
The get-value command is overloaded to take as an argument a list of objective names. This version of get-value is available after a call to optimize-sat or optimize-sat-next that returns anything other than unsat or unknown. It returns a list of pairs, each of which contains an objective name as the ifrst element of the pair and the corresponding value of that objective’s objective term in the computed solution as the second element of the pair.
The get-model command is similarly available whenever the most recent invocation of optimize-sat or optimize-sat-next returns something other than unsat or unknown. It returns a representation of the computed model that is a solution to the optimization problem, using the same format as is used in the SMT-LIB 2.7 standard. There is one exception to this. If the most recent optimized objective is of kind OBJECTIVE_BOX, then get-model instead returns a list of pairs. The first element of each pair is the name of one of the boxed objectives, and the second element is the model for that objective.
The get-info command can be used to query the solver for additional information about the most recent optimization attempt if that attempt returned either :limit-optimal or :unbounded. In addition, if that attempt was for an objective of kind OBJECTIVE_BOX, then the first argument of get-info is the name of the sub-objective (within the set of boxed objectives) for which information is requested. Otherwise, that argument is omitted. In either case, it always takes an argument specifying the value returned, indicating that more information is desired about that value. There are two possible values: :limit-optimal and :unbounded.
In the first case, issuing the command get-info :limit-optimal returns an explanation of what the solver knows about the limit-optimality, such as some value that is approached in the limit by the objective. In the second case, issuing the command get-info :unbounded provides details on the cause of unboundedness, such as whether the solver can determine if the objective term tends toward positive or negative infinity. In both cases, the solver should return a term, and the specific format of the term is solver-specific (i.e., it could be a string literal or it could have a richer term structure).
In this section, we show several full examples illustrating diferent commands and responses. We first revisit Example 1. (set-logic QF_BV) (set-option :produce-models true) (set-option :enable_omt true) (declare-const bv_var (_ BitVec 8)) (assert (= (bvand bv_var #b00000001) #b00000000)) (assert (= ((_ extract 7 7) bv_var) #b1))
optimal ((obj1c #b11111110)) ( (define-fun bv_var () (_ BitVec 8) #b11111110) ) The initial response is optimal. The result of the call to get-value shows that the objective term of obj1c has the value #b11111110 in the optimal solution. And the call to get-model simply returns the definition of the objective term, since it is the only user-declared symbol.
We next consider an example that tries to minimize the value of 1/. (set-logic QF_LRA) (set-option :produce-models true) (set-option :enable_omt true) (declare-const x Real) (assert (> x 0)) (define-objective obj6 OBJECTIVE_MIN (/ 1 x)) (optimize-sat obj6) (get-value (obj6)) (get-model) (get-info :limit-optimal) A possible output from a solver is shown below. limit-optimal ((obj6 0.0001)) ( (define-fun x () Real) 10000.0) ) (:limit-optimal "As x approaches infinity, the objective term approaches 0.") Since the objective approaches but never reaches 0, the call to optimize-sat returns limit-optimal. In this case, the solver finds a model that is within 10− 4 of the limit value. The request for more information returns a string explaining the limit.
We next revisit Example 4 with additional commands below. (set-logic QF_NRA) (set-option :produce-models true) (set-option :enable_omt true) (declare-const x Real) (declare-const y Real) (define-objective obj4b OBJECTIVE_MIN (/ (* (+ x (* -1 y) 2) (+ x (* -1 y) 2)) 2)) (define-multi-objective obj4 OBJECTIVE_MAXMIN obj4a obj4b) (optimize-sat obj4) (get-value (obj4)) (get-model) Recall that the exact optimal solution is when (, ) = (√3/2, 1/2). However, since the value of is an irrational, we cannot represent it precisely. The value of obj4 at this point is also irrational (1/2+3√3/4). This is another example where a response of limit-optimal would be appropriate. However, a solver that is unable to figure this out might instead return non-optimal and then return a decimal approximation for x, y, and the objective term. One possible solver output is shown below. non-optimal ((obj4 (800/289, 1681/578))) ( (define-fun x () Real (/ 15 17)) (define-fun y () Real (/ 8 17)) ) (set-logic QF_LRA) (set-option :produce-models true) (set-option :enable_omt true) (declare-const x Real) (assert (> x 0)) (define-objective obj7 OBJECTIVE_MAX x) (optimize-sat obj7) (get value (obj7)) (get-model) (get-info :unbounded)
Here, , , and the objective term are approximated with rational constants.
We next show an example with an unbounded objective. unbounded ((obj7 100000.0)) ( (define-fun x () Real) 100000.0) ) (:unbounded "The objective term approaches positive infinity as x approaches positive infinity.")
The final example illustrates the use of the optimize-sat-next command with Example 3. It outputs all three Pareto-optimal solutions, each preceded by the optimal response. (set-logic QF_SLIA) (set-option :produce-models true) (set-option :enable_omt true) (declare-const s String) (declare-const int_ub_len_s Int) A possible output may be like the one below. optimal ((obj3par (1, ""))) ( (define-fun int_ub_len_s () Int 1) (define-fun s () String "") ) optimal ((obj3par (2, "z"))) ( (define-fun int_ub_len_s () Int 2) (define-fun s () String "z") ) optimal ((obj3par (3, "zz"))) ( (define-fun int_ub_len_s () Int 3) (define-fun s () String "zz") ) unsat
The lack of a standardized SMT-LIB syntax for OMT remains a significant obstacle to the broad adoption and interoperability of OMT tools. To address this, we have proposed a concrete extension of the SMT-LIB v2.7 standard that can express all of the optimization modulo theories problems from the OMT literature. These extensions enhance both expressiveness and flexibility, making it possible to encode more complex optimization constructs, such as optimization with respect to any definable partial order, as well as arbitrary combinations of single- and multi-objective problems found in the literature, including MaxSMT and MinSMT. Future work will focus on refining the syntax through community feedback and assembling a representative suite of OMT benchmarks. Ultimately, this efort aims to enable more robust, reusable, and comparable OMT solutions, supporting the growing demand for optimization in formal methods, automated reasoning, and among end users.
Acknowledgments This work was supported in part by the Stanford Agile Hardware Center, the Stanford Center for Automated Reasoning, and by the National Science Foundation (grant 2006407). Declaration on Generative AI The authors used ChatGPT and Overleaf for spell check and targeted edits. After using these tools, the authors reviewed and edited content as needed and take full responsibility for the publication’s content.