問題タブ [minizinc]

すべてのソリューションを見つけて (gecode を使用)、統計を出力したい minizinc モデルがあります。これは簡単です。

しかし、このモデルは何千もの解を生成し、解ごとに区切り記号が出力されます。

これらの区切り記号を削除し、統計のみを出力する必要があります。方法はありますか？

==アップデート==

Gecodeソースを変更することでこれを解決できました

外したところ

もっと良い解決策があるかもしれませんが、これは私にとってはうまくいきました。

この動作中の MiniZinc コードを最適化するのを手伝ってください:

タスク: 6 つのタイムスロットがある会議があります。会議には 3 人の講演者が参加しており、それぞれ特定のスロットに参加できます。各スピーカーは、所定の数のスロットに参加します。

目的:スピーカーの終了が最も早いスケジュールを作成します。

例:スピーカー A、B & C. 通話時間 = [1, 2, 1]

スピーカーの可用性:

作業中の MiniZinc コードへのリンク: http://pastebin.com/raw.php?i=jUTaEDv0

私が最適化したいもの：

予想される解決策:

モデルを最適化しようとしています (解決にかかる時間に関して)。モデルは正しい答えを返しますが、MiniZinc は解を見つけるのに時間がかかりすぎます。私の問題は、初めてモデルを解こうとすると、minizinc に時間がかかることです。しかし、モデルをもう一度解くと、minizinc はほぼ瞬時に解を見つけます。そのため、モデルに導入した変更が解決を加速できたかどうかはわかりません。彼が以前に見つけた解決策を「忘れる」ように Minizinc に指示する方法はありますか?

ありがとうございました。

タスクのリストがあり、それらの間には相互依存性があります。9つのタスク。各 cpu グループから 6 cpu 2。3 つのグループ p1、p2、p3 があります。

異なる CPU での異なるタスクの実行時間が与えられます。タスク間でデータ データを転送する必要があります。ポイントツーポイントリンクを使用します。2 つの CPU 間のポイント ツー ポイント リンクを購入する必要があり、コストは 1 です。これらのリンクは後で再利用できます。

問題: これらの制約を指定したい。 r1!=r4 <=> b14=1; b14は、タスク 1 と 4 の間の通信の通信時間です。リンクのコストも必要です。r1: cpu タスク 1 が割り当てられています。

Minizinc でこれら 2 つの制約を指定する方法を教えてもらえますか? if then 制約を使用したくありません。

一連のブール方程式を解くために、次の入力を使用してConstraint-Programming Solver MiniZincを試しています。

MiniZincは小さなパラメータの解決策を見つけます(rows=cols=2, products=7)が、わずかに増加したパラメータでは解決しません。生成されたFlatZincモデルをCryptominisat、Lingeling 、またはClaspなどのSAT ソルバーにフィードしたいと考えています。これらのツールが既存の MiniZinc バックエンドよりも優れていることを願っています。

私の質問:純粋な Boolean FlatZincモデルをCNF (DIMACS)
に変換するツールはありますか? MiniZinc バックエンドの一部がサポートしていないように見える ため、述語を置き換えるにはどうすればよいですか?
xorall()

minizinc で pow 制約をサポートできる方法 (直接的または間接的) はありますか? Gecode は float および int 変数を使用したpow 制約をサポートしていますが、Minizinc および FlatZinc は変数の pow をサポートしていません。Minizinc と Flatzinc は、モデルへのパラメーターに対してのみ pow をサポートします。これを行うために、MiniZinc のサポートを Flatzinc (mzn2fzn) パーサーに追加する場所に関するポインタ。

- " pow( 4, x ) == y " 、つまり 4^x == y などの制約が必要です。