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に対しても本方式を採用したいと思っています。

相補性

ORの教科書では、DUALの値ｘスラック変数＝０　という説明がされています。

スケジュールナース実装では、列制約(Cover Constraints)にUnder/Over用と二つのスラックを用いています。これは、SchedulingBenchmarksでは、Underの重みが100、Overの重みが1という異なる重みになっているからです。(GUIでもそのオプションがあることが分かると思います。) つまり、一つの制約で、二つの方向をコントロールしている訳です。このようにしている理由は少しでもLpSolverの負担を減らす目的です。

で、教科書にはない、1制約について二つのスラックがあるとき、理論的にどういう挙動になるのかを解析してみます。

相補性定理により、最適解においては、RowPrice化、スラック変数のどちらかが0になるのはわかるのですが、スラック変数が二つあり、Under重み100、Overが重み1で入っていた場合はどうなりますか？数式で説明して。

問題の定式化

例えば「目標値 $b$ からのずれ」を Under/Over で表す典型的な形を

$$a^{\mathrm{\top }}x+u-o=b,u\ge 0,o\ge 0$$

とします。 目的関数側で

$$\min 100u+1o+\text{(他の項)}$$

という「Underに重み100、Overに重み1」を入れているとします。

これを標準形 LP

$$\min c^{\mathrm{\top }}z\text{s.t. }Az=b,z\ge 0$$

とみなすと、変数ベクトル $z$ の中に $u,o$ が含まれ、 その係数は

$$c_u=100,c_o=1$$

です。また制約行列 $A$ において、この行（対象の1本の制約）に対する列は

• $u$ の列：その行で係数 $+1$

• $o$ の列：その行で係数 $-1$

となります。

双対問題と RowPrice（双対変数）

この制約に対応する双対変数を $\pi$（RowPrice）とします。 標準形 $\min$ の双対は

$$\max b^{\mathrm{\top }}\pi \text{s.t. }{A}^{\mathrm{\top }}\pi \le c$$

なので、列ごとに

• $u$ に対する双対制約：

$$\pi \le 100$$

• $o$ に対する双対制約：

$$-\pi \le 1⟺\pi \ge -1$$

したがって、RowPrice $\pi$ は

$$-1\le \pi \le 100$$

という区間に縛られます。

相補性条件（補完性条件）

相補性定理（補完的スラックネス）は

$$\text{(変数)}\times \text{(対応する双対制約のスラック)}=0$$

という形になります。 ここで双対制約のスラックは

• $u$ に対して：$100-\pi \ge 0$

• $o$ に対して：$1+\pi \ge 0$

なので、相補性条件は

$$u(100-\pi )=0,o(1+\pi )=0.$$

これが「スラック変数と RowPrice のどちらかが 0 になる」という話の、2スラック版の正確な数式です。

どちらのスラックが 0 になるか

上の 2 つの式から、最適解では次のいずれかのパターンになります。

1. 両方ゼロのケース

$$u=0,o=0$$

このときは

$$100-\pi >0,1+\pi >0$$

すなわち

$$-1<\pi <100$$

となります。 → 目標値からのずれがなく、Under/Overとも使われていない状態。

2. Underだけ正のケース

$$u>0\Rightarrow 100-\pi =0\Rightarrow \pi =100,o=0\Rightarrow 1+\pi >0$$

つまり

$$\pi =100,o=0,u\ge 0.$$

→ Under側のスラックだけが正になりうる状況。

3. Overだけ正のケース

$$o>0\Rightarrow 1+\pi =0\Rightarrow \pi =-1,u=0\Rightarrow 100-\pi >0$$

つまり

$$\pi =-1,u=0,o\ge 0.$$

→ Over側のスラックだけが正になりうる状況。

4. 両方正は不可能

$$u>0,o>0$$

だとすると

$$100-\pi =0,1+\pi =0\Rightarrow \pi =100,\pi =-1$$

となり矛盾。 → 相補性により「UnderとOverが同時に正」にはなりえない。

まとめ（直感）

• 双対変数（RowPrice）$\pi$ は $-1\le \pi \le 100$ の範囲にあり、

• 相補性条件

$$u(100-\pi )=0,o(1+\pi )=0$$

により、

• $-1<\pi <100$ なら $u=o=0$

• $\pi =100$ なら $u\ge 0,o=0$

• $\pi =-1$ なら $u=0,o\ge 0$

• したがって、最適解では Under と Over のどちらか一方だけが正になるか、両方ゼロであり、両方同時に正にはならない。

重み 100 と 1 の非対称性は、「RowPrice がどちら側の端点（100 か -1）に張り付くか」を通じて、「どちらのスラックが正になりうるか」を決めている、と見るとスッキリします。

Instance13での解析

下記は、instance13でのLB=1348時の様子です。rowpriceが0でない制約のみ列挙しています。上で予測されている通り、

