Max-SMTはインクリメンタル・ソルーションのメリットはありますか？

Max-SMTはインクリメンタル・ソルーションのメリットはありますか？はいの場合、Z3はそれをサポートしていますか？どのように私はそれを使用することができますか？ありがとう。Max-SMTはインクリメンタル・ソルーションのメリットはありますか？

出典

2016-05-24 qsp

これは一般的なアルゴリズムに関する質問であるため、Programmers.SEでより良い回答を得ることができます。モデレーターにそれを移植するよう依頼することができます。 – msanford

@msanfordアルゴリズムの質問は両方のサイトで話題になりますが、この質問は少し不明です。移行を検討する前に改善する必要があります。 –

@Snowman良い点（特にあなたの血統を与えて）。私はしばしばこのタイプの質問がどこに属しているのか把握するのに苦労します。 – msanford

stackoverflowは増分質問を可能にしますが、Z3の最適化ルーチンは非インクリメンタルです:-) APIはプッシュ/ポップ機能を公開しますが、便宜上のものです。それが解決になると、Z3はアサートされた数式のセット全体に対して前処理を行い、次に最大化ルーチンを呼び出します。前処理がなかったとしても、有用な方法でコア（および補正セット）に基づくmax-satソルバーをインクリメンタルにすることは、おそらく興味深い質問です。

出典

2016-05-24 19:56:52

Max-SMTはインクリメンタル・ソルーションのメリットはありますか？

答えて

関連する問題