我想使用 z3 优化类来获得次优结果，同时仍然能够控制我离最佳结果有多远。我正在使用C++ API。
例如，CPLEX 具有参数 epgap 和 epagap 分别表示相对公差和绝对容差。它使用当前的下限或上限(取决于它是最小化还是最大化(来评估当前解决方案与最佳解决方案的距离(最多(。
当近似解决方案已经足够好时，这可以缩短运行时间。
这是否可以使用优化类，或者这是我需要使用求解器实例实现并自己控制边界的东西？
我对此不是绝对确定的，但我怀疑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之上自己实现这一点。
我建议使用二叉搜索模式(请参阅使用 LA(Q( 成本函数在 SMT 中进行优化(，否则 OMT 求解器将仅细化优化搜索间隔的一端，这可能会破坏搜索终止条件的预期目的。
请注意，为了使此方法有效，在搜索过程中遇到的每个中间模型的布尔赋值上调用内部T-optimizer非常重要。(我不确定此功能是否在 API 级别使用z3公开(。
您可能还想看看 Puli - 特定于问题的 OMT 求解器中使用的基于线性回归的方法。如果适用，它可以加快优化搜索并改进与最优解的相对距离的估计。
替代方案 #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尚未公开提供(。