■rowpriceがfractionalなら、minスラック(under)、maxスラック(over)ともに、0

■rowpriceが、-1ならば、overslack>=0

■rowpriceが、100ならば、underslack>=0

ここで、注意するのは、row_priceが0でないのは、全体の2割程度(119 out of 504)ということです。つまり、残り8割の制約については、row_priceが0なので、「効いていない」という特殊状況にあることが分かります。

        　　row[14]=-0.863305 day = 0 min val=2.55555e-12 max val=5.68424e-10 row[29]=-0.586112 day = 1 min val=2.71906e-12 max val=8.88973e-11 row[41]=-0.524564 day = 2 min val=2.85273e-12 max val=8.00538e-11 row[51]=-1 day = 2 min val=2.75741e-12 max val=0.0418587 row[59]=-1 day = 3 min val=2.76917e-12 max val=0.567414 row[65]=-1 day = 3 min val=2.76857e-12 max val=0.00902082 row[68]=-0.611479 day = 3 min val=2.70788e-12 max val=1.21897e-10 row[83]=-1 day = 4 min val=2.71771e-12 max val=0.00914605 row[86]=-0.816363 day = 4 min val=2.78994e-12 max val=3.59446e-10 row[90]=52.8873 day = 5 min val=4.51134e-12 max val=2.43741e-12 row[91]=52.8873 day = 5 min val=4.4417e-12 max val=2.53334e-12 row[92]=52.8873 day = 5 min val=4.50119e-12 max val=2.43681e-12 row[93]=52.8873 day = 5 min val=4.58953e-12 max val=2.38614e-12 row[94]=100 day = 5 min val=0.0826304 max val=1.60878e-12 row[95]=52.8873 day = 5 min val=4.45319e-12 max val=2.49542e-12 row[96]=52.8873 day = 5 min val=4.54492e-12 max val=2.36447e-12 row[97]=52.8873 day = 5 min val=4.60479e-12 max val=2.29994e-12 row[98]=52.8873 day = 5 min val=4.46162e-12 max val=2.50844e-12 row[99]=100 day = 5 min val=0.0244645 max val=1.68974e-12 row[100]=100 day = 5 min val=0.0276946 max val=1.48983e-12 row[101]=100 day = 5 min val=0.0197265 max val=1.63945e-12 row[102]=100 day = 5 min val=0.0241363 max val=1.60311e-12 row[103]=100 day = 5 min val=0.0352569 max val=1.68851e-12 row[104]=100 day = 5 min val=0.0548525 max val=1.65172e-12 row[105]=100 day = 5 min val=0.02621 max val=1.5467e-12 row[106]=100 day = 5 min val=0.385148 max val=1.29568e-12 row[107]=100 day = 5 min val=0.741131 max val=1.0914e-12 row[108]=47.1127 day = 6 min val=4.3592e-12 max val=2.38182e-12 row[109]=47.1127 day = 6 min val=4.18156e-12 max val=2.64174e-12 row[110]=47.1127 day = 6 min val=4.21321e-12 max val=2.59127e-12 row[111]=47.1127 day = 6 min val=4.22595e-12 max val=2.64134e-12 row[112]=47.1127 day = 6 min val=4.18462e-12 max val=2.74338e-12 row[113]=47.1127 day = 6 min val=4.2615e-12 max val=2.52519e-12 row[114]=47.1127 day = 6 min val=4.22859e-12 max val=2.59199e-12 row[115]=47.1127 day = 6 min val=4.18693e-12 max val=2.64157e-12 row[116]=46.2326 day = 6 min val=4.03356e-12 max val=2.87082e-12 row[117]=47.1127 day = 6 min val=3.96615e-12 max val=2.96322e-12 row[134]=-0.837218 day = 7 min val=2.58397e-12 max val=2.61113e-10 row[163]=-0.925784 day = 9 min val=2.59777e-12 max val=6.6424e-10 row[180]=-0.602286 day = 10 min val=2.70604e-12 max val=1.09113e-10 row[181]=-0.625962 day = 10 min val=2.91071e-12 max val=1.10779e-10 row[210]=-0.768445 day = 11 min val=2.79359e-12 max val=1.71992e-10 row[220]=100 day = 12 min val=0.025898 max val=1.74228e-12 row[225]=100 day = 12 min val=0.0205166 max val=1.80212e-12 row[226]=100 day = 12 min val=0.0184117 max val=1.74637e-12 row[227]=100 day = 12 min val=0.0179949 max val=1.70341e-12 row[228]=98.4456 day = 12 min val=6.02561e-11 max val=1.62807e-12 row[229]=100 day = 12 min val=0.0176241 max val=1.73514e-12 row[230]=100 day = 12 min val=0.0322697 max val=1.73808e-12 row[231]=100 day = 12 min val=0.0373443 max val=1.50067e-12 row[232]=100 day = 12 min val=1.18009 max val=1.41862e-12 row[233]=100 day = 12 min val=0.0403635 max val=1.57967e-12 row[234]=100 day = 13 min val=0.222295 max val=1.49075e-12 row[235]=100 day = 13 min val=0.124916 max val=1.45064e-12 row[236]=100 day = 13 min val=0.0436695 max val=1.47376e-12 row[237]=100 day = 13 min val=0.387442 max val=1.45202e-12 row[238]=100 day = 13 min val=0.152822 max val=1.66829e-12 row[239]=100 day = 13 min val=0.032794 max val=1.53126e-12 row[240]=100 day = 13 min val=0.0482729 max val=1.56177e-12 row[241]=100 day = 13 min val=0.0203498 max val=1.61615e-12 row[242]=100 day = 13 min val=0.0594985 max val=1.66069e-12 row[243]=100 day = 13 min val=0.914335 max val=1.24705e-12 row[260]=-0.685022 day = 14 min val=2.63634e-12 max val=1.35774e-10 row[265]=-1 day = 14 min val=2.60472e-12 max val=1.01838 row[283]=-1 day = 15 min val=2.87888e-12 max val=0.0561331 row[291]=-0.669252 day = 16 min val=2.72094e-12 max val=1.43556e-10 row[301]=-1 day = 16 min val=2.86499e-12 max val=0.0183823 row[309]=-0.70548 day = 17 min val=2.6219e-12 max val=1.69257e-10 row[313]=-0.883984 day = 17 min val=2.68177e-12 max val=4.08302e-10 row[319]=-1 day = 17 min val=2.5107e-12 max val=1 row[346]=98 day = 19 min val=4.59079e-11 max val=1.62041e-12 row[351]=100 day = 19 min val=0.646963 max val=1.37153e-12 row[352]=99.2295 day = 19 min val=1.0678e-10 max val=1.58572e-12 row[353]=100 day = 19 min val=0.0163243 max val=1.5739e-12 row[354]=100 day = 19 min val=0.0378528 max val=1.65346e-12 row[355]=100 day = 19 min val=0.10811 max val=1.51971e-12 row[356]=99.5536 day = 19 min val=2.40253e-10 max val=1.50882e-12 row[357]=100 day = 19 min val=0.0521357 max val=1.39095e-12 row[358]=100 day = 19 min val=0.651391 max val=1.25515e-12 row[359]=100 day = 19 min val=2.99785 max val=7.42342e-13 row[360]=100 day = 20 min val=0.025462 max val=1.56327e-12 row[361]=100 day = 20 min val=0.0124321 max val=1.75039e-12 row[362]=100 day = 20 min val=0.0323657 max val=1.63865e-12 row[363]=100 day = 20 min val=0.0133692 max val=1.73585e-12 row[364]=100 day = 20 min val=0.0191744 max val=1.79394e-12 row[365]=100 day = 20 min val=0.0307338 max val=1.73287e-12 row[366]=100 day = 20 min val=0.0295816 max val=1.66538e-12 row[367]=100 day = 20 min val=0.0157267 max val=1.74435e-12 row[368]=100 day = 20 min val=0.0348275 max val=1.64747e-12 row[369]=98.4726 day = 20 min val=5.25977e-11 max val=1.88827e-12 row[370]=-1 day = 20 min val=2.64508e-12 max val=0.145464 row[386]=-0.609231 day = 21 min val=2.73781e-12 max val=1.14469e-10 row[410]=-0.840048 day = 22 min val=2.74723e-12 max val=2.14573e-10 row[422]=-1 day = 23 min val=2.5522e-12 max val=0.314833 row[428]=-0.726678 day = 23 min val=2.35833e-12 max val=1.73831e-10 row[440]=-0.38895 day = 24 min val=2.83071e-12 max val=6.68554e-11 row[446]=-0.424308 day = 24 min val=2.38349e-12 max val=9.0038e-11 row[449]=-0.325618 day = 24 min val=2.88308e-12 max val=7.77122e-11 row[472]=100 day = 26 min val=0.0537183 max val=1.77114e-12 row[477]=100 day = 26 min val=0.0582241 max val=1.79152e-12 row[478]=100 day = 26 min val=0.0325335 max val=1.77199e-12 row[479]=100 day = 26 min val=0.0997524 max val=1.70957e-12 row[480]=100 day = 26 min val=0.0212184 max val=1.75241e-12 row[481]=100 day = 26 min val=0.0546691 max val=1.87567e-12 row[482]=100 day = 26 min val=0.0866728 max val=1.86261e-12 row[483]=100 day = 26 min val=0.0348345 max val=1.65861e-12 row[484]=100 day = 26 min val=0.0719359 max val=1.51472e-12 row[485]=100 day = 26 min val=0.323769 max val=1.52836e-12 row[486]=100 day = 27 min val=0.122186 max val=1.63422e-12 row[487]=100 day = 27 min val=0.0589922 max val=1.4626e-12 row[488]=100 day = 27 min val=0.0313694 max val=1.7076e-12 row[489]=100 day = 27 min val=0.0413175 max val=1.74454e-12 row[490]=100 day = 27 min val=0.0632407 max val=1.79693e-12 row[491]=100 day = 27 min val=0.0315268 max val=1.72677e-12 row[492]=100 day = 27 min val=0.0477631 max val=1.69113e-12 row[493]=100 day = 27 min val=0.0162712 max val=1.76216e-12 row[494]=100 day = 27 min val=0.0320612 max val=1.68608e-12 row[495]=100 day = 27 min val=0.175491 max val=1.60306e-12 row[496]=-0.883723 day = 27 min val=2.75924e-12 max val=5.71277e-10 effective rows=119 out of 504

