您如何为z3优化器设置超时，以使其在时间用尽时为您提供最知名的解决方案？
from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())
后续问题，您可以将z3设置为随机爬山还是始终执行完整搜索？
简短的简短回答，您不能。那根本不是优化器的工作方式。也就是说，它找不到解决方案，然后尝试对其进行改进。如果您中断它或设置超时，则当计时器到期时，它甚至可能没有令人满意的解决方案，更不用说“改进”了。您应该查看优化文件以获取详细信息：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是这方面的专家，他可能会就其用法单独提出意见。
[通常，@alias正确，当他说OMT求解器不能为优化搜索结束时被timeout信号打断时，不能提供任何保证。