CDCL による厳密解法を採用した MILP ソルバー

Transcript

1. CDCL による厳密解法を採用した MILP ソルバー 今井 義弥 2024/11/22 1
2. 自己紹介 • - 2011 : 数学とか離散最適化とか制御理論とかをやっていた • サークル活動でロボット制作に明け暮れていた • 2011 - 2022 : (NTT データ) 数理システムで数理最適化をやっていた • 2022 - : フリーランスとして数理最適化をやっている • OR 学会の普及委員 • 最近は趣味で MILP ソルバーを作っている ެӹࣾஂ๏ਓ
   ೔ຊΦϖϨʔγϣϯζɾϦαʔνֶձ $PNNVOJDBUJPOT
   PG
   UIF
   0QFSBUJPOT
   3FTFBSDI
   4PDJFUZ
   PG
   +BQBO
   ܦӦͷՊֶ WPM
   OP
    ಛूɹ޿͕ΓΏ͘اۀࣄྫɿ ೥൛ &$όοΫΤϯυۀ຿ʹ͓͚Δ਺ཧ࠷దԽͷ׆༻ ʕ;0;0508/ͷྫʕ Πϯλʔωοτ޿ࠂʹ͓͚Δӡ༻࠷దԽͱΫϦΤΠςΟϒ ࣗಈੜ੒ٕज़ͷ։ൃʕ͏Ε͍͠޿ࠂͷ࣮ݱʹ޲͚ͯʕ ग़࢈ҭࣇʹؔ͢Δঁੑ޲͚ίϛϡχςΟαʔϏεʹ͓͚Δ ػցֶशͷ׆༻ࣄྫ ϏζϦʔνʹ͓͚ΔϨίϝϯυͷऔΓ૊Έ ʕಛʹίʔϧυελʔτ໰୊΁ͷରԠʹ͍ͭͯʕ దਖ਼ࡏݿࣗಈௐ੔ํࣜͷ։ൃͱͦͷద༻ ʕ੡଄ྲྀ௨ۀʹ͓͚Δ4$.ͷऔ૊Έࣄྫʕ ਫॲཧϓϥϯτ಺ͷ૷ஔʹର͢Δ഑ஔઃܭʹؔ͢ΔऔΓ૊Έ ෆ࣮֬ੑԼͰͷ࠶ੜՄೳΤωϧΪʔ཈੍ͱ ެฏੑΛߟྀͨ͠ൃిܭը ࿈ࡌ ੈքΛ03͢Δࢹઢ  ୈ*෦ɹ௨৴ɾσδλϧٕज़ͷൃల
    ίϯϐϡʔλͷൃలɿίϯϐϡʔλՊֶͷ਺ֶతجૅʢଓ͖ʣ Φ ϖ Ϩ ồ γ ἀ ϯ ζ ɾ Ϧ α ồ ν ɹ ୈ  ר ɹ ୈ  ߸ ୈרୈ߸ɹ௨ר߸ɹྩ࿨೥݄೔ൃߦʢຖ݄ճ೔ൃߦʣɹ*44/
    2
