Gap tolerance control in Z3 optimization

Question

I would like to use z3 optimize class to get sub-optimal results, while still being able to control how far am I from the optimum result. I am using the C++ API.

As an example, CPLEX has the parameters epgap and epagap for relative and absolute tolerance respectively. It uses the current lower or upper bounds (depending if it is a minimization or maximization) to assess how far (at most) the current solution is from the optimal one.

This leads to shorter run-times for when an approximate solution is already good enough.

Is this possible using the optimize class, or is this something I would need to implement using a solver instance and control the bounds myself?

Answer 1

I am not absolutely certain about this, but I doubt that z3 has such parameters.

For sure, nothing like that appears to be exposed in the command-line interface:

~$ z3 -p
...
[module] opt, description: optimization parameters
    dump_benchmarks (bool) (default: false)
    dump_models (bool) (default: false)
    elim_01 (bool) (default: true)
    enable_sat (bool) (default: true)
    enable_sls (bool) (default: false)
    maxlex.enable (bool) (default: true)
    maxres.add_upper_bound_block (bool) (default: false)
    maxres.hill_climb (bool) (default: true)
    maxres.max_core_size (unsigned int) (default: 3)
    maxres.max_correction_set_size (unsigned int) (default: 3)
    maxres.max_num_cores (unsigned int) (default: 4294967295)
    maxres.maximize_assignment (bool) (default: false)
    maxres.pivot_on_correction_set (bool) (default: true)
    maxres.wmax (bool) (default: false)
    maxsat_engine (symbol) (default: maxres)
    optsmt_engine (symbol) (default: basic)
    pb.compile_equality (bool) (default: false)
    pp.neat (bool) (default: true)
    priority (symbol) (default: lex)
    rlimit (unsigned int) (default: 0)
    solution_prefix (symbol) (default: )
    timeout (unsigned int) (default: 4294967295)
 ...

---

Alternative #01:

An option is to implement this yourself on top of z3.

I would suggest using the binary search schema (see Optimization in SMT with LA(Q) Cost Functions), otherwise the OMT solver is going to refine only one end of the optimization search interval and this may defeat the intended purpose of your search-termination criteria.

Notice that in order for this approach to be effective, it is important that the internal T-optimizer is invoked over the Boolean assignment of each intermediate model encountered along the search. (I am not sure whether this functionality is exposed at the API level with z3).

You may also want to take a look at the approach based on linear regression used in Puli - A Problem-Specific OMT Solver. If applicable, it may speed-up the optimization search and improve the estimate of the relative distance from the optimal solution.

---

Alternative #02:

OptiMathSAT may be exposing the functionality you are looking for, both at the API and the command-line level:

~$ optimathsat -help
Optimization search options:
 -opt.abort_interval=FLOAT
          If greater than zero, an objective is no longer actively optimized as 
          soon as the current search interval size is smaller than the given 
          value. Applies to all objective functions. (default: 0) 
 -opt.abort_tolerance=FLOAT
          If greater than zero, an objective is no longer actively optimized as 
          soon as the ratio among the current search interval size wrt. its 
          initial size is smaller than the given value. Applies to all 
          objective functions. (default: 0) 

The abort interval is a termination criterion based on the absolute size of the current optimization search interval, while the abort tolerance is a termination criterion based on the relative size of the current optimization search interval with respect to the initial search interval.

Notice that in order to use these termination criteria, the user is expected to:

• provide (at least) an initial lower-bound for any minimization objective:

  (minimize ... :lower ...)
  

• provide (at least) an initial upper-bound for any maximization objective:

  (maximize ... :upper ...)
  

Furthermore, the tool must be configured to use either Binary or Adaptive search:

 -opt.strategy=STR
          Sets the optimization search strategy: 
           - lin : linear search (default)
           - bin : binary search
           - ada : adaptive search
          A lower bound is required to minimize an objective with bin/ada 
          search strategy. Dual for maximization. 

In case neither of these termination criterion is satisfactory to you, you can also implement your own algorithm on top of OptiMathSAT. It is relatively easy to do, thanks to the following option that can be set both via API and command-line:

 -opt.no_optimization=BOOL
          If true, the optimization search stops at the first (not optimal) 
          satisfiable solution. (default: false) 

When enabled, it makes OptiMathSAT behave like a regular SMT solver, except that when it finds a complete Boolean assignment for which there exists a Model of the input formula, it ensures that the Model is optimal wrt. the objective function and the given Boolean assignment (in other words, it invokes the internal T-optimizer procedure for you).

---

Some Thoughts.

OMT solvers work differently from most CP solvers. They use infinite-precision arithmetic and the optimization search is guided by the SAT engine. Improving the value of the objective function becomes increasingly difficult because the OMT solver is forced to enumerate a progressively larger number of (possibly total) Boolean assignments while resolving conflicts and back-jumping along the way.

In my opinion, the size of the current search interval is not always a good indicator of the relative difficulty of making progress with the optimization search. There are far too many factors to take into consideration, e.g. the pruning power of conflict clauses involving the objective function, the encoding of the input formula, and so on. This is also one of the reasons why, as far as I have seen, most people in the OMT community simply use a fixed timeout rather than bothering to use any other termination criteria. The only situation in which I have found it to be particularly useful, is when dealing with non-linear optimization (which, however, is not yet publicly available with OptiMathSAT).