Z3 优化中的间隙公差控制

Question

我想使用 z3 optimize class 来获得次优结果，同时仍然能够控制我与最佳结果的差距。我正在使用 C++ API.

例如，CPLEX 具有分别用于相对和绝对容差的参数 epgap 和 epagap。它使用当前的下限或上限（取决于它是最小化还是最大化）来评估（最多）当前解决方案与最佳解决方案的距离。

当近似解已经足够好时，这会缩短运行次。

这是否可以使用优化 class，或者这是我需要使用求解器实例来实现并自己控制边界的东西吗？

Answer 1

我不是很确定，但我怀疑z3有这样的参数。

可以肯定的是，在命令行界面中似乎没有公开任何类似内容：

~$ 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)
 ...

备选 #01:

一个选择是在 z3 之上自己实现它。

我建议使用 二元搜索 模式（参见 Optimization in SMT with LA(Q) Cost Functions），否则 OMT 求解器将只优化优化搜索区间的一端，而这可能会破坏您的 搜索终止条件 .

的预期目的

请注意，为了使这种方法有效，重要的是在搜索过程中遇到的每个中间模型的布尔赋值调用内部 T-optimizer。 （我不确定此功能是否在 API 级别与 z3 公开）。

您可能还想看看 Puli - A Problem-Specific OMT Solver 中使用的基于 线性回归 的方法。如果适用，它可能会加速优化搜索并改进对与最优解的相对距离的估计。

备选 #02:

OptiMathSAT 可能会在 API 和命令行级别公开您正在寻找的功能：

~$ 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)

中止间隔是基于当前的绝对大小的终止标准优化搜索间隔，而 abort tolerance 是基于 current 的 relative 大小的终止标准相对于初始搜索间隔的优化搜索间隔。

请注意，为了使用这些终止条件，用户需要：

为任何最小化提供（至少）初始下限 objective:
```
(minimize ... :lower ...)
```
为任何最大化提供（至少）初始上限 objective:
```
(maximize ... :upper ...)
```

此外，该工具必须配置为使用 二进制 或 自适应 搜索：

 -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.

如果您对这些终止标准都不满意，您也可以在 OptiMathSAT 之上实现自己的算法。由于可以通过 API 和命令行设置以下选项，这相对容易做到：

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

启用后，它使 OptiMathSAT 的行为类似于常规的 SMT 求解器，除了当它找到一个完整的布尔赋值且存在输入公式的模型时，它会确保该模型是最优的。 objective 函数和给定的布尔赋值 （换句话说，它为您调用内部 T-optimizer 过程）.

一些想法。

OMT 求解器的工作方式与大多数 CP 求解器不同。他们使用无限精度算法，优化搜索由 SAT 引擎引导。改进 objective 函数的值变得越来越困难，因为 OMT 求解器被迫枚举越来越多（可能是全部）的布尔赋值，同时解决冲突并沿途回跳。

在我看来，当前搜索区间的大小并不总是一个很好的指标，表明优化搜索取得进展的相对难度。有太多因素需要考虑，例如涉及 objective 函数的冲突子句的修剪能力、输入公式的编码等。这也是为什么，据我所知，OMT 社区中的大多数人只是使用固定的 timeout 而不是费心使用任何其他 termination 的原因之一标准。我发现它特别有用的唯一情况是处理 非线性 优化 （但是，OptiMathSAT 尚未公开） .

Z3 优化中的间隙公差控制

Gap tolerance control in Z3 optimization

optimization

z3

optimathsat