3

我想使用 z3 优化类来获得次优结果，同时仍然能够控制我与最佳结果之间的距离。我正在使用 C++ API。

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

当近似解决方案已经足够好时，这会导致运行时间更短。

这可能使用优化类，还是我需要使用求解器实例来实现并自己控制边界？

4

1 回答 1

2

我对此并不完全确定，但我怀疑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)

中止间隔是基于当前优化搜索间隔的绝对大小的终止准则，而中止容限是基于当前优化搜索间隔相对于初始搜索间隔的相对大小的终止准则。

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

  • 为任何最小化目标提供（至少）一个初始下限：

    (minimize ... :lower ...)

  • 为任何最大化目标提供（至少）一个初始上限：

    (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 求解器，除了当它找到存在输入公式模型的完整布尔分配时，它确保模型是最优的。目标函数和给定的布尔赋值（换句话说，它T-optimizer为您调用内部过程）。

一些想法。

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

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

于 2019-12-13T09:36:40.053 回答