3. 今日のはなし 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 話すことが多くて全体的にふわっとした説明になります． （雰囲気を感じ取っていただければ…） 3
4. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 4
5. 数理最適化って？ 制約条件を満たし，目的関数を最大または最小にする解を見つける 5
6. 数理最適化って？ 制約条件を満たし，目的関数を最大または最小にする解を見つける 計画の改善・計画作成負荷の低減などのために，様々な場面で使われている • プラントの運転計画 • 装置の特性・運転条件 • コスト最小化・CO2 排出量最小化 • 広告配信 • 広告主広告媒体との契約・運用ルール • 広告効果 (PV・リーチ率) の最大化 • スタッフスケジューリング • 労働基準法・労働契約・勤務ルール • 人件費の削減・サービス品質の向上・ 労働環境の改善 • 生産計画・配送計画・運行計画など… ੡࡞ɾஶ࡞˙ެӹࣾஂ๏ਓɹ೔ຊΦϖϨʔγϣϯζɾϦαʔνֶձɹฤू˙খౡ͋ΏΈɹΠϥετ˙٠஍ɹ࿕ɹσβΠϯ˙ΧΠΫϦΤΠτɹҹ࡮˙ਤॻҹ࡮גࣜձࣾɹୈ  ൛  ೥  ݄࡞੒ ίϯϏχ ߦ੓ మಓ ޻৔ Φϑ Ο εϏϧ ۭߓ 03Λ୳ͤ ʂ ʵ฻Β ͠ʹ༹͚ࠐΉ03ʵ ऩӹ؅ཧ ߤۭӡ௞Λί ϯ τ ϩʔ ϧ͠ ͯ ऩӹΛ࠷େԽ͢ Δ ಈతՁ֨ઃఆɺ ϨϕχϡʔϚωδ ϝϯ τ ௠ྻ ɾ ಈઢ ͍ͭങ͍ͨ ͘ ͳΔ௠ྻʹม͑ ͯ ച্͛૿ ୨ׂɺ Χ ΢ϯς Ο ϯάɺ ಈઢ෼ੳɺ Ϛʔές Ο ϯάɺ ফඅऀߦಈɺ ফඅऀ৺ཧɺ ߦಈ؍࡯ Ξ ϧόΠ τ ɾ γϑ τ ر๬Λ൓өͨ͠γϑ τ γϑ τ εέδ ϡ ʔ Ϧ ϯάɺ ฏ४Խɺ ެฏੑɺ όϥϯεɺ ϝλ ώ ϡ ʔ Ϧ ες Ο Ϋ ε Ϩδ ɾ ଴ͪߦྻ ٬Λ଴ͨͤͣ ɺ εϜ ʔζʹձܭ ଴ͪߦྻɺ ֬཰෼෍ɺ ϑ Υ ʔΫฒͼɺ Ϛϧί ϑ࿈࠯ϞϯςΧϧϩ๏ɺ Ϧ τ ϧͷެࣜ 104
   ɾ Ϗ ο άσʔλ Ͳͷ঎඼͕͍ͭ୭ʹചΕ͔ͨΛ ೺Ѳ͠ ͯൢചΛ༧ଌ Ϛʔές Ο ϯάɺ धཁ༧ଌɺ Ϩίϝ ϯσʔγ ϣ ϯɺ ࡏݿ؅ཧɺ σʔλϚΠ χϯά ࢪઃ഑ஔ ফ๷ॺͷҐஔɺ ֶߍͷ։ߍ΍౷ഇ߹Λ ܾΊ Δ ͨΊͷ৘ใΛఏڙ͢ Δ ࢪઃ഑ஔɺ ౎ࢢܭըɺ ू߹ඃ෴ɺ ެฏੑ Π ϯϑϥ੔උܭը ಓ࿏΍ݐ෺ɺ ަ௨ͳ Ͳ Π ϯϑ ϥ੔උͷޮՌΛ༧ଌ͢ Δ ε Ϛʔ τ γς Ο ɺ ౎ࢢܭըɺ ࣌ܥྻղੳɺ ")1 ʢ֊૚తҙࢥܾఆ๏ʣ ɺ ධՁͷ03 ආ೉ܭը ɾ ๷ࡂ ࡂ֐࣌ͷॅຽͷආ೉৔ॴ΍ ආ೉ܦ࿏ͷܭըΛαϙʔ τ ϚϧνΤʔδ Σϯ τ ɾ γϛ ϡ Ϩʔγϣϯɺ ެڞ੓ࡦ ϝϯςφϯε Π ϯϑ ϥͷϝ ϯςφϯεͷ ܭը࡞ Γ ҟৗݕ஌ɺ ৴པੑ ΤϨϕʔλʔ੍ޚ ΤϨϕʔλ ʔͷ ఀࢭ֊ΛܾΊͯɺ Ҡಈ࣌ؒ΍ࠞࡶΛݮΒ͢ ܈؅ཧɺ γ ϛ ϡ Ϩʔγ ϣ ϯ ۭௐ ʢΤωϧΪʔʣ ΤωϧΪʔݯΛ૊Έ߹Θͤͯ ۭௐΛί ϯ τ ϩʔ ϧ ΤωϧΪʔ ɾ ϛ ο Ϋ εɺ σϚϯ υ ɾ Ϩεϙϯε ϓϩδ ΣΫ τεέδ ϡʔ Ϧ ϯά ࡞ۀͷ։࢝ ɾ ऴྃɺ ͦͷؒͷखॱΛ ݟ͑ ΔԽ͠ ͯ࠷దͳεέδ ϡ ʔ ϧΛܾΊ Δ Ψϯ τ ν ϟʔ τɺ ϑ ϩʔŋμΠ Ξ άϥ Ϝɺ ΞϩʔŋμΠ Ϡάϥ Ϝɺ Ϋ Ϧ ς Ο Χϧύε ࢿ࢈ӡ༻ Ϧ εΫ ͷগͳ͍ ࢿ࢈ϙʔ τ ϑ Υ Ϧ Φ ΛఏҊ͢ Δ ۚ༥޻ֶɺ ฏۉ ɾ ෼ࢄϞσϧɺ Ϙϥς Ο Ϧ ς Ο ɺ ࣌ܥྻղੳɺ 'JO5FDI ഑ૹ ʢ෺ྲྀʣ ࠷దԽ ɾ ࡏݿ؅ཧ λ Π ϛ ϯάྑ ͘ ൃ஫͠ ͯɺ ഇغ΍ฦ඼ΛݮΒ ͠ɺ ঎඼΍ࡏݿΛແବͳ ͘ ؅ཧ ܦࡁతൃ஫ྔɺ ػձඅ༻ɺ ϩ ο τ αΠ ζܾఆϞσϧɺ αϓϥ Π ν Σ ʔ ϯ μΠ Ϡ ిंͷμΠ ϠΛܾΊɺ ஗Ԇ࣌ʹ ΋଎ ͘ ճ෮ͤ͞Δ ۭ࣌ؒω ο τ ϫʔΫ ɺ ਺ཧ࠷దԽɺ ӡߦεέδ ϡ ʔ Ϧ ϯά ৐Γ׵͑ܦ࿏Ҋ಺ ଎ ͘ ָʹ҆ ͘ ໨త஍ʹண ͘ ܦ࿏Λ͢ ͙ ʹڭ͑ Δ άϥ ϑ ɾ ω ο τ ϫʔΫ ɺ ࠷୹࿏ɺ μΠ Ϋ ε τ ϥ๏ ৐຿һεέδ ϡʔ Ϧ ϯά ࢝ൃ͔ Βऴి · Ͱͷӡసख΍ंঠɺ Ӻһɺ อक୲౰ऀͷ࢓ࣄ಺༰ ΛܾΊ Δ γϑ τ εέδ ϡ ʔ Ϧ ϯ άɺ ू߹ඃ෴ɺ ྻੜ੒ εϚʔ τ ϑ Υ ϯ ε Ϛʔ τ ϑ Υ ϯ্Ͱ ޷Έͷ঎඼΍αʔ Ϗε Λࣗಈදࣔ σʔλϚΠ χϯάɺ Ϩίϝ ϯσʔγ ϣ ϯɺ άϥ ϑ ɾ ω ο τ ϫʔΫ ɺ ػցֶश Ϛονϯά ཧ૝ͷύʔ τ φʔ Λݟ͚ͭ Δ ͓ݟ߹͍໰୊ɺ ҆ఆ݁ࠗ໰୊ վࡳ ɾ ଴ͪߦྻ Ӻߏ಺ͷࠞࡶΛγ ϛ ϡ Ϩʔγ ϣ ϯ ͠ ͯ ৐٬ͷྲྀΕΛε Ϝ ʔ ζʹ͢ Δ ଴ͪߦྻɺ ϚϧνΤʔδ Σϯ τ ɾ γ ϛ ϡ Ϩʔγ ϣ ϯ ΤωϧΪʔڙڅ ɾ ഑෼ ઃඋՔಇΛ੍ޚ͠ɺ ΤωϧΪʔधڅΛ࠷దԽ͠ ͯɺ লΤω ɾ লίε τ ʹߩݙ ࠷ద੍ޚɺ ىಈఀࢭܭըɺ γ ϛ ϡ Ϩʔγ ϣ ϯ धཁ༧ଌ ఱީͷมԽ΍ใಓɺ ࣾձಈ޲ͳ Ͳ͔Β ੡඼ͷधཁΛ༧ଌ͢ Δ ࣌ܥྻղੳɺ ճؼ෼ੳ ੜ࢈ܭը ɾ εέδ ϡʔ Ϧ ϯά ਓ ɾ Ϟϊ ɾ ࣌ؒΛޮ཰ྑ ͘ ࢖͍ɺ ඼࣭ ɾ ίε τ ɾ ೲظͷόϥ ϯεͷ औΕͨܭըӡ༻Λ͢ Δ ੜ࢈؅ཧɺ ࡏݿ؅ཧɺ ਺ཧ࠷దԽɺ αϓϥΠ ν Σ ʔϯ ήʔ τׂ౰ͯ ੔උһ΍৐һ͕ಈ͖ ΍͍͢ ήʔ τׂ౰ͯΛܭը͢ Δ ఆ࣌཰ɺ ཭ࢄܥγϛ ϡ Ϩʔγϣϯɺ ੔਺࠷దԽ ٧ࠐΈ ՟෺΍ίϯςφͷੵࡌ཰Λ্͛Δ ᩦཉ ʢͲΜΑ ͘ʣ ๏ɺ ੾ग़͠ ɾ ٧ࠐΈɺ ϝλ ώϡʔϦ ες Ο Ϋε ৐຿һεέδ ϡ ʔ Ϧ ϯά ৐຿һͷۈ຿εέδ ϡ ʔ ϧΛ ܭը͢ Δ γϑ τεέδ ϡʔϦ ϯάɺ ू߹ඃ෴ ൃணεέδϡʔϦϯά ҆શͰޮ཰తͳ཭ൃணͷ εέδ ϡ ʔϧΛܭը ɾ ࣮ߦ ਺ཧ࠷దԽɺ ϚϧνΤʔδ Σ ϯ τ ɾ γ ϛ ϡ Ϩʔγ ϣ ϯ ΦϖϨʔγϣϯζɾϦαʔνʢ0QFSBUJPOT
   3FTFBSDIɿ03ʣ͸ ʮࠔ͍ͬͯΔ ͜ ͱʯ ʢʹ໰୊ʣ ΛՊֶతʹղܾ͢ΔͨΊͷ ʮ໰୊ղ ֶܾʯ Ͱ͢ɻ ໰୊ͷ෼ੳͱղܾͷͨΊͷܭըཱҊ΍ͦͷ࣮ࢪɺҙ ࢥܾఆΛॿ͚Δ ʮֶ࣮ʯ ͳͷͰ͢ɻ 03 ͸໰୊ͷ͋Γ͔΍Ԡ༻ͷൣ ғΛબͼ·ͤΜɻ ͦͷͨΊɺ03 ͷݚڀΛਐΊΔ೔ຊ 03 ֶձ͸ ܦࡁֶɾܦӦֶɾཧֶɾ޻ֶɾ೶ֶɾҩֶɾܳज़ͳͲจܥ ཧܥΛ໰Θͣɺ ͋Γ ͱ͋ΒΏΔ෼໺ͷձһ͔Βߏ੒͞Ε͍ͯ· ͢ɻ IUUQXXXPSTKPSKQNFNCFSTQPTUFSIUNM
   03 ʹؔ͢ΔΑΓৄ͍͠৘ใ͸ͪ͜ΒͷϦϯΫ͔ΒΞΫηεͰ͖·͢ɻ 5
