来自NoneType模型的z3输出

Question

我使用MaxSMT来找到一组软约束和硬约束的解决方案。当超时为600秒时，我从求解器获得的模型输出是所有参数的非类型输出。我原以为求解者会给我一个次优解。我是不是错了。谁能解释一下吗？

编辑：所以我添加了详细的选项来打印中间步骤:我得到以下消息：

(optimize:check-sat)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 2)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.restarting :propagations 417 :decisions 948 :conflicts 101 :restart 100 :restart-outer 110 :agility 0.000299947)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 3497 :decisions 11262 :conflicts 202 :restart 110 :restart-outer 110 :agility 0.00588127)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 10138 :decisions 18514 :conflicts 313 :restart 100 :restart-outer 121 :agility 0.001524)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 16862 :decisions 21147 :conflicts 426 :restart 110 :restart-outer 121 :agility 0.0337523)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 17827 :decisions 24053 :conflicts 537 :restart 121 :restart-outer 121 :agility 0.0268182)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 25141 :decisions 36272 :conflicts 660 :restart 100 :restart-outer 133 :agility 0.00362989)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 35575 :decisions 47933 :conflicts 765 :restart 110 :restart-outer 133 :agility 0.00289772)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 39641 :decisions 52637 :conflicts 876 :restart 121 :restart-outer 133 :agility 0.000965057)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
        (smt.restarting :propagations 40803 :decisions 57913 :conflicts 998 :restart 133 :restart-outer 133 :agility 0.0349118)

似乎求解者不是ale来寻找可行的解决方案。这是否意味着没有一个软约束是可以满足的？

Answer 1

没有理由期望在超时后得到一个“次优”解决方案。除非解决者得到一个明确的答案，否则你能收集到的任何内部信息就是:一些可能或不相关的内部价值。更重要的是，没有理由期望它会是一个令人满意的例子。有关更多详细信息，请参见此答案：How to check progress for Z3 optimization problem

如果您处于时间紧迫且无法等待的情况下，您最好的选择是迭代自己:不要使用优化引擎，只需执行常规查询，评估成本函数，然后再次调用求解器，附加的约束条件是，成本应该比以前的要小。虽然这显然不一定会收敛到最优的解决方案，但它可以控制您想要进行的迭代次数，并且可以在实践中充分发挥作用。请参阅对此问题的讨论，以获得进一步的见解：Scalability of z3