我正在使用MaxSMT来找到一组软约束和硬约束的解决方案。超时为600秒，我从求解器得到的模型输出对于所有参数都是Nonetype。我期望求解器为我提供次优的解决方案。我认为这是错误的。有人可以解释一下吗？
没有理由期望您在超时后会得到“次优”的解决方案。除非求解器返回肯定的答案，否则您可以搜集到的任何内部信息都只是：有些内部值可能不相关。更重要的是，没有理由期望它甚至会是令人满意的实例。有关更多详细信息，请参见此答案：How to check progress for Z3 optimization problem
[如果您处于时间紧迫状态，等不及要等待，最好的选择也许就是迭代自己：不使用优化引擎，只需执行常规查询，评估成本函数并再次调用求解器，附加的约束是成本应该比以前少。尽管这显然不一定会收敛到最佳解决方案，但它使您可以控制要进行的迭代次数，并且可以在实践中充分发挥作用。请参阅有关此问题的讨论以获得更多见解：Scalability of z3