Day毎の累積最小・最大の確定

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

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

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

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

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

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

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一択です。

新しい整数化フェーズ方法

 LpsolverでLBを求めたあと、Branchとヒューリスティックを用いて整数化を行うのが常道です。しかしながら、Instance24は、超巨大インスタンスであり、常道のBranchを行って整数化を行っていたのでは、途方もない時間がかかってしまいます。そこで、新しい整数化方法を考えました。

上が、その系で、BranchしないIteration Loopになっています。TargetUB＝ceil(LB)を選び、

LP SolverとSAT Solverとの間で通信をしながら、徐々にBITを固定化していきます。めでたくSAT解が得られれば、そこで終了です。UNSATもしくは、LpSolverのLBが、TargetUBを超えたら、TargetUBはUNSATという証明が得られたということです。TargetUB+=1にしてIteration Loopをやり直します。この系においてはBranchingしないことが特徴です。Branchingするということは、その裏も厳密性のためには結局は見ないといけないです。ヒューリスティックにBranchしていたのでは、UNSATの厳密性が得られません。あくまで、厳密解にこだわったループになっています。

この方式は、MAXSATでは一般的なUNSAT 解法を模していますが、Lp Solverを含めたところが新しいです。多くの場合SATSolverがUNSATを返すよりも、LPSolverがExcessiveLBを検出する方が早いだろう、と予測しています。

一般的にSATSolverで、OR問題を解いたとき、UNSATを返すのは、UNSATLOOP初期段階もしくは、軽い系に限られることが多いです。真のBoundary付近では、SAT/UNSATの判別がつかない、という場面を多く経験しました。それに対してLP　SolverとSAT　Solverが互いに助けながら学習を進めていくこの方式は、互いの強みを生かしながら同時に弱点を補完しあいます。LPとSAT,アナログとデジタルのHybridループになっています。SATSOLVERは、UNSATを証明するための濃厚かつ重厚緻密計算を行う必要はないだろう、と見ています。

実は、Instance15を解いたときに、多くのBranchingLOOPを廻しました。計算機を一週間近く廻さないと、そのLBでは解がない、UNSAT証明が出来ませんでした。こうした場面でも上記アプローチは、有効ではないかと期待されます。

この方式では、目的関数値がLB近傍にあるときBranchingよりも高速に整数化できると期待されます。また上手くいったら、市井のNSPに対しても本方式を採用したいと思っています。