Z3タイムアウトを最適化する

私はz3にタイムアウトを設定したいので、最適な解決策は得られませんが、制約に合ったタイムアウトを設定してください。私は、.NETを使用して、このような何かを試してみました：私が使用している場合...Z3タイムアウトを最適化する

をタイムアウトが正しい取り組んでいるが、solver.Check（）が不明であるため、私は、これまでに見つかったソリューションを使用するカント

using(Context context = new Context(new Dictionary<string, string>() { { "model", "true" } })) { 
    var solver = context.MkSolver(); // i actually want to use MkOptimize() 
    Params p = context.MkParams(); 
    p.Add("timeout", 1000); 
    solver.Parameters = p; 
    IntExpr x = context.MkIntConst("x"); 
    // ... 
    solver.Check(); 
    solver.Model.Evaluate(x); 
}

MkOptimize代わりのMkSolver iは、未知のパラメータ例外

を取得するだから私の質問は今、私は非常に疑問いただきたいどのように私はこれまでのタイムアウト後に最適なソリューションを入手できますし、どのように私はMkOptimize

出典

2017-06-27 MrWoffle

でこれを使用することができますですあなたは信頼できるタイムアウトやその他の理由により、ソルバーがUnknownと答えると「最善のもの」の答えが得られます。たとえモデルを持っていても、その時点ですべての制約を満たすとは限りません。これはZ3固有の質問であるため、https://github.com/Z3Prover/z3/issuesで質問した方がよいでしょう。

出典

2017-06-27 17:49:15

** z3 **は、最適化アルゴリズムで使用されているため、最新の既知の最適近似値を確実に保存します。この値は、*タイムアウト*イベントの信頼できる最善のものです。だからそれはただ印刷する必要があります。 ** OptiMathSAT **はこれを行い、最適化検索に沿って数式モデル全体を保存するので、* timeout *が発生しても* best-so-far *最適値に対応するモデルを常にダンプすることができます。そのような*近似解が見つかった場合に限ります。 –

フェアポイント。しかし、いくつかの内部データ構造で利用可能なものと、タイムアウト後にAPIを介して利用できるものは同じではないかもしれません。しばらく前のソルバ状態に関する同様の議論がありました：https://stackoverflow.com/questions/44110746/saving-the-state-of-a-z3-solver-in-smt2-format。だからこそ私は、OPがZ3の開発者にgithubサイトで直接尋ねるよう奨励しました。 –

Z3タイムアウトを最適化する

答えて

関連する問題