optimization - Z3 优化超时

Question

您如何为 z3 优化器设置超时，以便在超时时为您提供最知名的解决方案？

from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())

后续问题，您可以将 z3 设置为随机爬山还是始终执行完整搜索？

score 5 · Accepted Answer

长回答短，你不能。这根本不是优化器的工作方式。也就是说，它没有找到解决方案，然后尝试改进它。如果您中断它或设置超时，当计时器到期时，它甚至可能没有令人满意的解决方案，更不用说以任何方式“改进”了。您应该查看优化论文以了解详细信息：https ://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

然而，对于数值量，z3 确实跟踪变量的界限。您可能能够提取这些，但一般来说，您无法知道您需要从这些间隔中选择哪些值才能为整个问题获得令人满意的解决方案。请参阅此答案进行讨论：Is it possible to get a legit range info when using a SMT constraint with Z3

这种“爬山”的问题经常出现在这个论坛上。答案很简单，这不是 z3 优化器的工作方式。这种方式的一些先前的问题：

在堆栈溢出中几乎没有其他问题。搜索“优化”和“超时”。

你最好的选择

这就是它的理论方面。在实践中，我认为处理此类问题的最佳方法是根本不使用优化器。而是执行以下操作：

陈述你的问题
求个模型。如果没有模型，请回复unsat。退出。
将当前模型保持为“迄今为止最好的”
没时间了？将您拥有的模型返回为“迄今为止最好的”。你完成了。
还有时间吗？

5a。计算这个模型的“成本”。即，您尝试最小化或最大化的指标。如果您将成本作为变量存储在模型中，您可以简单地从模型中查询其值。

5b。断言一个新的约束，说成本应该低于当前模型的成本。（如果您要最大化，则更高。）根据您想要获得的花哨程度，您可能希望将成本函数“加倍”，或者实施某种二进制搜索以更快地收敛到一个值。但这一切实际上取决于问题的确切细节。

5c。求一个新模型。如果unsat，则将您获得的最后一个模型返回为“最佳”。否则，从第 3 步开始重复。

我相信这是 z3 中时间约束优化最实用的方法。它使您可以完全控制迭代次数，并以您想要的任何方式引导搜索。（例如，您可以查询每个模型的各种变量，并通过说“给我找一个更大x的或更小y的等，而不是只看一个指标来指导搜索。）希望这是有道理的。

概括

请注意，SMT 求解器可以像您所描述的那样工作，即在超时消失时为您提供迄今为止最佳的解决方案。只是z3的优化器不是这样工作的。对于 z3，我发现上面描述的迭代循环是这种基于超时的优化的最实用的解决方案。

