Day毎の累積最小・最大の計算法

 SATソルバが鍵となります。

長大のインスタンスにおいて、いきなり年間[1840,1872]時間では、探索範囲が膨大過ぎます。探索範囲をなるべく限定することを考えます。

Power On時、Target Rangeに至る経路は膨大です。そのままでSAT SOLVEすると爆発して求めることができません。

そこで、まずは、LpSolverで、システム全体のLowerBoundまで求めます。LB≒UBの性質を利用してグラフをReductionします。Reductionしたグラフ上で、Day毎に[最小：最大]を算出して、上図のように探索範囲を限定してやろう、という算段です。最適化という作業は、選択と評価探索の言い換えです。OR世界では、Branch＆Boundという最強の手法が存在しますが、残念ながら、今回の規模は大きすぎてそれでも時間がかかりすぎるために、この手法に至っています。

具体的には、次のアルゴリズムで、Day毎の[最小：最大]を確定させます。

グラフ上では、レベルと呼ばれる変数があります。大まかにいえば、各レベルは各シフトに対応します。各シフトは、同一Dayでは連続します。各レベルでの最小、最大を求めてやれば、各Dayでの最小・最大に換算することは出来ます。なので、まずは、各レベルでの最小と最大を求めてやることが必要となります。それには、各レベル上の各ノードで、最小と最大値を得ることになります。それを各レベルにまとめ、さらに各Dayにまとめる、という作業になります。

動的計画法を単に用いただけでは、終端での最小・最大値しか担保されません。全ての中間ノードをScanすることで、はじめて厳密なDay毎の累計最小・最大状態を得ることが出来ます。

このように、ORにおける最適化とは、ほとんど枝刈りのための前処理と枝刈りそのものです。

Q.明け翌日が会議日であるなら日勤、それ以外は休みとなるようにしたい

 Q以下に記述してみましたが、

期待通りに動きません

Ans.

まずは、明けの後、「日勤または休み」を記述します。

シフト集合は、以下で記述します。

これで、明けの後に、「休み」または「日勤」に限定しました。

次に「明けの後の休みパターン」で会議日を禁止します。

これだけでは、明けのあと、会議日以外では、休みになるか日勤になるか特定されません。

そこで、次を追加します。

これを言葉で言うと

■「明けの後の日勤パターン」は、明けの翌日が職員会議日以外では禁止

となります。

ここで、「職員会議ではない」は、以下の最後行のように「でない」演算子を「職員会議」に適用して作成しました。

これで、題意の設定が完了しました。

ちょっと難しかったと思います。一般には、次の順序で考えると良いでしょう。

１）まず、あり得る状態を制約（1/2行目→明けの後のあり得ない状態を排除する）　

２）１）状態のなかで、さらに細かいところを詰めていく（制約していく 3/4行目、全ケースを網羅する）

結果的に全ケースを網羅している、ことに気づかれたでしょうか？　最初から全ケースを網羅しようとすると、考えること自体が面倒になってしまいますが、このように一行一行、パターン作成→解確認　で確認しながら作成するやり方もアリです。制約を言葉にしながら進むことがポイントです。

他に、

■通常パターンをソフト制約にして、

■イレギュラーを予定でハード制約する、

方が実装は簡単かとは思います。あまり美しくはないですがこれもアリです。

SAT Hard制約中に得たFixed LitsをSAT SOFT制約に投入してもよいか？

 Q.SATでHARD制約のみでSAT解を得た時のレベル０STACKをFIXEDLITSとして得る。SOFT制約を追加して、SAT SOLVEするが、前FIXEDLITSをADDしても厳密性は失われないか？

結論から言うと：

HARD 制約だけで得たレベル 0 の FIXED LITS（＝レベル 0 で強制される単位伝播の結果）を、 SOFT 制約を追加した後の SAT SOLVE にそのまま ADD しても、 厳密性（soundness）は一切失われません。

むしろ レベル 0 の FIXED LITS は「HARD 制約から論理的に必然な真理」なので、 SOFT 制約を追加しても常に保持すべき情報 です。

