【发布时间】：2019-11-13 15:30:32
【问题描述】：
我正在使用 MaxSMT 来寻找一组软约束和硬约束的解决方案。对于 600 秒的超时，我从求解器获得的模型输出对于所有参数都是 Nonetype。我期待求解器为我提供次优解决方案。我是否错误地假设了这一点。有人可以解释一下吗？
编辑：所以我添加了详细选项以打印出中间步骤：我收到以下消息：
(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)
求解器似乎无法找到可行的解决方案。这是否意味着没有一个软约束是可满足的？
【问题讨论】：
-
所有的约束都是算术约束。
-
求解器是否打印
SAT？(get-objectives)在(check-sat)之后的输出是什么？可以分享一下 SMT 模型吗？ -
求解器打印“未知”。
-
在超时时间内找到部分解决方案了吗？ （使用选项
-v）。否则，您可能需要增加超时时间。 -
我不希望
z3打印任何模型，甚至没有部分解决方案。