7. 最適化問題の種類 (KKT 条件が) 線形 非線形 連続 離散 LP CQP CNLP NLP MILP MIQP MINLP 簡単に解ける ちょっと解きづらい そこそこ解ける 絶望的に難しい LP 線形計画 MILP 混合整数線形計画 CQP 凸二次計画 MIQP 混合整数二次計画 CNLP 凸非線形計画 NLP (非凸) 非線形計画 MINLP 混合整数非線形計画 6
8. 混合整数線形計画 (MILP) • 目的関数が線形 • 制約条件が線形不等式 • 整数変数と連続変数のどちらもあってよい • 実務的にはおそらく最もよく使われている問題クラス • 整数変数をうまく使って，実務で現れる多くの要件をモデル化できる min cT 1 x + cT 2 y s.t. A1x + A2y ≥ b x ∈ Zm, y ∈ Rn 7
9. MILP では整数変数をフラグとして使うことができる 「整数」というと「個数」をイメージしやすいが， 0-1 変数を使って論理的な要件をモデル化できる 例: 新人 A が出勤するかつ上司 B が出勤しない，ならば先輩 C が出勤する • x, y, z を論理変数とする • x ⇔ 新人 A が出勤する • y ⇔ 上司 B が出勤する • z ⇔ 先輩 C が出勤する • 要件を論理式で書くと x ∧ ¬y ⇒ z • 論理和の形に書き換えると ¬x ∨ y ∨ z • x, y, z を 0-1 変数と思うと (1 − x) + y + z ≥ 1(線形不等式) 8
10. MILP では非線形関数を近似できる たとえば「プラント内の装置の特性が非線形」ということはよくある (消費電力に出力が比例しないなど) • MILP では変数間の非線形な関係を厳密 に表現することはできないが • 0-1 変数を使って折れ線を定式化するこ とは可能 • 具体的な定式化は省略 9
11. 【余談】非線形計画問題 (MI)LP と比較して， 凸な (MI)QP は難しくない (私はまだ実装したことがないが) • QP: 目的関数が二次・制約条件が線形 • 目的関数は非線形だが，KKT 条件の構造は LP と同じ (線形制約+非負制約+相補性条件) • LP と凸 QP はほぼ同じアルゴリズム (単体法・内点法) で解ける より一般の (MI)NLP は難しい • 計算に時間がかかる • よく使われる逐次二次計画法では，QP を繰り返し解く必要がある • 非凸な場合には局所最適解しか得られないこともある • 安定的に解くことが難しく，細かいパラメータ調整が必要になりがち • (MI)LP と比較すると，実務ではあまり使われていない 10
12. ソルバーって？ 最適化問題を入力すると，解を探索してくれる • 入力は最適化問題 • データを与えればいい感じにやってくれるわけではない • ユーザーが要件を最適化問題としてモデル化する必要がある • モデル：数式を使った現実世界のジオラマのようなもの • 解を探索してくれる • いい感じに探索してくれる • ユーザーが解を見つける手続きを考える必要はない 11
13. 探索の方法 (解法) の分類 汎用 ↔ 専用 • 「汎用ソルバー」という言葉はよく使われるものの，明確な定義はたぶんない • LP または ILP かそれよりも一般的な問題クラスを扱うことができて，かつ特定の業務 に特化していないものが汎用と呼ばれることが多い 厳密解法 ↔ 近似解法 • 出力される解の最適性が保証されるのが厳密解法 • 出力される解の最適性が保証されないのが近似解法 • 実務では厳密解法を使っていても計算時間に上限を設けるなどして計算を打ち切るこ とも多く，その場合には最適性が保証されないことになる 12
14. 【余談】汎用ソルバーを使う利点 汎用ソルバーを使うと開発が楽 • 最適化問題の定式化工数 専用アルゴリズムの開発工数 • 要件の変更に頑強 (無駄になる工数が少ないという意味で) 背景: 最適化案件の要件定義の難しさ • 数理最適化案件の多くは意思決定の自動化 • 人間は様々な暗黙知に基づいて意思決定を行っている • エネルギー系の案件はそうでもないかも • しかし，普通の人は自分が使っている暗黙知を説明できない 結果を見せて初めてわかることもある • 早い段階で結果を見せて暗黙知を引き出すことができる (そして要件は覆る) 13
15. 【余談】ソルバーでなんでも解けるわけではない 特に受託開発では，ソルバーで解けなかった，または要件を追加して解けなくなった場合 への備えは必要 備え • 問題を分割する • 粒度で分けて，荒く解いてから細かく解く • 部分で分けて，各部分を独立に解いて，後でつじつまを合わせる • 時系列で分けて，直近部分を解いてから順次未来の部分を解く • 専用アルゴリズムを構築 • 列挙・列生成法 • ヒューリスティクス • 解きづらさの原因になっている要件を諦める • 契約を細かく区切る 14
16. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 15
17. 分枝限定法ソルバー MILP に対するほとんどの厳密解法ソルバーは分枝限定法 • Gurobi, CPLEX, Nuorium Optimizer, SCIP, CBC など • ただし，現在のソルバーの実装は分枝限定法をベースにしつつ様々な手法を取り入れ ている • CSP 的な前処理手法 • ヒューリスティク探索 • 切除平面法 • SAT 的な conflict analysis • など • 分枝限定法に様々な手法を取り入れたことで，今日の MILP ソルバーは非常に高性能な ものとなっている 本日はそれらの手法には触れず，素朴な分枝限定法の話をします 16
18. 記号の定義 P min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h x ∈ {0, 1}m y ∈ Rn P 解きたい MILP • 簡単のために，以降では整数変数はすべて 0-1 と する ※ 一般の整数変数の場合も基本的な考え方は同じ 17
19. 記号の定義 P min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h x ∈ {0, 1}m y ∈ Rn P 解きたい MILP • 簡単のために，以降では整数変数はすべて 0-1 と する ※ 一般の整数変数の場合も基本的な考え方は同じ S 整数変数 xi を値 v に固定する制約条件 xi = v の 集合 • S = {xi1 = v1 , xi2 = v2 , . . . } • |S| ≤ m でもよい 17
20. 記号の定義 P min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h x ∈ {0, 1}m y ∈ Rn P(S) min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h x ∈ [0, 1]m, S y ∈ Rn P 解きたい MILP • 簡単のために，以降では整数変数はすべて 0-1 と する ※ 一般の整数変数の場合も基本的な考え方は同じ S 整数変数 xi を値 v に固定する制約条件 xi = v の 集合 • S = {xi1 = v1 , xi2 = v2 , . . . } • |S| ≤ m でもよい P(S) P の整数変数を連続緩和して，一部の変数を S に 従って固定した問題 (LP) 17
21. 分枝操作 分枝操作 変数の固定の集合 S に対して，まだ固定されてい ない変数 xi を選んで 2 つの集合を作る S0 = S ∪ {xi = 0} S1 = S ∪ {xi = 1} 分枝操作を再帰的に適用 • S を親ノード，S0, S1 を子ノードと思えば木 探索と等価 • 木のサイズは有限なので厳密解法 • 2m 個のリーフノードについて P を解けば最 適解が求まる S = {} x1 = 0 x2 = 0 xm = 0 {x1 = 0, .., xm = 0} x2 = 1 x1 = 1 x2 = 0 x2 = 1 xm = 1 {x1 = 1, .., xm = 1} ※ 例では 1 から順に選んでいるが，変数の 選択順序は任意 当然 2m 回も P(S) を解くわけには行かないので工夫が必要 18
22. 枝刈り 枝刈りのために各ノードで P(S) を解く 木では以下が成立する • 親が実行不可能ならば子も実行不可能 • 親の目的関数値よりも子の目的関数値の方が 大きいまたは等しい 10 x1 = 0 12.5 x1 = 1 10 19
23. 枝刈り 枝刈りのために各ノードで P(S) を解く 木では以下が成立する • 親が実行不可能ならば子も実行不可能 • 親の目的関数値よりも子の目的関数値の方が 大きいまたは等しい 以下の場合に枝刈り (ノードの終端) が可能 • 実行不可能 10 x1 = 0 12.5 x2 = 0 × x1 = 1 10 19
24. 枝刈り 枝刈りのために各ノードで P(S) を解く 木では以下が成立する • 親が実行不可能ならば子も実行不可能 • 親の目的関数値よりも子の目的関数値の方が 大きいまたは等しい 以下の場合に枝刈り (ノードの終端) が可能 • 実行不可能 • 全ての x が整数になった • 枝刈りと同時に暫定解を更新しておく 10 x1 = 0 12.5 x2 = 0 × x2 = 1 13.7 x1 = 1 10 暫定解の目的関数値: 13.7 19
25. 枝刈り 枝刈りのために各ノードで P(S) を解く 木では以下が成立する • 親が実行不可能ならば子も実行不可能 • 親の目的関数値よりも子の目的関数値の方が 大きいまたは等しい 以下の場合に枝刈り (ノードの終端) が可能 • 実行不可能 • 全ての x が整数になった • 枝刈りと同時に暫定解を更新しておく 10 x1 = 0 12.5 x2 = 0 × x2 = 1 13.7 x1 = 1 10 x3 = 0 11 x2 = 0 11.5 暫定解の目的関数値: 11.5 19
26. 枝刈り 枝刈りのために各ノードで P(S) を解く 木では以下が成立する • 親が実行不可能ならば子も実行不可能 • 親の目的関数値よりも子の目的関数値の方が 大きいまたは等しい 以下の場合に枝刈り (ノードの終端) が可能 • 実行不可能 • 全ての x が整数になった • 枝刈りと同時に暫定解を更新しておく • 目的関数値が暫定解以上 (限定操作) 10 x1 = 0 12.5 x2 = 0 × x2 = 1 13.7 x1 = 1 10 x3 = 0 11 x2 = 0 11.5 x2 = 1 × x3 = 1 12 最適な目的関数値: 11.5 19
27. 枝刈り 枝刈りのために各ノードで P(S) を解く 木では以下が成立する • 親が実行不可能ならば子も実行不可能 • 親の目的関数値よりも子の目的関数値の方が 大きいまたは等しい 以下の場合に枝刈り (ノードの終端) が可能 • 実行不可能 • 全ての x が整数になった • 枝刈りと同時に暫定解を更新しておく • 目的関数値が暫定解以上 (限定操作) 10 x1 = 0 12.5 x2 = 0 × x2 = 1 13.7 x1 = 1 10 x3 = 0 11 x2 = 0 11.5 x2 = 1 × x3 = 1 12 最適な目的関数値: 11.5 限定操作を効果的に行えるように，基本的には幅優先探索がもちいられる 19
28. 分枝限定法のまとめ 分枝操作 • S → S0 = S ∪ {xi = 0}, S1 = S ∪ {xi = 1} • 木探索と等価 • 効果的な限定操作のために，基本的に幅優先探索 各ノードで LP を解く • 一部の変数を固定した緩和問題 P(S) 枝刈り • 実行不可能になった場合 • 整数解が得られた場合 • 目的関数値が暫定解以上となった場合 (限定操作) P min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h x ∈ {0, 1}m y ∈ Rn P(S) min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h x ∈ [0, 1]m, S y ∈ Rn 20
29. なぜ分枝限定法で解けるのか？ 最悪ケースでは 2m 個ぐらいのノードの評価が必要 • 実際に，高速な商用ソルバーを使っても解くことができない数十変数程度のインスタ ンスは存在する • 例: MIPLIB2017 の pb-market-split8-70-4 (0-1 変数のみで 70 変数，8 制約) 専用のアルゴリズムを使って 2023 年に初めて解かれた [田中,2024] • 分枝限定法が駄目なのではなく，そもそも MILP は NP-hard • どのようなアルゴリズムに対しても，効率よく解けない例が存在 (と言われている) しかし実用上は高速に解けることが多い • 現実のインスタンスでは緩和解 (ルートノード) の近くに厳密解があることが多いから • 緩和解が厳密解の良い近似になっているとも言える • 評価するノードの数は 2m よりも遥かに少なく済む • 「なぜ現実のインスタンスにそのような傾向があるのか」はよくわからない 21
30. 分枝限定法は MILP に対する厳密解法の決定版なのか？ 分枝限定法の弱点は変数選択の難しさ • 下手な変数を選ぶと，親とほぼ同じ 難しさの子問題 2 つになる • 一度分枝すると原則取り消せない 極端な例 ※ 実際のソルバーはこのような簡単な罠には引っかかってくれない P に 0-1 変数 z を追加した問題を考える P min cT x + dT y s.t. Ax ≥ b, Fx + Gy ≥ h x ∈ {0, 1}m, y ∈ Rn, z ∈ {0, 1} もし z を最初の分枝変数に選んでしまう と，P と同じ難しさの問題が 2 つになる z = 0 P と同じ難しさ z = 1 P と同じ難しさ 22
31. 分枝限定法は MILP に対する厳密解法の決定版なのか？ 分枝限定法の弱点は変数選択の難しさ • 下手な変数を選ぶと，親とほぼ同じ 難しさの子問題 2 つになる • 一度分枝すると原則取り消せない 実際の分枝限定法ソルバーでの対策 • 前処理による余分な変数の削除 • 実際のソルバーでは，z のような 変数は前処理で削除される • 慎重な変数選択 • リスタート (木を破棄してやり直し) 極端な例 ※ 実際のソルバーはこのような簡単な罠には引っかかってくれない P に 0-1 変数 z を追加した問題を考える P min cT x + dT y s.t. Ax ≥ b, Fx + Gy ≥ h x ∈ {0, 1}m, y ∈ Rn, z ∈ {0, 1} もし z を最初の分枝変数に選んでしまう と，P と同じ難しさの問題が 2 つになる z = 0 P と同じ難しさ z = 1 P と同じ難しさ 22
32. 分枝限定法は MILP に対する厳密解法の決定版なのか？ 分枝限定法の弱点は変数選択の難しさ • 下手な変数を選ぶと，親とほぼ同じ 難しさの子問題 2 つになる • 一度分枝すると原則取り消せない 実際の分枝限定法ソルバーでの対策 • 前処理による余分な変数の削除 • 実際のソルバーでは，z のような 変数は前処理で削除される • 慎重な変数選択 • リスタート (木を破棄してやり直し) 極端な例 ※ 実際のソルバーはこのような簡単な罠には引っかかってくれない P に 0-1 変数 z を追加した問題を考える P min cT x + dT y s.t. Ax ≥ b, Fx + Gy ≥ h x ∈ {0, 1}m, y ∈ Rn, z ∈ {0, 1} もし z を最初の分枝変数に選んでしまう と，P と同じ難しさの問題が 2 つになる z = 0 P と同じ難しさ z = 1 P と同じ難しさ この弱点を根本的に解消する手段はないのか？ → CDCL 22
33. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 23
34. CDCL? Conflict Driven Clause Learning • SAT(Satisfiability Problem: 充足可能性問題) の解法として考案された [Bayardo Jr+, 1997][Marques-Silva+,1999] • 現在の SAT ソルバーの多くが CDCL • 2000 年代には更に様々な手法が考案されて SAT ソルバーの性能が飛躍的に向上 • 2010 年には人工知能学会誌でも特集「最近の SAT 技術の発展」が組まれた Conflict Driven Constraint Learning • SAT を整数線形不等式系に拡張した IntSat というアルゴリズムが提案されている [Nieuwenhuis,2014], [Nieuwenhuis+,2023] • Conflict Driven Constraint Learning という言葉が使われたのは 2023 年の論文 • Pseudo Boolean (0-1 変数の線形不等式系など) でも同じようなことが行われている 24
35. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 25
36. SAT（Satisfiability Problem …充足可能性問題） SAT の例 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 • すべての変数はブール変数 • False か True • 各 x1, ¬x1, . . . をリテラル，リテラルを ∨ で結んだ論 理式を節 (Clause) と呼ぶ • 節の集合が与えられたときに，全ての節を充足する解 が存在するかを判定し，存在するならその解を得たい 26
37. SAT（Satisfiability Problem …充足可能性問題） SAT の例 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 • すべての変数はブール変数 • False か True • 各 x1, ¬x1, . . . をリテラル，リテラルを ∨ で結んだ論 理式を節 (Clause) と呼ぶ • 節の集合が与えられたときに，全ての節を充足する解 が存在するかを判定し，存在するならその解を得たい • 左の例は充足可能 • 例えば x = (F, T, T, T, F) が解 • すべての節が充足される (真であるリテラルが少なく とも 1 つ存在) 26
38. SAT（Satisfiability Problem …充足可能性問題） SAT は MILP の特殊ケース • ブール変数を 0-1 変数と思って等価な MILP に書き換えることができる • ( i∈I xi ) ∨ ( j∈J ¬xj ) → i∈I xi − j∈J xj ≥ 1 − |J| • ただし，SAT も NP-hard x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 → min 0 s.t. x1 + x2 ≥ 1 − x2 + x4 + x5 ≥ 0 x3 − x4 + x5 ≥ 0 x4 − x5 ≥ 0, −x4 − x5 ≥ −1 x1 ∈ {0, 1} 27
39. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 S (スタック) ¬x1 1. Decision: x1 に F を割り当て 28
40. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 S (スタック) ¬x1 x2 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 28
41. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 S (スタック) ¬x1 x2 ¬x3 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 28
42. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 S (スタック) ¬x1 x2 ¬x3 ¬x4 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て 28
43. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 S (スタック) ¬x1 x2 ¬x3 ¬x4 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て • Conflict: (x5 ∧ ¬x5 ) 28
44. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 ¬x2 ∨ x4 S (スタック) ¬x1 x2 ¬x3 ¬x4 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て • Conflict: (x5 ∧ ¬x5 ) • Analysys: 節を融合して学習節を生成 (¬x2 ∨ x4 ∨ x5 ) ∧ (x4 ∨ ¬x5 ) ⇒ ¬x2 ∨ x4 ※ 手順の詳細は省略．一般には複数回の融合が必要 学習節は現在の割当 S を否定する 28
45. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 ¬x2 ∨ x4 S (スタック) ¬x1 x2 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て • Conflict: (x5 ∧ ¬x5 ) • Analysys: 節を融合して学習節を生成 (¬x2 ∨ x4 ∨ x5 ) ∧ (x4 ∨ ¬x5 ) ⇒ ¬x2 ∨ x4 ※ 手順の詳細は省略．一般には複数回の融合が必要 学習節は現在の割当 S を否定する 4. Backjump 28
46. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 ¬x2 ∨ x4 S (スタック) ¬x1 x2 x4 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て • Conflict: (x5 ∧ ¬x5 ) • Analysys: 節を融合して学習節を生成 (¬x2 ∨ x4 ∨ x5 ) ∧ (x4 ∨ ¬x5 ) ⇒ ¬x2 ∨ x4 ※ 手順の詳細は省略．一般には複数回の融合が必要 学習節は現在の割当 S を否定する 4. Backjump • Propagation: x4 に T を割り当て 28
47. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 ¬x2 ∨ x4 S (スタック) ¬x1 x2 x4 ¬x5 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て • Conflict: (x5 ∧ ¬x5 ) • Analysys: 節を融合して学習節を生成 (¬x2 ∨ x4 ∨ x5 ) ∧ (x4 ∨ ¬x5 ) ⇒ ¬x2 ∨ x4 ※ 手順の詳細は省略．一般には複数回の融合が必要 学習節は現在の割当 S を否定する 4. Backjump • Propagation: x4 に T を割り当て • Propagation: x5 に F を割り当て 28
48. CDCL(Conflict Driven Clause Learning) の動作例 節 x1 ∨ x2 ¬x2 ∨ x4 ∨ x5 x3 ∨ ¬x4 ∨ x5 x4 ∨ ¬x5 ¬x4 ∨ ¬x5 ¬x2 ∨ x4 S (スタック) ¬x1 x2 x4 ¬x5 x3 1. Decision: x1 に F を割り当て • x1 ∨ x2 による Propagation: x2 に T を割り当て 2. Decision: x3 に F を割り当て 3. Decision: x4 に F を割り当て • Conflict: (x5 ∧ ¬x5 ) • Analysys: 節を融合して学習節を生成 (¬x2 ∨ x4 ∨ x5 ) ∧ (x4 ∨ ¬x5 ) ⇒ ¬x2 ∨ x4 ※ 手順の詳細は省略．一般には複数回の融合が必要 学習節は現在の割当 S を否定する 4. Backjump • Propagation: x4 に T を割り当て • Propagation: x5 に F を割り当て • Propagation: x3 に T を割り当て 28
49. 普通の深さ優先探索 (DPLL) と CDCL の違い CDCL では学習節による枝刈りが可能 • 今回の例では ¬x2 ∨ x4 • 学習節による枝刈りを効果的に行うためにバックジャンプする • 節の数が増えてしまうが，多くの場合枝刈りの効果のほうが大きい DPLL で探索されるノード ¬x1 x2 ¬x3 ¬x4 × x4 × x3 ¬x4 × x4 ¬x5 CDCL で探索されるノード ¬x1 x2 ¬x3 ¬x4 × x4 ¬x5 x3 29
50. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 30
51. 整数線形不等式系に対する Conflict Driven Constraint Learning (IntSat) CDCL を整数線形不等式系に拡張したアルゴリズムが提案されている 整数線形不等式系の例 x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 SAT に対する CDCL とほぼ同じことができる • Decision • x = T, x = F • x ≥ a, x ≤ b, a ∈ Z, b ∈ Z • Propagation • x1 ∧ ¬x2 ∧ (¬x1 ∨ x2 ∨ x3 ) ⇒ x3 • x1 ≤ 1 ∧ (x1 + 2x2 ≥ 2) ⇒ 2x2 ≥ 1 ⇒ x2 ≥ 1 • 学習制約 (Learnt Constraint) の生成 • (¬x2 ∨ x4 ∨ x5 ) ∧ (x4 ∨ ¬x5 ) ⇒ ¬x2 ∨ x4 • (x1 + 2x2 ≥ 2) ∧ (−3x1 + x2 − x3 ≥ 0) ⇒ 3(x1 + 2x2 ) + (−3x1 + x2 − x3 ) ≥ 3 · 2 − 0 ⇒ 7x2 − x3 ≥ 6 31
52. 【ちょっと余談】整数線形不等式系に対する CDCL の問題点 (Rounding Problem) SAT に対する CDCL と同じことをやってみると 1. Decision x1 ≤ 1 x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 32
53. 【ちょっと余談】整数線形不等式系に対する CDCL の問題点 (Rounding Problem) SAT に対する CDCL と同じことをやってみると 1. Decision x1 ≤ 1 • 矛盾が発生 x1 ≤ 1 ∧ (x1 + 2x2 ≥ 2) ⇒ 2x2 ≥ 1 ⇒ x2 ≥ 1 x1 ≤ 1 ∧ (x1 − 2x2 ≥ 0) ⇒ 2x2 ≤ 1 ⇒ x2 ≤ 0 x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 32
54. 【ちょっと余談】整数線形不等式系に対する CDCL の問題点 (Rounding Problem) SAT に対する CDCL と同じことをやってみると 1. Decision x1 ≤ 1 • 矛盾が発生 x1 ≤ 1 ∧ (x1 + 2x2 ≥ 2) ⇒ 2x2 ≥ 1 ⇒ x2 ≥ 1 x1 ≤ 1 ∧ (x1 − 2x2 ≥ 0) ⇒ 2x2 ≤ 1 ⇒ x2 ≤ 0 • SAT と同じように学習制約を生成しようとすると (x1 − 2x2 ) + (x1 − 2x2 ) ≥ 2 + 0 ⇒ x1 ≥ 1 x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 32
55. 【ちょっと余談】整数線形不等式系に対する CDCL の問題点 (Rounding Problem) SAT に対する CDCL と同じことをやってみると 1. Decision x1 ≤ 1 • 矛盾が発生 x1 ≤ 1 ∧ (x1 + 2x2 ≥ 2) ⇒ 2x2 ≥ 1 ⇒ x2 ≥ 1 x1 ≤ 1 ∧ (x1 − 2x2 ≥ 0) ⇒ 2x2 ≤ 1 ⇒ x2 ≤ 0 • SAT と同じように学習制約を生成しようとすると (x1 − 2x2 ) + (x1 − 2x2 ) ≥ 2 + 0 ⇒ x1 ≥ 1 • 学習制約が現在の割当 (x1 ≤ 1) を否定できていない … x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 32
56. 【ちょっと余談】整数線形不等式系に対する CDCL の問題点 (Rounding Problem) SAT に対する CDCL と同じことをやってみると 1. Decision x1 ≤ 1 • 矛盾が発生 x1 ≤ 1 ∧ (x1 + 2x2 ≥ 2) ⇒ 2x2 ≥ 1 ⇒ x2 ≥ 1 x1 ≤ 1 ∧ (x1 − 2x2 ≥ 0) ⇒ 2x2 ≤ 1 ⇒ x2 ≤ 0 • SAT と同じように学習制約を生成しようとすると (x1 − 2x2 ) + (x1 − 2x2 ) ≥ 2 + 0 ⇒ x1 ≥ 1 • 学習制約が現在の割当 (x1 ≤ 1) を否定できていない … バックジャンプできない x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 32
57. 【ちょっと余談】整数線形不等式系に対する CDCL の問題点 (Rounding Problem) SAT に対する CDCL と同じことをやってみると 1. Decision x1 ≤ 1 • 矛盾が発生 x1 ≤ 1 ∧ (x1 + 2x2 ≥ 2) ⇒ 2x2 ≥ 1 ⇒ x2 ≥ 1 x1 ≤ 1 ∧ (x1 − 2x2 ≥ 0) ⇒ 2x2 ≤ 1 ⇒ x2 ≤ 0 • SAT と同じように学習制約を生成しようとすると (x1 − 2x2 ) + (x1 − 2x2 ) ≥ 2 + 0 ⇒ x1 ≥ 1 • 学習制約が現在の割当 (x1 ≤ 1) を否定できていない … バックジャンプできない x1 + 2x2 ≥ 2 x1 − 2x2 ≥ 0 −3x1 + x2 − x3 ≥ 0 0 ≤ x1 ≤ 5 0 ≤ x2 ≤ 2 −4 ≤ x3 ≤ 4 現状の IntSat にはまだ課題がありそう • [Nieuwenhuis,2014], [Nieuwenhuis+,2023] ではこの問題を Rounding Problem と呼ん でいて，対処方法が提案されている • ただし，まだ工夫の余地はありそう 32
58. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 33
59. CDCL で MILP を解くための準備 解きたい問題 P に対して二種類の部分問題を考える • Q: P の整数変数部分をとりだし，制約条件 Λx ≤ Θ と変数の固定 S を追加したもの • P: P の緩和問題に変数の固定 S を追加したもの • S: 整数変数の固定 (xi = 0 or xi = 1) の集合 (すべての変数を含まなくても良い) • Λ, Θ, u: 行列とベクトルとスカラー P min cx + dT y s.t. Ax ≥ b Fx + Gy ≥ h xi ∈ {0, 1}, yj ∈ R Q(Λ, Θ, u, S) s.t. Ax ≥ b Λ1x ≤ Θ1 Λ2x ≤ Θ2 + 1u xi ∈ {0, 1}, S P(S) min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h xi ∈ [0, 1], yj ∈ R, S 34
60. Q を IntSat ソルバーで解く Q(Λ, Θ, u, S) s.t. Ax ≥ b Λ1x ≤ Θ1 Λ2x ≤ Θ2 + 1u xi ∈ {0, 1}, S IntSat ソルバー • 実行可能であれば実行可能解 x∗ を返す • 実行不可能であればその原因 S ⊂ S を返す • Q(Λ, Θ, S ) が実行不可能となる S ⊂ S ※ S は極小である必要はなく，最悪 S = S でもよい • Q を解く際に内部で生成された学習制約は破棄せず保持し ておく • S は整数変数の固定 (xi = 0 or xi = 1) の集合 • Λ, Θ, u は行列・ベクトル・スカラー 35
61. P を単体法で解く P(S) min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h xi ∈ [0, 1], S yj ∈ R 単体法ソルバー • 実行可能である場合，ある定数 u に対して • 目的関数値が u 以下であれば最適解 x∗, y∗ を返す • 目的関数値が u より大きければ Benders Cut λT x ≤ θ + u を返す • 実行不可能であれば Benders Cut λT x ≤ θ を返す 36
62. Benders Cut ? 大規模 MI(L)P の解法として古くから知られている Benders 分解で用いられる不等式 P(S) min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h xi ∈ [0, 1], S yj ∈ R Benders Cut • LP が実行不可能となった場合に生成できる • 目的関数値が一定値以上となった場合にも生成できるが今回は 省略 (目的関数の上限を制約条件と思えばいい) • P の S 以外の制約条件の必要条件 Ax ≥ b ∧ Fx + Gy ≥ h ∧ xi ∈ [0, 1] ⇒ λT x ≤ µ • S を否定する xi ∈ [0, 1] ∧ S ⇒ λT x > µ つまり，P(S) が実行不可能となる理由を 1 本の制約で表したもの 37
63. Benders Cut ? 大規模 MI(L)P の解法として古くから知られている Benders 分解で用いられる不等式 P(S) min cT x + dT y s.t. Ax ≥ b Fx + Gy ≥ h xi ∈ [0, 1], S yj ∈ R Benders Cut • LP が実行不可能となった場合に生成できる • 目的関数値が一定値以上となった場合にも生成できるが今回は 省略 (目的関数の上限を制約条件と思えばいい) • P の S 以外の制約条件の必要条件 Ax ≥ b ∧ Fx + Gy ≥ h ∧ xi ∈ [0, 1] ⇒ λT x ≤ µ • S を否定する xi ∈ [0, 1] ∧ S ⇒ λT x > µ つまり，P(S) が実行不可能となる理由を 1 本の制約で表したもの 「SAT での学習節」 ， 「整数線形不等式系での学習制約」の LP 版が Benders Cut といえる 37
64. IntSat ソルバーと単体法ソルバーを組み合わせた MILP ソルバー ソルバーの構成 • IntSat ソルバーは内部で学習制約を生成 • 単体法ソルバーで生成した Benders Cut を IntSat ソルバーに追加 IntSat ソルバー 単体法ソルバー Benders Cut Learnt Constraint 38
65. IntSat ソルバーと単体法ソルバーを組み合わせた MILP ソルバー ソルバーの構成 • IntSat ソルバーは内部で学習制約を生成 • 単体法ソルバーで生成した Benders Cut を IntSat ソルバーに追加 IntSat ソルバー 単体法ソルバー Benders Cut Learnt Constraint 具体的な手順の一例: S を更新しながら Q(S, Λ, Θ, u), P(S) を解く • Q，P ともに実行可能な場合 • P の目的関数値が上限 u を超えていれば Benders Cut λT x ≤ θ + u を Λ, Θ に追加 • P の解が整数であれば上限 u を更新し，Benders Cut λT x ≤ θ + u を Λ, Θ に追加 • P の解が非整数であれば適当な変数の固定 xi = v を S に追加 • Q が実行可能かつ P が実行不可能な場合 • Benders Cut λT x ≤ θ を Λ, Θ に追加 • Q が実行不可能な場合 • 適当な変数の固定 s ∈ S を S から削除 38
66. 手順の詳細 u := ∞, S := ∅, Λ ∈ R0×m, µ ∈ R0 u: P の最適値の上界, S: 整数変数の部分的な固定 Λ, µ: Benders Cut Q(S, Λ, µ) S = ∅? 終了 S := S\{s} s ∈ S P(S) Λ1 := Λ1 ∪ λ Θ1 := Θ1 ∪ θ P∗ ≤ u? Λ2 := Λ2 ∪ λ Θ2 := Θ2 ∪ θ Q(S, Λ, µ) x∗ 整数? u := P∗ − S := S ∪ {s} Unsat Sat Unsat Sat No No Yes Yes Yes No ※ IntSat ソルバーと単体法ソルバーの連携には様々な方法が考えられ，上記は 2024/3 時点に試したもの．この連携方法がよいという知見が得られているわけではない． また，Q 自体が難しい問題であり現実的な時間で解けない可能性があるため，実装上は IntSat ソルバーを中断して計算を続行するなどの工夫が必要となる． 39
67. 手順の詳細 u := ∞, S := ∅, Λ ∈ R0×m, µ ∈ R0 u: P の最適値の上界, S: 整数変数の部分的な固定 Λ, µ: Benders Cut Q(S, Λ, µ) S = ∅? 終了 S := S\{s} s ∈ S P(S) Λ1 := Λ1 ∪ λ Θ1 := Θ1 ∪ θ P∗ ≤ u? Λ2 := Λ2 ∪ λ Θ2 := Θ2 ∪ θ Q(S, Λ, µ) x∗ 整数? u := P∗ − S := S ∪ {s} Unsat Sat Unsat Sat No No Yes Yes Yes No Q, P が実行可能かつ目的関数値が u 以下かつ x∗ が非整数 →適当な変数の固定 s を S に追加 39
68. 手順の詳細 u := ∞, S := ∅, Λ ∈ R0×m, µ ∈ R0 u: P の最適値の上界, S: 整数変数の部分的な固定 Λ, µ: Benders Cut Q(S, Λ, µ) S = ∅? 終了 S := S\{s} s ∈ S P(S) Λ1 := Λ1 ∪ λ Θ1 := Θ1 ∪ θ P∗ ≤ u? Λ2 := Λ2 ∪ λ Θ2 := Θ2 ∪ θ Q(S, Λ, µ) ※ Benders Cut は S に対して成立しないので 　ここでの Q は常に実行不可能 x∗ 整数? u := P∗ − S := S ∪ {s} Unsat Sat Unsat Sat No No Yes Yes Yes No Q または P が実行不可能または目的関数値が u より大きい →必要に応じて Benders Cut を生成・追加し，S から適当な変数の固定を削除 39
69. 手順の詳細 u := ∞, S := ∅, Λ ∈ R0×m, µ ∈ R0 u: P の最適値の上界, S: 整数変数の部分的な固定 Λ, µ: Benders Cut Q(S, Λ, µ) S = ∅? 終了 S := S\{s} s ∈ S P(S) Λ1 := Λ1 ∪ λ Θ1 := Θ1 ∪ θ P∗ ≤ u? Λ2 := Λ2 ∪ λ Θ2 := Θ2 ∪ θ Q(S, Λ, µ) x∗ 整数? u := P∗ − S := S ∪ {s} Unsat Sat Unsat Sat No No Yes Yes Yes No Q, P が実行可能かつ目的関数値が u 以下かつ x∗ が整数 →最適値の上界 u を更新 39
70. 手順の詳細 u := ∞, S := ∅, Λ ∈ R0×m, µ ∈ R0 u: P の最適値の上界, S: 整数変数の部分的な固定 Λ, µ: Benders Cut Q(S, Λ, µ) S = ∅? 終了 S := S\{s} s ∈ S P(S) Λ1 := Λ1 ∪ λ Θ1 := Θ1 ∪ θ P∗ ≤ u? Λ2 := Λ2 ∪ λ Θ2 := Θ2 ∪ θ Q(S, Λ, µ) x∗ 整数? u := P∗ − S := S ∪ {s} Unsat Sat Unsat Sat No No Yes Yes Yes No S = ∅ となる場合には終了 (u = ∞ なら P は実行不可能，そうでなければ u が最適値) 39
71. 手順の詳細 …本当に厳密解法なのか u := ∞, S := ∅, Λ ∈ R0×m, µ ∈ R0 u: P の最適値の上界, S: 整数変数の部分的な固定 Λ, µ: Benders Cut Q(S, Λ, µ) S = ∅? 終了 S := S\{s} s ∈ S P(S) Λ1 := Λ1 ∪ λ Θ1 := Θ1 ∪ θ P∗ ≤ u? Λ2 := Λ2 ∪ λ Θ2 := Θ2 ∪ θ Q(S, Λ, µ) x∗ 整数? u := P∗ − S := S ∪ {s} Unsat Sat Unsat Sat No No Yes Yes Yes No Benders Cut の生成または上界の更新を行わない無限ループが存在しなければ厳密解法 ※ S := S ∪ {s} での s の選び方に注意する必要がある（が本日は割愛） 39
72. 【参考】数値実験 • MIPLIB2017 のインスタンスのうち 0-1 変数だけからなる 190 問に対して，SCIP で前処 理を行ったデータを使用 • 初めて動くようになった (2024/3) 時点での結果 • これ以降 2 ヶ月ほど調整してみたが，ほとんど改善しなかった • 今は気を取り直して Rust で再実装している • 実行可能解を見つけるだけであればそれなりの性能だが，最適性を証明できた問題は 少ない ソルバー 600 秒以内に実行可能解が得られた問題数 600 秒以内に解けた問題数 CBC ※ 119 65 SCIP 151 80 CDCL 147 54 ※ CBC のタイムアウト機能にバグがあるようで，タイムアウトしない場合には強制終了しているため，正確な 値ではないかもしれない 40
73. 分枝限定法との違い 分枝しない + 変数の固定を取り消すことができる • 分枝限定法は木探索と等価 S → S0 = S ∪ {xi = 0}, S1 = S ∪ {xi = 1} • CDCL は木探索ではない S → S ∪ {xi = v} または S → S\{xi = v} 代わりに学習制約と Benders Cut を生成し，保持し続ける必要がある • 強力な枝刈りができる一方で，学習制約が増えると計算が重たくなる 原則深さ優先探索になる • 幅優先探索ではないので，限定操作が効果を発揮しづらいかもしれない • ただし，CDCL に分枝操作を追加することは容易 ※最近の一部の分枝限定法ソルバーでは学習節・学習制約を生成して枝刈りに使用している [Achterberg,2007][Mexi+,2023] ので，同じものに収斂していくのかもしれない 41
74. 分枝しないと何が嬉しいのか (分枝限定法の弱点の話) 極端な例 (再掲) P に 0-1 変数 z を追加した問題を考える P min cT x + dT y s.t. Ax ≥ b, Fx + Gy ≥ h x ∈ {0, 1}m, y ∈ Rn z ∈ {0, 1} もし z を最初の分枝変数に選んでしまう と，P と同じ難しさの問題が 2 つになる z = 0 P と同じ難しさ z = 1 P と同じ難しさ CDCL ではこの問題は発生しない • 学習制約・Benders Cut に z が含まれる ことはない • 学習制約・Benders Cut は部分問題が 実行不可能となる理由を説明する不等 式で，z は実行不可能の理由になりえな いから • z = 0 の場合と z = 1 の場合の 2 回同じ 問題を解くことにはならない 42
75. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 43
76. Benders 分解 もとの問題を 2 つの部分問題に分解して繰り返し解くことで厳密解を得る Q 整数変数部分に Benders Cut を追加した問題 (ILP) P Q の最適解 x∗ をパラメータとした，P の連続変数部分の問題 (LP) • Benders Cut を生成して Λ, Θ に追加 P min cx + dT y s.t. Ax ≥ b Fx + Gy ≥ h xi ∈ {0, 1}, yj ∈ R Q (Λ, Θ) min cT x + z s.t. Ax ≥ b Λ1x ≤ Θ1 Λ2x ≤ Θ2 + 1z xi ∈ {0, 1}, z ∈ R P (x∗) min dT y s.t. Gy ≥ h − Fx∗ yj ∈ R 44
77. Benders 分解との対比 Benders 分解 • S のような状態を持たない • Benders Cut を蓄積するだけ • Q は最適化問題 • 目的関数を改善しやすい x が得ら れることを期待できる • P では全ての整数変数 x を固定 CDCL による MILP の解法 • 変数の固定 S を更新しつつ部分問題を解く • Q は一部の変数を固定した制約充足問題 • 比較的容易に解ける • IntSat ソルバーを使うことができる • P では一部の x だけを固定 (他は連続緩和) • より強い Benders Cut が得られることを期 待できる 45
78. Benders 分解との対比 Benders 分解 • S のような状態を持たない • Benders Cut を蓄積するだけ • Q は最適化問題 • 目的関数を改善しやすい x が得ら れることを期待できる • P では全ての整数変数 x を固定 CDCL による MILP の解法 • 変数の固定 S を更新しつつ部分問題を解く • Q は一部の変数を固定した制約充足問題 • 比較的容易に解ける • IntSat ソルバーを使うことができる • P では一部の x だけを固定 (他は連続緩和) • より強い Benders Cut が得られることを期 待できる なぜ強い Benders Cut を期待できるのか • Benders Cut は変数の固定 S を否定する制約条件 • CDCL を使った方法では固定される変数が少ない • より少ない変数の固定 (=弱い仮定) を否定するので，強い制約になっていそう 45
79. SMT(Satisfiability Modulo Theories) ソルバー SAT ソルバー + 理論ソルバー • 命題論理を扱う SAT ソルバーに，理論ソルバーを外付け • 理論ソルバーは命題論理で効率的に表現できない理論を扱う • 理論をラップして，命題論理を入出力とするブラックボックスのように振る舞う • 配列理論などの理論ソルバーを使って，プログラム検証に適用されていたりする（らしい） Sat ソルバー 理論ソルバー Propagation, Explain, Leant Clause Learnt Clause 46
80. SMT(Satisfiability Modulo Theories) ソルバー SAT ソルバー + 理論ソルバー • 命題論理を扱う SAT ソルバーに，理論ソルバーを外付け • 理論ソルバーは命題論理で効率的に表現できない理論を扱う • 理論をラップして，命題論理を入出力とするブラックボックスのように振る舞う • 配列理論などの理論ソルバーを使って，プログラム検証に適用されていたりする（らしい） Sat ソルバー 理論ソルバー Propagation, Explain, Leant Clause Learnt Clause 理論ソルバーの機能の例 (2x1 + x2 − x3 ≤ 1 の場合) • Propagation • 割当 x1 = 1 を通知されたら割当 x2 = 0, x3 = 1 を返す • Explain (Propagation の理由を説明) • x2 = 0 の理由を聞かれたら節 x1 = 0 ∨ x2 = 0 を返す • 実行不可能を検知したら Leant Clause を返す • 割当 x1 = 1, x3 = 0 を通知されたら，充足不可能であ る旨と学習節 x = 0 ∨ x = 1 を返す 46
81. SMT ソルバーとの対比 (MILP の場合) SMT ソルバー Sat ソルバー 整数線形不等式理論ソルバー 単体法ソルバー Propagation, Explain, Leant Clause Learnt Clause Learnt Clause CDCL による MILP の解法 IntSat ソルバー 単体法ソルバー Benders Cut Learnt Constraint 原理的には同じもので，中身が SAT ソル バーか IntSat ソルバーかの違い 47
82. SMT ソルバーとの対比 (MILP の場合) SMT ソルバー Sat ソルバー 整数線形不等式理論ソルバー 単体法ソルバー Propagation, Explain, Leant Clause Learnt Clause Learnt Clause CDCL による MILP の解法 IntSat ソルバー 単体法ソルバー Benders Cut Learnt Constraint 原理的には同じもので，中身が SAT ソル バーか IntSat ソルバーかの違い 最初は SMT ソルバーを作ろうとしていたのだが • SAT+整数線形不等式理論ソルバーを使った実験で思っていた性能が得られなかった • 線形不等式と節のギャップが大きすぎることが原因と考えている • 途中で IntSat ソルバーを使う方針に切り替えた • Benders Cut が整数線形不等式であることとの相性はいいかも 47
83. SAT, SMT, IntSat ソルバーとの関係 SAT ソルバー 命題論理 SMT ソルバー 様々な理論 PB・IntSat ソルバー 0-1 または一般整数 理論ソルバーを外付け CDCL そのものを拡張 48
84. SAT, SMT, IntSat ソルバーとの関係 SAT ソルバー 命題論理 SMT ソルバー 様々な理論 PB・IntSat ソルバー 0-1 または一般整数 僕の考えた最強のソルバー 整数+連続 理論ソルバーを外付け CDCL そのものを拡張 中身を IntSat に 単体法ソルバーを外付け 似た取り組みはいっぱいありそう ([Devriendt+,2021] など) 48
85. 数理最適化・ソルバーって？ 分枝限定法 CDCL SAT に対する CDCL 整数線形不等式系に対する CDCL(IntSat) :::::::::::::::::::::::: CDCL による MILP の解法 他の厳密解法との関連 まとめ 49
86. まとめ • 分枝限定法 • 広く使われている • 実用上は高速に解けることが多い • 変数選択の難しさが弱点 (かもしれない) • CDCL をもちいた MILP の解法 • IntSat ソルバー + 単体法ソルバー • 分枝限定法の弱点を回避できそう • 原理的には Benders 分解・SMT ソルバーとの関連が深い • 【参考】数値実験結果 • 実行可能解を見つける能力に関しては既存の（オープンソースの）分枝限定法ソルバーに 近い結果が得られている • が，商用ソルバーとの差は大きい • 最適性を証明する能力でははまだ及ばない 50
87. 参考文献 • Achterberg, Tobias. (2007). Conflict analysis in mixed integer programming. Discrete Optimization. 4. 4-20. https://doi.org/10.1016/j.disopt.2006.10.006 • Bayardo Jr, R. J., & Schrag, R. (1997). Using CSP look-back techniques to solve real-world SAT instances. In Aaai/iaai (pp. 203-208). • Devriendt, J., Gleixner, A. & Nordström, J. (2021), Learn to relax: Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search. Constraints 26, 26 – 55. https://doi.org/10.1007/s10601-020-09318-x • J. P. Marques-Silva & K. A. Sakallah. (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Transactions on Computers, vol. 48, no. 5, pp. 506-521. https://doi.org/10.1109/12.769433 • Gioni Mexi, Timo Berthold, Ambros Gleixner, Jakob Nordström. Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. arXiv preprint arXiv:2307.14166. https://doi.org/10.48550/arXiv.2307.14166 • Nieuwenhuis, R. (2014). The IntSat Method for Integer Linear Programming. In: O’ Sullivan, B. (eds) Principles and Practice of Constraint Programming. CP 2014. Lecture Notes in Computer Science, vol 8656. Springer, Cham. https://doi.org/10.1007/978-3-319-10428-7_42 • Nieuwenhuis, R., Oliveras, A., & Rodríguez-Carbonell, E. (2023). IntSat: integer linear programming by conflict-driven constraint learning. Optimization Methods and Software, 39(1), 169 – 196. https://doi.org/10.1080/10556788.2023.2246167 • 田中大毅. (2024). 列挙の方法による market split 問題の解法, 日本オペレーションズ・リサーチ学会 2024 年春季研究 発表会アブストラクト集 2-D-12 51