🎯 結論（最重要）

• レベル 0 の FIXED LITS は HARD 制約から論理的に導かれる必然の事実

• SOFT 制約は目的関数を変えるだけで、HARD 制約の論理的帰結を壊さない

• よって レベル 0 の FIXED LITS を再投入しても soundness は完全に保たれる

🔍 なぜ soundness が保たれるのか（論理的理由）

◆ 1. レベル 0 の FIXED LITS とは何か？

レベル 0 の割り当ては：

• HARD 制約だけで単位伝播した結果

• どんな SAT 解でも必ず満たさなければならない真理

• つまり HARD 制約の論理的帰結（logical consequences）

形式的には：

$$\text{HARD}\models l$$

という形で表せる。

◆ 2. SOFT 制約は「目的関数」または「優先度」を追加するだけ

SOFT 制約は：

• 満たされなくてもよい（ただしペナルティがある）

• HARD 制約の論理的帰結を壊すことはない

つまり SOFT 制約を追加しても：

$$\text{HARD}\models l$$

は変わらない。

◆ 3. よって FIXED LITS を再投入しても soundness は壊れない

なぜなら：

• FIXED LITS は HARD 制約の論理的帰結

• SOFT 制約は HARD 制約を弱めない

• したがって FIXED LITS を追加しても 本来存在する最適解を排除しない

つまり soundness が保たれる。

RC Fixingにより、目的関数値は変化するか？

Q.RC FixingによりRMPのOBJが変化することはあるか?

 Iterativeに解いていくこのアルゴリズムは、自然にOBJが上昇することを期待しています。一応、AIの意見を聞きました。

結論から言うと：

Reduced Cost Fixing（RCF）そのものは RMP の OBJ 値を変化させません。 ただし、RCF によって “変数の上限・下限が固定される” ことで、 RMP を解き直したときの LB（＝RMP の OBJ）は変化することがあります。

つまり：

• RCF = OBJ を直接いじらない（安全）

• RCF の結果として RMP の feasible set が縮む → LB が上がることはある

• LB が下がることは絶対にない（soundness の理由）

この 3 点が本質です。

◆ Reduced Cost Fixing が「OBJ を変えない」理由

RCF は次のような操作です：

• ある変数 x を 0 に固定（UB=0）

• または 1 に固定（LB=1）

これは 目的関数の係数（重み）を変更する操作ではない。

したがって：

• OBJ の式は変わらない

• 目的関数の係数も変わらない

• RMP の線形構造も変わらない

RCF は 制約（bounds）を tighten するだけ です。

◆ ではなぜ LB（RMP の OBJ）が変わることがあるのか？

理由はシンプルで：

変数を固定すると、RMP の feasible region が縮むから。

LP の性質として：

• feasible region を縮める → LB は 上がるか同じ

• feasible region を広げる → LB は 下がるか同じ

RCF は feasible region を 縮めるだけ なので、

$$L{B}_{\text{new}}\ge L{B}_{\text{old}}$$

が常に成立します。

これが soundness の根拠でもある。

◆ 重要：LB が下がることは絶対にない

RCF は「増やす方向の Fixing」しか行わないため、

• 最適解を排除しない（sound）

• LB が下がることはない（安全）

LB が下がる Fixing は 危険（unsound） であり、 あなたの方式では絶対に起きません。

◆ まとめ（最重要）

• RCF は OBJ の式を変えない → OBJ は変化しない

• ただし、変数固定により feasible region が縮む → LB が上がることはある

• LB が下がることは絶対にない（soundness）

soundnessとは？

 Q.soundness証明とは？

学会の質問で「Is it sound？」というのを見かけることがあります。

これは、「～ぽい」ではなくて、アルゴリズムが堅牢であるかどうか？を尋ねていた、ということです。提案しているアルゴリズムが、soundnessであるか？AIの見解を聞きました。

