編集の理由により、解決する大きなブール式があります。ここに画像を貼り付ける必要があります。
areaまた、 4 つの整数の次元を測定する関数が既にあります。area(c,d,e,f)=|c−d|×|e−f|
数式が満足できるかどうかを判断するだけ(a,b,c,d,e,f)ではなく、大きな数式を作成し、数式を満たす他の 6 タプルの次元以上の最適な 6 タプルをTRUE探しarea(c,d,e,f)ています。
言い換えれMax(area(c,d,e,f))ば、大きな公式の対象を見つけてください。
SMT ソルバーがこの問題に役立つかどうか疑問に思っています。Z3が をサポートしていることを学びquantifiers、ブール式が満足できるかどうかを判断できるようになりました。しかし問題はZ3、関数の最適解を見つけるのに役立つかどうかareaです。
誰にもアイデアはありますか？SMT ソルバー、Z3、またはその他のアルゴリズムについてのコメントをお待ちしております...
要するに、はい。
数式は数量詞で構成されているため、MicrosoftSolverFoundationは適切な選択ではないと思います。あなたが言ったように、Z3は数量詞、整数の理論をサポートし、充足可能性をチェックするために使用されます。Z3は最適化を直接サポートしていませんが、全称記号を使用して最適化問題を簡単にエンコードできます。
sat（a、b、c、d、e、f）=>（forall a1、b1、c1、d1、e1、f1。sat（a1、b1、c1、d1、e1、f1）&&ゴール（a、b 、c、d、e、f）> =ゴール（a1、b1、c1、d1、e1、f1））
ここで、はsat充足可能性をチェックするためのブール式でgoalあり、はarea関数、最適化の目標です。
ご覧のとおり、定式化は質問の要件から文字通り翻訳されています。の割り当て(a, b, c, d, e, f)は、見つける必要のある最適なソリューションです。
ちなみに、Z3にはLinuxディストリビューションがあり、好みに完全に適合するOCamlAPIを提供します。
目的関数は、非線形整数演算と量指定子を使用します。すでに非線形整数演算は、量指定子なしでは困難 (決定不能) であり、量指定子を追加するとさらに悪化します。ソートを Int から Real に変更すると、非線形実数の量指定子の除去が非常に制限されます ((set-option :ELIM_QUANTIFIERS true) (set-option :ELIM_NLARITH_QUANTIFIERS true))。あなたが解決しているように見える問題。線形または二次最適化問題として定式化できるかどうかを確認してください。二次最適化に向けて調整された多くのツールがあります (Z3 のようなブール検索などはおそらくあまり調整されていません)。たとえば、いくつかの最適化ツールのプラグインを含む Solver Foundation を試してみてください。
最適化問題を解くために Z3 を使用することは可能ですが、典型的なアプローチは Z3 の外側にループを持つことです。最初に、確認したい問題が充足可能かどうかを提起し、次に、現在の問題を改善する (充足モデルから取得する) 次の充足課題を検索します。次の満足のいく割り当てを検索するには、探している次の値に割り当てられた「目標」が現在の最良の値に割り当てられた「目標」を改善することをアサートします。
関連するスライドhttp://research.microsoft.com/en-us/people/nbjorner/lecture1.pptx を次に示します。彼らはこの種の問題にかなり近づいています。この資料の最後の数枚のスライドでは、Z3 の API を使用してモデルを検索する方法を示しています。もちろん、出力形式のパーサーを書きたい場合は、テキスト API を使用することもできます。最適化問題のために Z3 と対話する方法は他にもたくさんありますが、すべて Z3 上で最適化検索をプログラムする必要があります。これは、Z3 でサポートされている算術およびその他のドメインに対する制約のブール型の組み合わせがある場合にも役立ちますが、専用の最適化ツールを使用すると、標準の最適化問題をより適切に解決できます。
このページは非常に役立つと思います。例はよく説明されており、投稿全体を読むのに役立ちます。
あなたの問題は、まさに充足可能性の1つではなく、最適化またはより具体的には混合整数プログラミングの1つです。これは、無料版も提供するMicrosoft Solver Foundationなどのソルバーを使用して解決するのはそれほど難しくありません (質問 Z3 にタグを付け、Windows を使用しているようです) 。