Z3优化的超时

Question

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

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

后续问题，你能把z3设置为随机爬山，还是它总是执行一个完整的搜索？

Answer 1

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

然而，对于数值量，z3确实跟踪变量的界。您可能能够提取这些值，但是通常情况下，您将无法知道从这些间隔中选择哪些值才能为整个问题找到令人满意的解决方案。有关讨论，请参见以下答案：在Z3中使用SMT约束时，是否可以获得合法的范围信息？

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

• Z3时间限制优化
• z3最小化和超时

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

你最好的选择

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

1. 陈述你的问题
2. 找个模特。如果没有模型，请响应unsat。放弃吧。
3. 坚持目前的模式为“迄今为止最好的”。
4. 没时间了？把你拥有的模型归为“目前为止最好的”。你完了。
5. 还有时间吗？ 5a。计算该模型的“成本”。也就是说，你试图最小化或最大化的度量。如果将成本作为变量存储在模型中，则可以简单地从模型中查询其值。 5b。声明一个新的约束，认为成本应该低于当前模型的成本。(如果你是在最大化的话，就更高了。)根据您想要的花哨程度，您可能希望将成本函数“加倍”，或者实现某种二进制搜索，以便更快地收敛于某个值。但这一切实际上取决于问题的具体细节。 5c.要新型号的。如果是unsat，返回最后一个模型为“最优”。否则，从步骤3重复。

我认为这是z3中最实用的时间约束优化方法.它让您完全控制迭代次数，并以任何您想要的方式指导搜索。(例如，您可以在每个模型中查询各种变量，并通过这样的方式指导搜索：“给我找一个更大的x或更小的y等等，而不是只看一个度量。)

摘要

请注意，SMT求解程序可以像您所描述的那样工作，也就是说，当超时发生时，给出一个最优的解决方案。只是Z3的优化器不是这样工作的。对于z3，我发现上面描述的迭代循环是这种基于超时的优化最实用的解决方案。

您还可以查看OptiMathSAT (http://optimathsat.disi.unitn.it/)，它可能在这方面提供更好的功能。@Patrick经常阅读这个论坛，他是这方面的专家，他可能会对它的用法提出不同的看法。

Answer 2

通常，@别名是正确的，当他声明当OMT求解器被timeout信号打断时，在优化搜索结束时不提供任何解决方案的保证。

OMT求解程序可以通过以下两种方法中的一种寻找最优解：

• 从公式的初始模型开始，试图改进目标函数的值，这是标准OMT方法的情况，它列举了一些部分优化的解，直到找到最优解为止。
• 通过从超过最优、不可满足的分配开始，并逐步放松这类分配直到得到最优解；AFAIK，这只是处理MaxSMT问题的最大分辨率引擎的情况。

当OMT求解器使用属于第一类的优化技术时，如果OMT求解器在优化搜索期间将其存储在安全的位置，则可以在其耗尽时间时检索最知名的解决方案。第二个MaxRes引擎的情况并非如此(参见本问答)。

--可能的解决办法。(请注意:我还没有测试这个) z3沿着优化搜索跟踪目标函数的lower和upper界限。当最小时，upper界对应于OMT求解器最近发现的部分解中目标函数的值(对偶表示最大化)。在超时信号发生后，最小化(resp )。最大化)从obj (resp )获得的一个minimize()实例。maximize())，我们应该能够通过调用obj.upper() (resp )来检索obj最优值的最新近似v。obj.lower())。假设这样的值v不同于+oo (resp )。( -oo)，可以逐步学习cost = 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]信号的类型。

示例：下面的示例是包含在我的示例 github存储库中的timeout.py单元测试，它提供了许多如何使用OptiMathSAT的Python接口的示例。

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