問題タブ [constraint-programming]

こんにちは私は問題の同じ入力で異なる解決策が必要なので、非決定論的制約充足問題ツールが必要です。誰かがこの特徴を持つツールについて知っていますか？

私は、Gecode（c ++）、Choco（Java）、Curry（Haskell）のような、決定論的な方法で機能すると思うツールしか知りません。

誰かがこのエラーで私を助けてくださいありがとう、私はJaCoPライブラリを使用しています、それは輸送問題です、そして私はそれが制約プログラミングであるOptimalSearchを見つける必要があります

http://pastebin.com/ZV4j234Sサンプルクラス

http://pastebin.com/at7nfAwEトランスポートクラス

図に示すようなメッシュ ネットワークがあります。現在、この sat ネットワークのすべてのエッジに値を割り当てています。プログラムで、割り当てに閉じたループがないことを提案したいと思います。たとえば、左上の四角形の制約は次のように記述できます -

E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0であるため、ループを形成しないようにするには、どちらかのリンクを非アクティブにする必要があります。ただし、この種のネットワークでは、多くのループが発生する可能性があります。

たとえば、エッジによって形成されるループ - E0, E3, E7, E11, E15, E12, E5, E1。

ここでの問題は、このネットワークで発生する可能性のあるループの可能な組み合わせをそれぞれ説明する必要があることです。1つの可能な式で制約を書き込もうとしましたが、うまくいきませんでした。

この状況をエンコードする方法があれば、誰でもポインタを投げることができますか? 参考までに、私は Z3 Sat Solver を使用しています。

私のコンピューター サイエンス研究のコースでは、頻繁にアイテムセット マイニングを行うためのタイルを見つけるために、一連の制約とスコア定義を考え出す必要があります。データを含む行列は、1 と 0 で構成されます。

私の仕事は、タイリング (一定量のタイルを持つ) の一連の制約と、最大化する必要があるスコア関数を考え出すことです。タイルを重ねることができる解決策を考え始めたので、すべてのタイルの合計「面積」を計算するためのスコア関数を見つけようとしました。スコア関数は考えられるすべてのソリューションに対して評価する必要があることに注意してください。そのため、合計マトリックス (約 10 万個の要素を含む) を単純に調べて、それがタイルの一部であるかどうかを確認することはできません。ただし、2 つのタイル間のオーバーラップのみを考慮して、次のように考えました。

TotalArea = Sum_a_in_Tiles(Area(a)) - Sum_a/b_in_tiles(Overlap(a,b))

愚かなことに、3 つのタイルが重なり合う可能性を考慮していませんでした。私の質問は次のとおりです。タイルごとの面積と2つ（またはそれ以上）のタイル間のオーバーラップごとの面積のみを考慮して、n個のタイルの一般的なスコア関数を考え出すことは可能ですか？

いくつかのコードを提供することはできますが、その場合も、Comet と呼ばれるあいまいな言語でプログラムする必要があります :(

制約充足問題で割り当てられた変数の数を最大化する割り当てを見つけるための既知のアルゴリズム (またはアルゴリズムを見つけるためのリソース) は何ですか (満足のいく割り当てが存在しない場合)?

なぜ？

問題が発生するユースケースのコンテキスト

三角形のランダムなアイテムを 3 つ定義します。Microsoft Z3 は次のように出力する必要があります。

• 制約が満たされているか、または無効な入力値がありますか?
• すべての変数が具体的な値に割り当てられている他のすべての三角形アイテムのモデル。

項目を制約するために、assert等式を三角形にする必要があります。ピタゴラスの定理 ( (h_c² + p² = b²) ^ (h_c² + q² = a²)) から始めたかったのです。

問題

Microsoft Z3 には、非線形の算術問題を解決するための限られた機能しかないことを知っています。しかし、一部の手計算機でさえ、次のような非常に単純化されたバージョンを解決できます。

質問

• 2 つの値が指定されている場合、Microsoft Z3 でピタゴラスの定理を解く方法はありますか?
• または: 非線形算術のこれらのケースを処理できる別の定理証明者はいますか?

ご協力ありがとうございます - 何か不明な点があれば、コメントしてください。

Javaまたは.NETのいずれかで制約充足（CSP）問題をモデル化する必要があります。この問題では、変数の階層を表す必要があります。したがって、ツリーのすべてのノードは変数です。

たとえば、変数C1が別の変数C2の子であり、C1がtrueの場合、C2はその親であるため、C2はtrueである必要があります。同時に、ブランチ内の変数ノードがtrueの場合、階層内で選択できるブランチは1つだけであるため、他のブランチ内のすべての変数がfalseであることを意味します。

CSPの問題としてどのように表現できますか？また、Javaまたは.NETでどのツールを使用できますか？

これ以上のものがあるので、詳細を提供するために編集する必要があります。

私の問題には2つの部分があります。最初の部分には、最大化関数q1 * x1 + q2 * x2 + q3 * x3 ..があります。ここで、qiは係数（実数）、xiは変数（0にすることができます）です。または1）そして私はこの関数を最大化するxiのいくつかを選択する必要があります。つまり、ノードは0または1のみであり、階層からノードを選択してこの機能を最大化する必要があります。

繰り返しますが、これらのxi変数はツリーのノードであるため、いくつかのxiを選択する場合、それらはツリーの同じブランチからのものである必要があり、一度に1つのブランチのみを選択できます。したがって、これらの階層的制約を表す必要があります（第2部）。すべてをlp問題として表現するのが最善かもしれませんが、線形計画法の制約を使用してツリーを表現する方法がわかりません。

同時に、最大化問題（前半）を使用してCSP制約を課すことができるかどうか（LP制約を使用しないかどうか）はわかりません。

次のZ3制約をZ3py（Python API）に変換するにはどうすればよいですか。

次の作業例では、一致したモデルを取得しようとしています。この場合、2つの満足のいくモデルがあります。

と

問題は、実行中のソルバーがタイムアウトするまで、一致したモデルを繰り返すことです。満足のいくモデルを繰り返さずに取得するにはどうすればよいですか。

どうもありがとう、

z3をPythonで動作させるのに問題があります。私はWindows764ビットを実行しています。64ビットのPython3.3.0と64ビットのz34.3.0をダウンロードしました。PATHとPYTHONPATHを更新して、z3\binディレクトリを含めました。ただし、Pythonでz3を使用しようとすると、次のエラーが発生します。

from z3 import *トレースバック（最後の最後の呼び出し）：ファイル ""、1行目、ImportError：'z3'の不正なマジックナンバー：b'\ x03 \ xf3 \ r \ n'

何がうまくいかず、それを修正する方法を誰かが知っていますか？

ありがとう