結論から言うと、soundness（健全性）証明とは「この Fixing（枝刈り）は 本来存在する最適解を絶対に消さない」ことを数学的に保証する証明のことです。 最適化アルゴリズムでは 正しさの根幹 になる概念です。

🎯 soundness（健全性）とは何か

最適化アルゴリズムにおける soundness とは：

枝刈り・Fixing・制約追加などの操作が、 真の最適整数解を絶対に排除しないこと。

これが保証されていないと、 「速いけど間違った解しか返さないアルゴリズム」になってしまう。

🔍 あなたの Reduced Cost Fixing の soundness はどう証明されるか

あなたの Fixing は次の形でした：

$$w\cdot \mathrm{\Delta }{n}_w\le GAP=TargetUB-LB$$

したがって

$$\mathrm{\Delta }{n}_w\le \lfloor \frac{GA\mathrm{P/}}{}$$w⌋

これは LB（下界）と TargetUB（上界）から導かれる “絶対に破れない論理的制約” です。

✔ soundness の証明の骨格

(1) LB ≤ OPT（整数最適値）

LP の LB は常に整数最適値 OPT の下界。

(2) TargetUB ≥ OPT で初めて SAT になる

あなたの探索は TargetUB を 1 ずつ増やす方式なので、

• TargetUB < OPT → UNSAT

• TargetUB = OPT → SAT（初めて）

これはすでに議論済み。

(3) Fixing の条件は OPT を排除しない

最適解の目的値は OPT なので、

$$\sum w\cdot \mathrm{\Delta }{n}_w=OPT-LB\le TargetUB-LB=GAP$$

よって最適解は必ず

$$w\cdot \mathrm{\Delta }{n}_w\le GAP$$

を満たす。

つまり Fixing は最適解の Δn を排除しない。

(4) よって Fixing は sound（健全）

Fixing によって削除されるのは

• 最適解よりもコストが高くなる構造

• TargetUB を超える構造

だけであり、 最適解そのものは絶対に削除されない。

これが soundness の証明。

🧠 直感的な説明

Fixing は「GAP の容量制約」を使っているだけなので、

GAP の中に収まる解（＝最適解）は絶対に残る。 GAP を超える解（＝最適ではない）は全部切ってよい。

という非常に自然な論理になっている。

📌 completeness（完全性）との違い

• soundness（健全性） → 正しい解を消さない

• completeness（完全性） → 必ず解を見つける

あなたのアルゴリズムは両方満たしている：

• soundness：Fixing が最適解を消さない

• completeness：TargetUB を増やせば必ず OPT に到達する

✅ まとめ

soundness 証明とは「Fixing が最適解を絶対に消さない」ことの数学的保証。 あなたの Reduced Cost Fixing は LB と TargetUB の差（GAP）に基づくため、 最適解は必ず GAP 内に収まる → soundness が成立する。

MDD TREEの枝刈り

Scheduling Benchmarksでは、すべて、

RMPの重みは、Understaffing=100、Overstaffing＝１

スタッフ側(Pricer)は、希望休み・シフトに対する違反重み種類が3種類(1,2,3)

と非常にシンプルです。

前提の整理

• 最小化問題とします。

• 目的関数は、重み付き個数の和：

$$z=100x_{100}+1x_1+1y_1+2y_2+3y_3$$

のような形（RMP に 100,1、Pricer に 1,2,3 の重み）。

• 線形緩和の最適値を $LB$、現在の整数実行可能解の値を $UB$ とし、

$$GAP=UB-LB$$

とする。

基本アイデア

ある重み $w$ を持つ変数（列）を、LP 解から整数解に向かうときに「どれだけ増やせるか」は、

$$w\cdot \mathrm{\Delta }{n}_w\le GAP$$

を満たさないと $UB$ を超えてしまう、という制約から来ます。 したがって、

$$\mathrm{\Delta }{n}_w\le \lfloor \frac{GAP}{w}\rfloor$$

が、その重みクラスについて許される“増分の最大数”になります。

各重みごとの限定

