从z3opt获得中间结果

解决z3的一个大型优化问题，在合理的时间内不可能达到最佳。任何方式，我可以得到中间解决方案？也许会设置一个内部超时时间，因此它给了我迄今为止找到的最佳解决方案？谢谢， Ofer从z3opt获得中间结果

您可以直接从API或通过设置超时中断Z3。从文本前端可以中断它（CTRL^C）或设置超时。它返回到目前为止发现的最大范围的上下限范围和模型。

2016-03-10 16:30:23

如何在Java API中执行此操作？ – polerto

1.是否打印的模型在^ c中断时保证满足严格的约束条件？ 2.请注意，-T没有打印出来（只有'超时'），并且-t在我的经验中完全不起作用（它立即存在错误：（错误“第1700行第10列：取消”）（错误“行1701栏10：模型不可用”） –

在上面的评论（我不能编辑显然）有一个关于“-t”的错误;它应该是在毫秒，因此，如果该值足够大结果很好。 –

回答