z3最小化和超時

我嘗試使用z3求解器來解決最小化問題。我試圖超時，並返回迄今爲止最好的解決方案。我使用python API，並使用超時選項「smt.timeout」與z3最小化和超時

set_option("smt.timeout", 1000) # 1s timeout

實際上在大約1秒後超時。然而，較大的超時不能提供較小的目標。我結束了在開啓冗長與

set_option("verbose", 2)

而且我認爲，Z3先後評估大我的目標的值，直到問題得到滿足的：

(opt.maxres [0:6117664]) 
(opt.maxres [175560:6117664]) 
(opt.maxres [236460:6117664]) 
(opt.maxres [297360:6117664]) 
... 
(opt.maxres [940415:6117664]) 
(opt.maxres [945805:6117664]) 
...

我這樣有兩個問題：

我可以相反地告訴z3從上限開始，並連續返回具有較小值的模型用於我的目標函數（就像例如Minizinc註釋indomain_maxhttp://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html）
它仍然看起來像求解器返回我的問題的可滿足的實例。它是如何發現的？如果它試圖先後評估大我的目標的值，它不應該發生超時時發現還沒有令人滿意的情況下...

編輯：在opt.maxres日誌，上界永遠不會收縮。

爲了記錄在案，我發現的選項更詳細的描述在這兒爲源極opt_params.pyg

編輯對不起，打擾，我已經木珠潛入這家最近的一次。無論如何，我認爲這可能對其他人有用。我發現我實際上必須調用Optimize.upper方法來獲得上限，並且該模型仍然不是與此上限相對應的方法。我已經能夠將它添加爲一個新的約束，並稱爲解算器（沒有優化，只是SAT），但這可能不是最好的主意。通過閱讀this我覺得我應該在解算器超時後調用Optimize.update_upper，但python接口沒有這樣的方法（？）。至少我現在可以得到上限和相應的模型（以不必要的計算爲代價）。

來源

2016-02-04 Emilien

下面是使用C++ API的相同問題：[Z3：用於C++優化的超時]（https://stackoverflow.com/questions/38674049/z3-timeout-for-optimize-in-c/38680055） –

Z3找到硬約束的解決方案並記錄目標和軟約束的當前值。如果您要求模型，則返回最後找到的模型（最後一個具有目標最佳值的模型）。 maxres策略主要改進軟約束的下界（例如，任何解決方案必須至少有xx的成本），並在可能時改進上界（可選解決方案的成本至多爲yy）。除了縮小可能的最佳值的範圍之外，下限不會告訴你太多。當您超時時，上限可用。您可以嘗試其他策略之一，例如名爲「wmax」的策略，其中執行分支和剪枝。通常情況下，maxres的效果會更好，但是用wmax改善上限可能會有更好的體驗（取決於問題）。

我沒有一個模式，你得到一個模型流。原則上可行，但需要一些（非平凡的）重組。對於帕累託前沿，您可以連續調用Optimize.check（）來獲得連續的前沿。

來源

2016-02-04 18:03:57

感謝你的答案，我不能編輯，但你可能意味着最佳，而不是可選。我不知道如何使用wmax策略而不是maxres策略。我嘗試了'set_option（「opt.maxres.wmax」，True）'但我沒有看到任何重大更改（opt.maxres日誌相同）。 – Emilien

所以我設法改變模型，然後使用'optsmt'，而根據日誌找到更好的上界。但是，當它超時時，返回的模型不是具有目前最佳值的那個（目標值與我可以使用'objective.upper'訪問的目標值不同）。你知道我怎麼能得到相應的模型？ – Emilien

z3最小化和超時

回答

相關問題