• 重み 100 の列:

$$\mathrm{\Delta }{n}_{100}\le \lfloor \frac{GAP}{100}\rfloor$$

• 重み 3 の列:

$$\mathrm{\Delta }{n}_3\le \lfloor \frac{GAP}{3}\rfloor$$

• 重み 2 の列:

$$\mathrm{\Delta }{n}_2\le \lfloor \frac{GAP}{2}\rfloor$$

• 重み 1 の列（RMP, Pricer 両方含めて）:

$$\mathrm{\Delta }{n}_1\le GAP$$

ここでの $\mathrm{\Delta }{n}_w$ は「LP 解から整数化の過程で、その重みクラスについて増やせる“余分な個数”」という意味です。 他の重みクラスの変数をすでにある程度固定しているなら、その分のコストを差し引いた残りの余裕に対して同じ式を適用できます。

直感的なまとめ

• GAP が小さいほど、重い列（重み 100 や 3）の「取りすぎ」はすぐに UB を超えるので、 それぞれ $\lfloor GAP\mathrm{/}w\rfloor$ 個までしか“余分には”許されない。

• これを使うと、整数化フェーズで「重み 100 の列は LP 解から多くても $\lfloor GAP\mathrm{/}100\rfloor$ 本まで」「重み 3 は $\lfloor GAP\mathrm{/}3\rfloor$ 本まで」などと、探索空間をかなり素直にカットできます。

もし「RMP 側の 100 と 1」「Pricer 側の 1,2,3」を別々に扱いたい（例えば RMP の 1 と Pricer の 1 を区別したい）なら、そのクラスごとに同じ形で上限を入れていく形になります。

この方向性で、実際に使っている目的関数の形（係数と変数の対応）をもう少し具体的に書いてくれたら、 「絶対個数の上限」まで踏み込んだ式に落とし込むこともできますが、まずはこの $\lfloor GAP\mathrm{/}w\rfloor$ ルールがコアになります。

Q.GAPが1.5のときどうなりますか？

結論だけ先に言うと、GAP = 1.5 のとき、重み 2・3・100 の列は “追加ゼロ” しか許されません。 追加できるのは重み 1 の列だけで、最大 1 本まで です。

◆ なぜそうなるか（核心）

整数化で LP 解から増やせる本数 Δn は

$$w\cdot \mathrm{\Delta }n\le GAP$$

なので

$$\mathrm{\Delta }n\le \lfloor \frac{GAP}{w}\rfloor$$

を満たす必要があります。

GAP = 1.5 を代入すると：

◆ 重みごとの上限（GAP = 1.5）

• 重み 100

$$\mathrm{\Delta }{n}_{100}\le \lfloor \frac{\mathrm{1.5/}}{100}\rfloor =0$$

• 重み 3

$$\mathrm{\Delta }{n}_3\le \lfloor \frac{\mathrm{1.5/}}{3}\rfloor =0$$

• 重み 2

$$\mathrm{\Delta }{n}_2\le \lfloor \frac{\mathrm{1.5/}}{2}\rfloor =0$$

• 重み 1（RMP・Pricer 共通）

$$\mathrm{\Delta }{n}_1\le \lfloor 1.5\rfloor =1$$

◆ つまりどうなるか

• 重い列（100, 3, 2）は一切増やせない → 追加した瞬間に UB を超えるため。

• 重み 1 の列だけが最大 1 本まで許される → GAP 1.5 の範囲で収まる唯一のクラス。

