我想使用z3优化类来获得次优的结果，同时仍然能够控制我离最优结果有多远。我正在使用C ++ API。
例如，CPLEX分别具有参数epgap和epagap用于相对和绝对公差。它使用当前的上下限（取决于是最小化还是最大化）来评估当前解决方案与最佳解有多远（最多）。
这样可以缩短近似解决方案的运行时间。
是否可以使用optimize类，或者这是我需要使用求解器实例来实现并自己控制范围的事情吗？
我对此不确定，但我怀疑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之上自行实现。
我建议使用binary search模式（请参阅Optimization in SMT with LA(Q) Cost Functions），否则OMT求解程序将仅优化优化搜索间隔的一端，这可能会破坏您的search-终止条件。
注意，为了使此方法有效，重要的是，在搜索过程中遇到的每个中间模型的布尔分配上调用内部T-optimizer。 （（我不确定此功能是否通过z3在API级别公开。
您可能还想看看基于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 interval是基于current优化搜索间隔的absolute大小的终止标准，而abort tolerance是基于 当前优化搜索间隔相对于initial搜索间隔的大小。
请注意，为了使用这些终止条件，用户应该：
（至少）为任何最小化目标提供初始下限：
(minimize ... :lower ...)
（至少）为任何最大化目标提供初始上限：
(maximize ... :upper ...)
此外，该工具必须配置为使用Binary或Adaptive搜索：
-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社区中的大多数人只是使用固定的[[timeout
而不是费心使用任何其他终止标准的原因之一。我发现它特别有用的唯一情况是在处理non-linear优化（但是，尚未在OptiMathSAT中公开提供）。