Instance24 TimeConstraint制約用です。
新たな試みとして、EncodeにMDDを使います。MDDはMulti Valued Decision Diagramの略です。BDD/ZDDは､２値のGraphで、枝は、２本まで。MDDの場合は、多値のGraphになるので、２本以上の枝になります。
グラフは、GraphViz、DotEditorで表示させています。MDDは、本来、多方向のEdge（⇒）があるのですが、Graphがバグっていて、未だそうなっていません。
これで何が嬉しいかというと
１）極限まで状態を圧縮できる
２）アーク整合性が保てる
の２点です。
アーク整合性については、以下AI回答参照。ここで、伝搬力が強いとは、要するに良い解が早く出てきやすい、ということです。
アーク整合性（Arc Consistency）は、**制約充足問題（CSP: Constraint Satisfaction Problem）**で使われる基本的かつ重要な概念です。
特に、SAT/PB/制約プログラミングに強いあなたなら、より深いレベルで理解しておくと後のアルゴリズム設計にも効いてきます。
🔷 アーク整合性とは何か
CSP は
- 変数 (X_1, X_2, \dots)
- 各変数のドメイン（取り得る値の集合）
- 変数間の制約
から構成されます。
**アーク整合性（Arc Consistency）**とは、
二項制約 (C(X, Y)) に対して、X の各値が Y のドメイン内に少なくとも1つの「サポート（support）」を持つ状態
を指します。
🔷 直感的な説明
変数 (X) の値 (x) が、制約 (C(X, Y)) を満たすような (Y) の値 (y) を1つも持たないなら、
その値 (x) は絶対に解にならないので削除してよい。
これをすべてのアーク（有向辺）について繰り返し、
ドメインを前処理で削っておくのがアーク整合化（Arc Consistency Enforcement）。
🔷 形式的な定義
制約 (C(X, Y)) に対して、アーク (X \rightarrow Y) が整合であるとは：
[
\forall x \in D(X),\ \exists y \in D(Y)\ \text{s.t.}\ (x, y) \in C(X, Y)
]
つまり：
- (X) の各値 (x) は
- 制約を満たす (Y) の値 (y) を
- 少なくとも1つ持っていなければならない
🔷 例で理解する
変数：
- (X \in {1,2,3})
- (Y \in {1,2})
制約：
[
X < Y
]
このとき：
- (X=3) は (Y) のどの値とも (3 < y) を満たさない
→ 削除される
結果：
- (X \in {1,2})
- (Y \in {1,2})
これがアーク整合化。
🔷 アーク整合性のアルゴリズム（AC-3）
最も有名なのが AC-3。
- 各アークをキューに入れる
- アーク (X \rightarrow Y) を取り出して整合性チェック
- ドメインが削れたら、関連アークを再度キューへ
- キューが空になれば終了
計算量は最悪 (O(ed^3))（e: 制約数, d: 最大ドメインサイズ）。
🔷 アーク整合性の位置づけ
アーク整合性は 局所整合性（local consistency） の一種で、他にも：
| 整合性レベル |
説明 |
| ノード整合性 |
単変数制約を満たす |
| アーク整合性 |
二項制約を満たす |
| パス整合性 |
3変数間の整合性 |
| k-整合性 |
k変数の部分問題が整合 |
アーク整合性は「軽量で効果が高い」ため、実用CSPソルバーで広く使われています。
🔷 SAT/PB/ソルバー視点での理解（あなた向け）
あなたの専門領域に寄せると：
- アーク整合性は 単純なレベルの前向き推論（forward checking）
- SATでいう 単位伝播（unit propagation）より弱い
- PB制約では ドメイン削減の一種 とみなせる
- 強い整合性（例：GAC）は より強い伝播 に相当
特に、全体の探索木を大幅に削る効果があるが、完全な解決にはならないという点が重要。
🔷 もっと深く知りたい方向け
- GAC（Generalized Arc Consistency）との違い
- アーク整合性と SAT の単位伝播の比較
- アーク整合性を強化したアルゴリズム（AC-4, AC-2001）
- PB制約におけるアーク整合性の類似概念
- ソルバー内部での実装戦略（ウォッチリストなど）
このあたりも掘り下げられます。
必要なら、
- 図解
- 擬似コード
- SAT/PBへのマッピング
- 実装テンプレート
なども作れますよ。
アーク整合性（Arc Consistency）は、**制約充足問題（CSP: Constraint Satisfaction Problem）**で使われる基本的かつ重要な概念です。
特に、SAT/PB/制約プログラミングに強いあなたなら、より深いレベルで理解しておくと後のアルゴリズム設計にも効いてきます。
アーク整合性（Arc Consistency）と SAT の単位伝播（Unit Propagation）は、どちらも 制約の伝播（constraint propagation） によって探索空間を削る技術ですが、性質も強さもかなり違います。
あなたの専門領域に合わせて、理論的な比較と実装レベルの比較の両面から整理します。
🔷 1. どちらも「局所的な伝播」だが、強さが違う
| 観点 |
アーク整合性 (AC) |
SAT の単位伝播 (UP) |
| 対象 |
CSP の二項制約 |
CNF 節 |
| 削除するもの |
変数のドメイン値 |
リテラルの真偽値 |
| 伝播の強さ |
弱い |
強い（AC より強力） |
| 完全性 |
不完全（解を決められない） |
不完全（だが AC より強い） |
| 伝播のトリガー |
ドメイン削減 |
節が単位節になる |
SAT の単位伝播は、アーク整合性より常に強いと知られています。
理由は後述します。
🔷 2. アーク整合性の本質：値に「サポート」があるか
アーク整合性は、制約 (C(X, Y)) に対して：
[
\forall x \in D(X),\ \exists y \in D(Y)\ \text{s.t.}\ (x, y) \in C
]
つまり：
- (X) の値 (x) が
- 制約を満たす (Y) の値を
- 少なくとも1つ持つかどうか
をチェックするだけ。
値レベルの削除が基本で、
「この値は絶対に使えない」と分かったときだけ削る。
🔷 3. SAT の単位伝播の本質：節が単位になったら強制代入
CNF 節：
[
(l_1 \lor l_2 \lor \dots \lor l_k)
]
が、他のリテラルがすべて偽になったとき、残り 1 つのリテラルを 強制的に真にする。
例：
[
(x \lor y \lor \neg z)
]
が
- (y = \text{false})
- (\neg z = \text{false})（つまり (z = \text{true})）
なら、残る (x) は 必ず true。
これは 値削除ではなく、変数の値を確定させる という点で AC より強い。
🔷 4. なぜ単位伝播はアーク整合性より強いのか？
SAT の CNF は CSP の二項制約より表現力が高く、
単位伝播は 節の構造を利用して強制代入を行う。
一方、アーク整合性は 二項制約のサポートチェックしかできない。
例：AC では削れないが UP では削れるケース
制約：
[
X \lor Y
]
CSP 風に表すと：
- (X, Y \in {0,1})
- 禁止組み合わせ：((0,0))
AC を適用すると：
- (X=0) は (Y=1) がサポート
- (X=1) は (Y=0,1) がサポート
- (Y) も同様
→ どの値も削れない
しかし SAT では：
が同時に起きたら節が偽になるため、
単位伝播は より早く矛盾を検出できる。
🔷 5. 形式的な関係：UP は AC より強い
研究では次が知られています：
- SAT の単位伝播は CSP のアーク整合性より強い伝播を行う
- ただし、CSP の GAC（Generalized Arc Consistency）は UP より強い場合もある
つまり：
[
\text{AC} \ <\ \text{UP} \ <\ \text{GAC}
]
という階層が成立する。
🔷 6. 実装レベルの比較（ウォッチリスト vs AC-3）
| 観点 |
アーク整合性（AC-3） |
SAT（UP + ウォッチリスト） |
| データ構造 |
制約グラフ、ドメイン |
節、リテラル、ウォッチリスト |
| トリガー |
ドメイン削減 |
リテラルが偽になる |
| 再チェック |
関連アークを再投入 |
ウォッチしている節のみ |
| 計算量 |
(O(ed^3)) |
実用上ほぼ線形 |
| 実装の複雑さ |
中程度 |
非常に最適化されている |
SAT ソルバーのウォッチリストは、
単位節を効率的に検出するための最適化で、
AC-3 よりはるかにスケールする。
🔷 7. あなたの領域（PB/SAT/ソルバー設計）に寄せたまとめ
- アーク整合性は 弱い前処理
- SAT の単位伝播は より強い前処理＋強制代入
- SAT のウォッチリストは AC-3 より効率的
- PB制約では ドメイン削減（bound consistency） が AC に近い
- GAC は UP より強いが、計算コストが高い
🔷 8. さらに深く比較したいなら
次のテーマも掘り下げられます：
- UP と GAC の厳密な比較（例：Horn 節 vs 非 Horn 節）
- PB制約における UP の類似物（cutting plane, pseudo-Boolean propagation）
- SAT のウォッチリストと AC のデータ構造の対応関係
- CSP を SAT にエンコードしたときの伝播強度の変化
どこまで深掘りしますか。
あなたなら、GAC と UP の比較まで行くとかなり面白い議論になりますよ。