Q.重み個数n(デルタではなく）の限定式を重みWとGAPからまとめてください。

結論から先にまとめると：

重み $W$ を持つ変数の「整数解で許される最大個数 $n_w$」は、 LP 解の値 $x_w^{LP}$ と GAP を使って

$$>n_w\le \lfloor x_w^{LP}+\frac{\mathrm{G}\mathrm{A}\mathrm{P/}}{W}\rfloor >$$

で与えられる。

これが “重み W と GAP から導く、絶対個数の上限式” の完成形です。

🎯 1. なぜこの式になるのか（最重要）

整数化で変数 $x_w$ を LP 値から整数値へ動かすとき、 目的値の悪化は最低でも

$$W\cdot (n_w-x_w^{LP})$$

です。

整数解が TargetUB を超えないためには：

$$W\cdot (n_w-x_w^{LP})\le \mathrm{G}\mathrm{A}\mathrm{P}$$

これを $n_w$ について解くと：

$$n_w\le x_w^{LP}+\frac{\mathrm{G}\mathrm{A}\mathrm{P/}}{W}$$

整数変数なので：

$$\boxed{{\displaystyle n_w\le \lfloor x_w^{LP}+\frac{\mathrm{G}\mathrm{A}\mathrm{P/}}{W}\rfloor }}$$

これが 重み W の変数の絶対個数上限。

🎯 2. Δではなく「絶対個数 n_w」で書く理由

あなたが求めているのは：

• Δ（増分）ではなく

• 整数解でその変数を最大いくつまで許せるか（絶対個数）

なので、LP 値 $x_w^{LP}$ を含めた式が必要になる。

🎯 3. 例：重み 100、LP 値 0.3、GAP=1.5

$$n_{100}\le \lfloor 0.3+\frac{\mathrm{1.5/}}{100}\rfloor =\lfloor 0.315\rfloor =0$$

→ 整数解では 0 に固定（増やせない）

🎯 4. 例：重み 1、LP 値 2.4、GAP=1.5

$$n_1\le \lfloor 2.4+\frac{\mathrm{1.5/}}{1}\rfloor =\lfloor 3.9\rfloor =3$$

→ 整数解では最大 3 本まで許される

🎯 5. まとめ（あなたが欲しかった式）

重み $W$ の変数の整数解での最大個数は：

$$\boxed{{\displaystyle n_w^{\max }=\lfloor x_w^{LP}+\frac{\mathrm{G}\mathrm{A}\mathrm{P/}}{W}\rfloor }}$$

• $x_w^{LP}$：RMP の LP 解の値

• $W$：その変数の重み

• $\mathrm{G}\mathrm{A}\mathrm{P}=\mathrm{T}\mathrm{a}\mathrm{r}\mathrm{g}\mathrm{e}\mathrm{t}\mathrm{U}\mathrm{B}-LB$

UBを表すMDD Structure

 SAT Solverは、MDDを採用します。SchedulingBenchmarksにおいて、重みは、わずか4種類に限定されます。100,3,2,1です。100は、UnderStaffingです。１は、OverStaffingの重みと希望休みの重みとで共用しています。

これをMDD構造で書くと

という具体になります。大きな重み順にTreeを構成した方がノード数が少なくて済みます。最終的なTarget UB Nodeは、一つに限られます。Nodeから出るEdgeは、重み係数です。各々の重みは、UnaryCounterによって構成されています。例えば、最初の階層34700を実現するには、347の値を指しているUnaryCounterをEncodeすればよいです。

このTreeの大きさを決めるのは、各重み係数のあり得る範囲に依存します。この範囲が狭ければ狭い程、探索Treeを小さくできるので、高速にSAT/UNSAT解が求まることになります。

MDDがやっていることは、

■TargetUBになり得るすべての重み係数の組み合わせを列挙する

ということだけです。

＜Treeをなるべく小さくするには＞

■重い順から列挙

■係数範囲を絞る

当然、重み種類が多ければ多い程、また係数範囲が大きければ大きい程、Tree大きくなり、最悪の場合爆発、破綻します。そこで、あり得る範囲を限定する作業が必要になってきます。

各重み係数範囲を理論的に求めるのは、OR手法を用いて行いますが、かなり高度です。ここでは、それが求まっていることを前提に話を進めます。

＜UnaryCounterとは＞

UnaryCounterは、1進カウンタです。定番のEncodingです。SATSolverに乗せるには、必須のテクニックですが、数々の方法が提案されています。これ位の規模だとTotalizer一択です。