Branchを繰り返した結果、UB=1348の整数解時では、全RowPriceが整数となりました。

　　　　row[450]=100 day = 25 min val=0 max val=0 row[451]=100 day = 25 min val=0 max val=0 row[452]=-1 day = 25 min val=0 max val=0 row[453]=100 day = 25 min val=0 max val=0 row[454]=100 day = 25 min val=0 max val=0 row[455]=100 day = 25 min val=0 max val=0 row[456]=100 day = 25 min val=0 max val=0 row[457]=100 day = 25 min val=0 max val=0 row[458]=100 day = 25 min val=0 max val=0 row[459]=-1 day = 25 min val=0 max val=0 row[460]=100 day = 25 min val=0 max val=0 row[461]=100 day = 25 min val=0 max val=0 row[462]=100 day = 25 min val=0 max val=0 row[463]=100 day = 25 min val=4.44089e-16 max val=0 row[464]=-1 day = 25 min val=0 max val=0 row[465]=100 day = 25 min val=0 max val=0 row[466]=100 day = 25 min val=0 max val=0 row[467]=100 day = 25 min val=0 max val=0 row[468]=100 day = 26 min val=0 max val=0 row[469]=-1 day = 26 min val=0 max val=0 row[470]=-1 day = 26 min val=0 max val=0 row[471]=100 day = 26 min val=-4.44089e-16 max val=0 row[472]=-1 day = 26 min val=0 max val=0 row[473]=-1 day = 26 min val=0 max val=0 row[474]=100 day = 26 min val=0 max val=0 row[475]=-1 day = 26 min val=0 max val=0 row[476]=100 day = 26 min val=0 max val=0 row[477]=100 day = 26 min val=0 max val=0 row[478]=100 day = 26 min val=0 max val=0 row[479]=100 day = 26 min val=-4.44089e-16 max val=0 row[480]=-1 day = 26 min val=0 max val=0 row[481]=-1 day = 26 min val=0 max val=0 row[482]=-1 day = 26 min val=0 max val=0 row[483]=100 day = 26 min val=1 max val=0 row[484]=-1 day = 26 min val=0 max val=0 row[485]=100 day = 26 min val=0 max val=0 row[486]=100 day = 27 min val=0 max val=0 row[487]=-1 day = 27 min val=0 max val=0 row[488]=-1 day = 27 min val=0 max val=0 row[489]=-1 day = 27 min val=0 max val=0 row[490]=-1 day = 27 min val=0 max val=0 row[491]=-1 day = 27 min val=0 max val=0 row[492]=-1 day = 27 min val=0 max val=0 row[493]=-1 day = 27 min val=0 max val=0 row[494]=100 day = 27 min val=1 max val=0 row[495]=100 day = 27 min val=2 max val=0 row[496]=-1 day = 27 min val=0 max val=0 row[497]=100 day = 27 min val=0 max val=0 row[498]=-1 day = 27 min val=0 max val=0 row[499]=100 day = 27 min val=-8.88178e-16 max val=0 row[500]=-1 day = 27 min val=0 max val=0 row[501]=-1 day = 27 min val=0 max val=0 row[502]=-1 day = 27 min val=0 max val=0 row[503]=100 day = 27 min val=0 max val=0 effective rows=504 out of 504

一瞬、「こんなに効いていないのが支配的であるのなら、とりあえず制約を外して..」という邪な高速化を思いついたのですが、他のインスタンスを観察したところ、むしろ上のような状況の方が特殊であることが分かりました。instance13の方が特殊、ということです。残念。

ちなみに、整数解時、row[494][495]のスラックが整数になっています。これは、LB時にもその萌芽が見られます。Lpsolverは、ベクトル的に最適解に近い解を出力する、ということを基にして（前提にして）解くのがMIPSolve的な解法となります。