0

マルチセットを、合計が等しい 2 つのセットに分割する必要があります。たとえば、マルチセットが与えられた場合:

1 3 5 1 3 -1 2 0

2 つのセットを出力します。

1) 1 3 3
2) 5 -1 2 1 0

どちらも合計すると 7 になります。

Z3 (smt2 入力形式) と「線形演算ロジック」を使用してこれを行う必要があります。これは次のように定義されています。

formula : formula /\ formula | (formula) | atom
   atom : sum op sum
     op : = | <= | <
    sum : term | sum + term
   term : identifier | constant | constant identifier

正直なところ、これをどこから始めればよいかわかりません。アドバイスをいただければ幸いです。

よろしく。

4

2 に答える 2

1

ここにアイデアがあります：

c_i1-各要素に対して0 ～ 1 の整数変数を作成します。要素c_iが最初のセットにある場合はゼロであり、2 番目のセットにある場合は 1 です。あなたはそれを言うことによってそれを達成することができ0 <= c_iますc_i <= 1.

2- 最初のセットの要素の合計は、次のように記述できます。1*(1 - c_1) + 3*(1 - c_2) + ... +

3- 2 番目のセットの要素の合計は、次のように記述できます。1*c1 + 3*c2 + ...

于 2012-01-29T04:24:15.210 に答える
1

SMT-Lib2 は非常に表現力豊かですが、プログラミングするのが最も簡単な言語ではありません。SMTLib2 で直接コーディングする必要があるという厳しい要件がない限り、SMT ソルバーへのより高いレベルのバインディングを持つ他の言語を検討することをお勧めします。たとえば、Haskell と Scala の両方に、はるかに高いレベルで SMT ソルバーをスクリプト化できるライブラリがあります。たとえば、Haskell を使用して問題を解決する方法は次のとおりです: https://gist.github.com/1701881。

これらのライブラリを使用すると、はるかに高いレベルでコーディングできるようになり、必要な変換と SMT ソルバーのクエリを舞台裏で実行できるようになります。(実際に問題の SMTLib エンコーディングを取得する必要がある場合は、これらのライブラリも使用できます。これらのライブラリには通常、ソルバーにクエリを実行する前に、生成した SMTLib をダンプするために必要な API が付属しているためです。)

これらのライブラリは、Z3 が SMTLib を介してアクセスできるすべてのものを提供するわけではありませんが、関心のあるほとんどの実用的な問題に対してはるかに簡単に使用できます。

于 2012-01-30T01:56:39.233 に答える