您还可以查看 OptiMathSAT ( http://optimathsat.disi.unitn.it/ )，它可能在这方面提供更好的设施。@Patrick Trentin 经常阅读这个论坛，是这方面的专家，他可能会就其用法单独发表意见。

score 4 · Accepted Answer

一般来说，@alias是正确的，他指出 OMT 求解器不保证在优化搜索结束时解决方案被timeout信号中断时可用。

OMT 求解器可以通过以下两种方式之一寻找最优解：

通过从公式的初始模型开始并尝试提高目标函数的值；标准 OMT 方法就是这种情况，它列举了许多部分优化的解决方案，直到找到最佳解决方案。
从超过最优的、不可满足的分配开始，并逐渐放宽这种分配，直到它产生最佳解决方案；AFAIK，这只是用于处理 MaxSMT 问题的最大分辨率引擎的情况。

当 OMT 求解器使用属于第一类的优化技术时，如果 OMT 求解器在优化搜索期间将其存储在安全的地方，则可以在时间用完时检索最佳已知解决方案。第二个 MaxRes 引擎不是这种情况（请参阅此 Q/A）。

一种可能的解决方法。 （警告：我没有测试过这个） 沿着优化搜索z3跟踪目标函数lower的边界。upper最小化时，upper边界对应于 OMT 求解器找到的最近部分解中的目标函数的值（最大化对偶）。obj在最小化（或最大化）从minimize()(resp. ) 获得的实例时发生超时信号后maximize()，应该能够通过调用(resp. )检索v的最佳值的最新近似值。假设这样的值与(resp. ) 不同，可以逐步学习形式的约束objobj.upper()obj.lower()v+oo-oocost = v并执行可满足性的增量 SMT 检查，以重建与遇到的次优解决方案相对应的模型z3。

OptiMathSAT是一种 OMT 求解器，可将在优化搜索期间遇到的最新解决方案存储在安全的地方。这使您可以轻松实现您想要做的事情。

中有两种类型的timeout信号OptiMathSAT：

硬超时：一旦timeout触发，优化搜索立即停止；如果 OMT 求解器找到任何解，则优化搜索的结果（可通过访问msat_objective_result(env, obj)）是MSAT_OPT_SAT_PARTIAL，并且可以提取和打印与最新的次优解对应的模型；相反，如果 OMT 求解器没有找到任何解，则优化搜索的结果是MSAT_UNKNOWN并且没有可用的模型。
软超时：如果timeout在 OMT 求解器找到任何解决方案后触发，则搜索将立即停止，就像硬超时的情况一样。否则，timeout忽略直到OMT 求解器找到一个解。

timeout可以使用选项设置信号类型opt.soft_timeout=[true|false]。

示例：以下示例是包含在我的omt_python_examples github 存储库中的 timeout.py单元测试，其中包含许多如何使用.OptiMathSAT

"""
timeout unit-test.
"""

###
### SETUP PATHS
###

import os
import sys

BASE_DIR = os.path.dirname(os.path.abspath(__file__))
INCLUDE_DIR = os.path.join(BASE_DIR, '..', 'include')
LIB_DIR = os.path.join(BASE_DIR, '..', 'lib')
sys.path.append(INCLUDE_DIR)
sys.path.append(LIB_DIR)

from wrapper import * # pylint: disable=unused-wildcard-import,wildcard-import

###
### DATA
###

OPTIONS = {
    "model_generation" : "true",      # !IMPORTANT!
    "opt.soft_timeout" : "false",
    "opt.verbose"      : "true",
}

###
### TIMEOUT UNIT-TEST
###

with create_config(OPTIONS) as cfg:
    with create_env(cfg) as env:

        # Load Hard Problem from file
        with open(os.path.join(BASE_DIR, 'smt2', 'bacp-19.smt2'), 'r') as f:
            TERM = msat_from_smtlib2(env, f.read())
            assert not MSAT_ERROR_TERM(TERM)
            msat_assert_formula(env, TERM)

        # Impose a timeout of 3.0 seconds
        CALLBACK = Timer(3.0)
        msat_set_termination_test(env, CALLBACK)

        with create_minimize(env, "objective", lower="23", upper="100") as obj:
            assert_objective(env, obj)

            solve(env)                    # optimization search until timeout
            get_objectives_pretty(env)    # print latest range of optimization search

            load_model(env, obj)          # retrieve sub-optimal model
            dump_model(env)               # print sub-optimal model

这是优化搜索的详细输出：

# obj(.cost_0) := objective
# obj(.cost_0) - search start: [ 23, 100 ]
# obj(.cost_0) - linear step: 1
# obj(.cost_0) -  new: 46
# obj(.cost_0) -  update upper: [ 23, 46 ]
# obj(.cost_0) - linear step: 2
# obj(.cost_0) -  new: 130/3
# obj(.cost_0) -  update upper: [ 23, 130/3 ]
# obj(.cost_0) - linear step: 3
# obj(.cost_0) -  new: 40
# obj(.cost_0) -  update upper: [ 23, 40 ]
# obj(.cost_0) - linear step: 4
# obj(.cost_0) -  new: 119/3
# obj(.cost_0) -  update upper: [ 23, 119/3 ]
# obj(.cost_0) - linear step: 5
# obj(.cost_0) -  new: 112/3
# obj(.cost_0) -  update upper: [ 23, 112/3 ]
# obj(.cost_0) - linear step: 6
# obj(.cost_0) -  new: 104/3
# obj(.cost_0) -  update upper: [ 23, 104/3 ]
# obj(.cost_0) - linear step: 7
# obj(.cost_0) -  new: 34
# obj(.cost_0) -  update upper: [ 23, 34 ]
# obj(.cost_0) - linear step: 8
# obj(.cost_0) -  new: 133/4
# obj(.cost_0) -  update upper: [ 23, 133/4 ]
# obj(.cost_0) - linear step: 9
# obj(.cost_0) -  new: 161/5
# obj(.cost_0) -  update upper: [ 23, 161/5 ]
# obj(.cost_0) - linear step: 10
# obj(.cost_0) -  new: 32
# obj(.cost_0) -  update upper: [ 23, 32 ]
# obj(.cost_0) - linear step: 11
# obj(.cost_0) -  new: 158/5
# obj(.cost_0) -  update upper: [ 23, 158/5 ]
# obj(.cost_0) - linear step: 12
# obj(.cost_0) -  new: 247/8
# obj(.cost_0) -  update upper: [ 23, 247/8 ]
# obj(.cost_0) - linear step: 13
# obj(.cost_0) -  new: 123/4
# obj(.cost_0) -  update upper: [ 23, 123/4 ]
# obj(.cost_0) - linear step: 14
# obj(.cost_0) -  new: 61/2
# obj(.cost_0) -  update upper: [ 23, 61/2 ]
# obj(.cost_0) - linear step: 15
unknown                                       ;; <== Timeout!
(objectives
  (objective 61/2), partial search, range: [ 23, 61/2 ]
)                                             ;; sub-optimal value, latest search interval

  course_load__ARRAY__1 : 9                   ;; and the corresponding sub-optimal model
  course_load__ARRAY__2 : 1
  course_load__ARRAY__3 : 2
  course_load__ARRAY__4 : 10
  course_load__ARRAY__5 : 3
  course_load__ARRAY__6 : 4
  course_load__ARRAY__7 : 1
  course_load__ARRAY__8 : 10
  course_load__ARRAY__9 : 4
  course_load__ARRAY__10 : 1
  course_load__ARRAY__11 : 1
  course_load__ARRAY__12 : 5
  course_load__ARRAY__13 : 10
  course_load__ARRAY__14 : 9
  course_load__ARRAY__15 : 1
  ...
  ;; the sub-optimal model is pretty long, it has been cut to fit this answer!
  ...

optimization - Z3 优化超时

2 回答 2

你最好的选择

概括

Related

Reference