Z3時間受限優化

我已經看到Z3支持通過例如斷言軟。根據我的理解，如果給予足夠的時間，Z3會報告給定SMT公式的最佳解決方案。Z3時間受限優化

但是，如果可以在有限的時間內運行Z3並報告可找到的最佳解決方案（這並不一定意味着它是最佳解決方案），我很感興趣。

如果我在SMT公式上運行Z3並限制時間（通過參數-T），它只會報告'超時'，如果它沒有最優解決它。我讀到默認的wmax解算器使用一個簡單的過程來限定權重，並且很好奇是否可以將權重從上限而不是下限進行綁定。

問候，埃米爾

來源

2015-11-23 Emir

-T導致進程終止，因此不會返回任何中間值的超時選項。如果使用-t選項（軟超時），那麼進程不會終止。相反，Z3會在檢查取消的某個點停止搜索。然後它產生迄今爲止最好的答案。它對應於設置取消狀態。我希望這會對你有用。

來源

2015-11-23 10:00:19

謝謝你的迴應。 -t選項似乎比指定的時間長。我指定-t：60，意思是60毫秒，但它在我手動終止它之前運行了五分鐘。但即使手動終止，它也能打印解決方案，這非常棒！ – Emir

另外一個小問題：[here]（http://rise4fun.com/z3opt/tutorialcontent/guide）我讀過，可以指定不同的優化引擎。但是，當我編寫「（set-option：opt.wmaxsat_engine hsmax）」時，我在模塊'opt'「上從Z3」未知參數'wmaxsat_engine'中收到錯誤。我使用了「opt.maxsat_engine」，但解決方案似乎無視所有限制。當前是否實施了其他引擎？我上傳了文件[here]（http://www.speedyshare.com/5RTHc/1dfb5107/smtInstance）。預先感謝您！ – Emir

如果長時間運行的步驟不檢查取消，則可以忽略軟超時。我們依靠repros來確定丟失取消檢查的位置。沒有選項wmaxsat_engine。您正在考慮的選項是maxsat_engine。有兩個主要引擎：wmax和maxres。其他（已實施）的引擎雖然應該可以訪問，但性能較差。 –

Z3時間受限優化

回答

相關問題