問題タブ [constraint-satisfaction]

私はJava 6のソース間トランスフォーマーに取り組んでいます^*1)。

肯定的な情報だけでなく、否定的な情報も保持する必要があるため、トランスに小さな制約システムを実装する必要があります。制約システムは、次のように定義できる制限された種類の CNF 式です。

(v1 == c1 /\ v2 == c2 ... vn == cn) /\ ((w1,1 != d1,1 \/ w1,2 !== d1,2 ... w1,k != d1,k) /\ (w2,1 != d2,1 \/ ...) /\ ... (wm,1 != dm,1 \/ ... \/ wm,k != dm,k))

等式制約(代入、変数割り当て) はvi == ciどこにありますか?

wj != dj,lは不等式制約であり、

vi, wj,l変数、_

ci, dj,l定数(リテラル) です。

定数型は、整数にマップされた Java プリミティブ型および参照型です。定数は、任意の AST に似た構造でもあります (部分的に評価された式を表し、(メタ) 変数を含む可能性があります)。

制約システムは次のように機能します。

トランスフォーマーが条件 (例: if(x == c) then b else b1)に達すると、制約がthen分岐の制約システムx == cに追加され、次に制約がelse分岐の制約システム(式) に追加されます。x != c

したがって、then分岐の新しい式は次のとおりです。x == c /\ formula(式の正の部分は等号の結合です);

else分岐の新しい式は次のとおりですx != c \/ formula(式の負の部分は、不等式の選言の結合です)。

編集：制約システムの充足可能性。

制約システムが充足可能であるためには、制約が満たされるように、システム内の変数に値を割り当てることが可能でなければなりません。

したがって、各方程式に対してThetaがThetaと構文的に同一になり、同様に、各不等式に対してThetaがThetaと構文的に異なるような代入Thetaが存在する場合、制約システムは満たされます。 v = c vcw != d wd

残念ながら、私は制約プログラミングにかなり慣れていないため、問題に遭遇しました。

1. この場合、AST定数を整数にマップする方法は完全には明らかではありません。定数の配列のインデックスまたはハッシュ関数を使用する必要がありますか?

2. ロングタイプの扱いが不明。int ベースのソルバーを書き換えて long ベースにするか、浮動小数点ソルバーを使用しますか?

3. また、整数データと浮動小数点データの組み合わせを処理する方法も明確ではありません。簡単な解決策は、整数制約と浮動小数点制約の両方に浮動小数点ソルバーを使用することです。本当ですか？または、制約の浮動小数点部分と整数部分を別々に解決できますか?

誰か助けてくれませんか？いくつかの方向性、ヒント...

¹⁾現在、source=8 / target=8スキームは受け入れられています。

今が紀元前 3000 年で、異性愛規範的で一夫多妻制のスピードデートを設定していると想像してみてください。n_c男性とn_s女性がいます（ n_s > n_c）。n_rスピードデートはラウンドで進行します。各ラウンドで、男性のそれぞれが女性と会います。したがって、n_r*n_cスロットを埋める必要があります。

また、彼らはすべて、スロットの 1 つで男性と女性u(i,j)をペアにするユーティリティを提供するスコアリング関数を構築した石板アンケートに記入しました 。ij

目標は、すべてのスロットでスコアの合計を最大化することです。男性は同じ女性に 2 回以上会うことはなく、各女性は多くても男性としか会わないという制約の下で行われ ceil(n_r*n_c/n_s) ます。（つまり、各女性はほぼ同じ数の男性と会うべきです。）

これを解決するアルゴリズムをスケッチできますか? 男性と女性の数は 100 人未満、おそらく 50 人未満であると想定できます。ああ、現代のハードウェアを紀元前 3000 年に持ち込んだとします。

CSP プランナーの視野を広げるのをいつやめるべきですか? 具体的には、制約充足問題プランナーの条件はありますか? 検索とのアークの一貫性があるホライズンで失敗すると、アークの一貫性がすべてのより長いホライズンでも失敗することを意味します。

その値 val1 >= val2 をアサートする必要があります。つまり、モデルのチェックに関して、証人 (反例) は val1 >= val2 であると断言する必要があります。

C（cbmc）で次のように簡単に実行できます。

Pythonでそれを行う方法はありますか?

アップデート：

引き起こす

でももしそうなら

結果は、私が望むものの逆です (val2 >= val1 が必要です)。 編集：

選択した z と r の値に応じて、これは中断するか通過して x 、 y を出力します。したがって、これは __CPROVER_assert のようには機能せず、有効な/満足している証人/解釈を見つけます!

たとえば、同じコードを 3 回実行した結果は次のようになりました。

Python で制約の充足可能性を確認する方法はありますか。

Arc-Consistency Algorithm の複雑さはなぜ O(cd ³ ) なのですか?

一般に、扱いにくい制約充足問題は NP 完全問題と見なされるため、NP 完全制約充足問題の Big-O の最悪のケースの実行時間はどれくらいですか?