從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」的錯誤;它應該是在毫秒，因此，如果該值足夠大結果很好。 –

回答