CDCL を用いた MILP の厳密解法

Transcript

1. CDCL を用いた MILP の厳密解法 今井 義弥 2026/9/11 1
2. 自己紹介 • 2011 - 2022 : (NTT データ) 数理システムで数理最適化をやっていた • 2022 - : フリーランスとして数理最適化をやっている • 本学会の研究普及委員 • 企業事例交流会・機関誌での企業事例の特集などを企画している委員会 • 委員会では発表していただける企業の方を随時募集しています • 研究普及委員にお声がけいただくか，学会 HP に記載のメールアドレスにご連絡ください． 広がりゆく企業事例：2023 年版 ECバックエンド業務における数理最適化の活用 ―ZOZOTOWNの例― 経営の科学 vol.70 no.8, 2025 70 第 号 第 号 特集 巻 巻 8 第70巻第8号 通巻776号 令和7年8月1日発行（毎月1回1日発行） ISSN 0030-3674 Communications of the Operations Research Society of Japan 第 第 経営の科学 vol.68 no.8, 2023 68 オペレーションズ・リサーチ オペレーションズ・リサーチ 第68巻第8号 通巻752号 令和5年8月1日発行（毎月1回1日発行） ISSN 0030-3674 Communications of the Operations Research Society of Japan 8 特集 広がりゆく企業事例：2025 年版 ホテル清掃業務における数理最適化の実践 ―暗黙知の形式知化と業務効率化― インターネット広告における運用最適化とクリエイティブ 自動生成技術の開発―うれしい広告の実現に向けて― 信用スコアリングモデルの高度化に向けた軌跡 ―迅速な資金供給に向けて― 出産育児に関する女性向けコミュニティサービスにおける 機械学習の活用事例 機械学習を活用した新製品需要予測モデルの開発 ―需要計画立案業務におけるDX推進事例― ビズリーチにおけるレコメンドの取り組み ―特にコールドスタート問題への対応について― 熟練プランナーに依存しない本船荷役作業計画の 自動化に向けた取組事例 適正在庫自動調整方式の開発とその適用 ―製造流通業におけるSCMの取組み事例― 数理最適化技術による東海道新幹線車両運用 自動作成システムの開発 水処理プラント内の装置に対する配置設計に関する取り組み 物流倉庫パレタイズシステム向け混載積み付け 計画アルゴリズムの開発 不確実性下での再生可能エネルギー抑制と 公平性を考慮した発電計画 連載 世界をORする視線(25)第I部 通信・デジタル技術の発展 (3)コンピュータの発展：コンピュータ科学の数学的基礎（続き12） 公益社団法人 日本オペレーションズ・リサーチ学会 事例研究［論文］ 異なる情報源で指定された折れ線を道路ネットワーク 地図上のパスに照合するための最短路問題へのモデル化 公益社団法人 日本オペレーションズ・リサーチ学会 2
3. 本日の発表内容 一言でまとめると 分枝限定法とは異なるアプローチで，分枝限定法に匹敵する MILP ソルバーを作ることができる （かもしれない） 具体的には 背景 – 分枝限定法とその問題点 提案手法 – CDCL を用いた厳密解法 数値実験 まとめと考察 3
4. 背景 – 分枝限定法とその問題点 提案手法 – CDCL を用いた厳密解法 数値実験 まとめと考察 4
5. 既存の MILP ソルバーのほとんどは分枝限定法 • Gurobi, CPLEX, Nuorium Optimizer, SCIP, CBC など • ただし，現在のソルバーの実装は分枝限定法をベースにしつつ，様々な手法を取り入れている • CSP 的な前処理手法 • ヒューリスティク探索 • 切除平面法 • SAT 的な矛盾解析 (Conflict Analysis) など • 分枝限定法に様々な手法を取り入れたことで，今日の MILP ソルバーは非常に高性能なものと なっている • (本発表では，それらの手法には触れず素朴な分枝限定法の話をします) 5
6. 記号と部分問題の定義 元の問題 P min cTI x + cTR y s.t. AI x ≥ bI • 簡単のために，以降では整数変数はすべて 0-1 とする • 一般の整数変数の場合も (本発表の範囲内では) 基本的 な考え方は同じ AM x + AR y ≥ b M x ∈ {0, 1}m y ∈ Rn 6
7. 記号と部分問題の定義 元の問題 P min cTI x + cTR y s.t. AI x ≥ bI • 簡単のために，以降では整数変数はすべて 0-1 とする • 一般の整数変数の場合も (本発表の範囲内では) 基本的 な考え方は同じ AM x + AR y ≥ b M x ∈ {0, 1}m y ∈ Rn 部分問題 – 分枝限定法ではこの部分問題を繰り返し解く P (S) min cTI x + cTR y s.t. AI x ≥ bI AM x + AR y ≥ bM x ∈ [0, 1]m , S y ∈ Rn • S: 整数変数 xi を値 v に固定する制約条件 xi = v の 集合 • S := {xi1 = v1 , xi2 = v2 , . . . } • |S| ≤ m でもよい • 整数変数を連続緩和し，一部の変数を S に従って固定 した問題 (LP) 6
8. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 7
9. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) 10 x1 = 0 x1 = 1 7
10. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 x1 = 1 x2 = 0 x2 = 1 7
11. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 • 条件を満たせばノードを終端 • 緩和問題が実行不可能 x1 = 1 x2 = 0 x2 = 1 ∞ 7
12. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 • 条件を満たせばノードを終端 • 緩和問題が実行不可能 • 整数解が得られた x1 = 1 x2 = 0 x2 = 1 ∞ 13.7 暫定解の目的関数値: 13.7 7
13. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 • 条件を満たせばノードを終端 • 緩和問題が実行不可能 • 整数解が得られた x1 = 1 x2 = 0 ∞ 10 x2 = 1 x3 = 0 13.7 x3 = 1 11 x2 = 0 x2 = 1 11.5 ∞ 暫定解の目的関数値: 11.5 7
14. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 • 条件を満たせばノードを終端 • 緩和問題が実行不可能 • 整数解が得られた • 目的関数値が，それまでに得られた暫定解を超えた x1 = 1 x2 = 0 ∞ 10 x2 = 1 x3 = 0 x3 = 1 13.7 12 11 x2 = 0 x2 = 1 11.5 ∞ 暫定解の目的関数値: 11.5 7
15. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 • 条件を満たせばノードを終端 • 緩和問題が実行不可能 • 整数解が得られた • 目的関数値が，それまでに得られた暫定解を超えた • 全てのノードが終端されれば終了 • 暫定解が最適解 x1 = 1 x2 = 0 ∞ 10 x2 = 1 x3 = 0 x3 = 1 13.7 12 11 x2 = 0 x2 = 1 11.5 ∞ 暫定解の目的関数値: 11.5 7
16. 分枝限定法の手順 • S := ∅ として緩和問題 P (S) を解く 10 • 適当な変数を選んで S0 := S ∪ {x1 = 0}, S1 := S ∪ {x1 = 1} に場合分け (分枝操作) x1 = 0 12.5 • 緩和問題の求解と分枝操作を繰り返す • 通常は目的関数値が小さいノードを優先 • 条件を満たせばノードを終端 • 緩和問題が実行不可能 • 整数解が得られた • 目的関数値が，それまでに得られた暫定解を超えた x2 = 0 ∞ • 全てのノードが終端されれば終了 • 暫定解が最適解 x1 = 1 10 x2 = 1 x3 = 0 x3 = 1 13.7 12 11 x2 = 0 x2 = 1 11.5 ∞ 暫定解の目的関数値: 11.5 分枝限定法は木を構築するアルゴリズムとみなせる • 計算時間は木のノード数に依存 • 木のノード数は，各ノードでの分枝変数の選び方に依存 7
17. 分枝限定法の問題点 分枝変数の選択が難しい • 各ノードで緩和問題を解いた時点では， 「どの分枝変数を選ぶと結果的に木のノード数が少なく なるか」を予測することは困難 • 分枝操作は原則取り消すことができない 8
18. 分枝限定法の問題点 分枝変数の選択が難しい • 各ノードで緩和問題を解いた時点では， 「どの分枝変数を選ぶと結果的に木のノード数が少なく なるか」を予測することは困難 • 分枝操作は原則取り消すことができない 極端な例 • ある問題に意味のない 0-1 変数 z を追加した 問題を考える min cT x s.t. Ax ≥ b x ∈ {0, 1} z ∈ {0, 1} m • もし最初の分枝変数として z を選ぶと，もと の問題を２回解くことになってしまう z=0 z=1 ※ 実際のソルバーはここまで簡単な罠にはひっかか らない 8
19. 分枝限定法の問題点 分枝変数の選択が難しい • 各ノードで緩和問題を解いた時点では， 「どの分枝変数を選ぶと結果的に木のノード数が少なく なるか」を予測することは困難 • 分枝操作は原則取り消すことができない 実際の分枝限定法ソルバーは様々な対策をしている • 前処理 (さきほどのような簡単なケースであれば，前処理によって不要な変数が削除される) • 慎重な分枝変数選択 (Strong Branching など) • リスタート (木を破棄して最初からやり直す) 8
20. 分枝限定法の問題点 分枝変数の選択が難しい • 各ノードで緩和問題を解いた時点では， 「どの分枝変数を選ぶと結果的に木のノード数が少なく なるか」を予測することは困難 • 分枝操作は原則取り消すことができない 実際の分枝限定法ソルバーは様々な対策をしている • 前処理 (さきほどのような簡単なケースであれば，前処理によって不要な変数が削除される) • 慎重な分枝変数選択 (Strong Branching など) • リスタート (木を破棄して最初からやり直す) しかし，根本的な問題の解消になっていないのでは? 分枝操作を取り消すことのできるアルゴリズムを構築できないか →CDCL 8
21. 背景 – 分枝限定法とその問題点 提案手法 – CDCL を用いた厳密解法 数値実験 まとめと考察 9
22. CDCL? Conflict Driven Clause Learning • SAT(Satisfiability Problem: 充足可能性問題) の解法として考案された [1] [2] • 現在の SAT ソルバーの多くが CDCL • 2000 年代には更に様々な手法が考案されて SAT ソルバーの性能が飛躍的に向上 • 2010 年には人工知能学会誌で特集「最近の SAT 技術の発展」が組まれた Conflict Driven Constraint Learning • SAT の CDCL をより一般の制約充足問題または最適化問題に拡張 • Pseudo-Boolean: 0-1 変数の（主に）線形不等式系 [3] • IntSat: 一般整数変数の線形不等式系 [4] [5] おおまかには，探索中に部分問題が実行不可能 (Conflict) となったら枝刈りのための学習制約を生 成し，探索領域を絞り込んでいくアルゴリズム 10
23. 【余談】Pseudo-Boolean ソルバー • 提案手法では，部分問題を解くために Pseudo-Boolean ソルバーを使用 • 使用している Pseudo-Boolean ソルバーも私が実装したもの • https://github.com/AI448/PBSolver26 • Pseudo Boolean Competition 2026 に参加 • https://www.cril.univ-artois.fr/PB26/ • 0-1 変数の線形不等式の制約充足部門 11
24. 【余談】Pseudo-Boolean ソルバー • 提案手法では，部分問題を解くために Pseudo-Boolean ソルバーを使用 • 使用している Pseudo-Boolean ソルバーも私が実装したもの • https://github.com/AI448/PBSolver26 • Pseudo Boolean Competition 2026 に参加 • https://www.cril.univ-artois.fr/PB26/ • 0-1 変数の線形不等式の制約充足部門 • 全参加ソルバーの中では下から数えたほうが速い • 言い訳 • 上位陣は，もともと高速なソルバーを改造したものが多い • MILP ソルバーのサブルーチンとして開発したものなので前処理をやっていない 11
25. 【余談】Pseudo-Boolean ソルバー • 提案手法では，部分問題を解くために Pseudo-Boolean ソルバーを使用 • 使用している Pseudo-Boolean ソルバーも私が実装したもの • https://github.com/AI448/PBSolver26 • Pseudo Boolean Competition 2026 に参加 • https://www.cril.univ-artois.fr/PB26/ • 0-1 変数の線形不等式の制約充足部門 • 全参加ソルバーの中では下から数えたほうが速い • 言い訳 • 上位陣は，もともと高速なソルバーを改造したものが多い • MILP ソルバーのサブルーチンとして開発したものなので前処理をやっていない • google のソルバーに勝った 11
26. MILP への拡張に関しての，提案手法の方針と関連研究 提案手法のおおまかな方針 • 連続緩和問題を解いて Bender’s Cut を生成 • 連続緩和問題を解く点は分枝限定法と同じ • Bender’s Cut を学習制約として Pseudo-Boolean ソルバーに追加する • (Bender’s Cut を追加できるように拡張したソルバーを使用) • 木構造のかわりに Bender’s Cut を保持することで厳密解法となっている 関連研究 • Pseudo-Boolean ソルバーに連続緩和を活用したもの [6] • 分枝限定法ベースの MIP ソルバーに，CDCL の手法を取り入れたもの [7] [8] 12
27. 提案手法での部分問題の定義 緩和問題 (分枝限定法での部分問題と同じ) • 元の問題 P の整数変数を連続緩和し，一部の変数を S P (S) min cT x + dT y に従って固定した問題 s.t. Ax ≥ b • 以下では S を仮定集合とよぶ F x + Gy ≥ h x ∈ [0, 1]m , y ∈ Rn , S 整数変数部分 Q(Λ, Θ, z ∗ , S) s.t. AI x ≥ bI z ≤ z∗ −  ΛF x ≥ ΘF • 元の問題 P の整数変数部分に以下を追加した問題 • 連続変数 z とその上限制約 • S • 追加の制約条件 ΛF x ≥ ΘF , ΛO x ≤ ΘO + 1z • Bender’s Cut ΛO x ≤ ΘO + 1z xi ∈ {0, 1}, z ∈ R, S 13
28. P (S) を単体法ソルバーで解く P (S) min cT x + dT y s.t. Ax ≥ b F x + Gy ≥ h x ∈ [0, 1]m , y ∈ Rn , S 単体法ソルバーの動作 • 最適解が得られた場合 • 最適解 x∗ と Bender’s Cut λT x ≤ θ + z の係数 λ, θ を返す • 実行不可能である場合 • Bender’s Cut λT x ≥ θ の係数 λ, θ を返す Bender’s Cut? • Bender’s 分解というアルゴリズムで用いられる切除平面 • λT x ≤ θ + z • P の目的関数値が z 以下であるため必要条件 • λ x≥θ T • P が実行可能であるための必要条件 • Pseudo-Boolean の人たちは Farkas Constraint と呼んでいる 14
29. Q(Λ, Θ, z ∗ , S) を Pseudo-Boolean ソルバーで解く Pseudo-Boolean ソルバーの動作 (Q を解き切らなくても良い) Q(Λ, Θ, z ∗ , S) s.t. AI x ≥ bI ΛF x ≥ ΘF ΛO x ≤ ΘO + 1z z ≤ z∗ −  xi ∈ {0, 1}, z ∈ R, S • Q(Λ, Θ, z ∗ , S) が実行可能かもしれない場合 ::::::::::::::::::: • S に対応する必要条件の集合 T := {xi1 = vi1 , · · · } を返す • Q(Λ, Θ, z ∗ , S) が:::::::::::::::::::: 実行不可能と判明した場合 • Q(Λ, Θ, z ∗ , S) が実行可能かもしれない S 0 ⊂ S と S 0 に対応 する必要条件の集合 T 0 を返す • Q(Λ, Θ, z ∗ , ∅) が実行不可能と判明した場合 (後述) 必要条件の集合 T について • Q の制約条件のもとで ∧s∈S s ⇒ ∧t∈T t となる T • Pseudo-Boolean ソルバーが内部で行っている制約伝播に よって容易に得られる • 例： x1 + x2 ≥ 1 という制約がある場合に S = {x1 = 0} で あれば x1 = 0 ⇒ x2 = 1 なので T = {x1 = 0, x2 = 1} 15
30. アルゴリズムの動作イメージ • アルゴリズムの初期状態 変数選択 ヒューリスティック S ∪ {xj = vj } S z∗ S S z∗ λ, θ 単体法ソルバー • S, z ∗ での実行可能性を検証 • 整数変数部分を Pseudo-Boolean ソルバーで検証 • 実行不可能であれば S を S 0 に縮小 S0 Pseudo-Boolean ソルバー T • 仮定集合 S := ∅ • 暫定解の目的関数値 z ∗ := ∞ • 緩和問題を単体法ソルバーで検証 z∗ • Bender’s Cust を生成 • 整数解が得られた際には z ∗ を更新 • S をそれ以上縮小できなくなるまで反復 • S をそれ以上縮小できなくなったら S に新たな要素を追加 • S = ∅ で実行不可能となったら終了 • z ∗ が最適値 16
31. アルゴリズムの動作イメージ • アルゴリズムの初期状態 変数選択 ヒューリスティック S ∪ {xj = vj } S z∗ S S z∗ λ, θ 単体法ソルバー • S, z ∗ での実行可能性を検証 • 整数変数部分を Pseudo-Boolean ソルバーで検証 • 実行不可能であれば S を S 0 に縮小 S0 Pseudo-Boolean ソルバー T • 仮定集合 S := ∅ • 暫定解の目的関数値 z ∗ := ∞ • 緩和問題を単体法ソルバーで検証 z∗ • Bender’s Cust を生成 • 整数解が得られた際には z ∗ を更新 • S をそれ以上縮小できなくなるまで反復 • S をそれ以上縮小できなくなったら S に新たな要素を追加 • S = ∅ で実行不可能となったら終了 • z ∗ が最適値 16
32. アルゴリズムの動作イメージ • アルゴリズムの初期状態 変数選択 ヒューリスティック S ∪ {xj = vj } S z∗ S S z∗ λ, θ 単体法ソルバー • S, z ∗ での実行可能性を検証 • 整数変数部分を Pseudo-Boolean ソルバーで検証 • 実行不可能であれば S を S 0 に縮小 S0 Pseudo-Boolean ソルバー T • 仮定集合 S := ∅ • 暫定解の目的関数値 z ∗ := ∞ • 緩和問題を単体法ソルバーで検証 z∗ • Bender’s Cust を生成 • 整数解が得られた際には z ∗ を更新 • S をそれ以上縮小できなくなるまで反復 • S をそれ以上縮小できなくなったら S に新たな要素を追加 • S = ∅ で実行不可能となったら終了 • z ∗ が最適値 16
33. アルゴリズムの動作イメージ • アルゴリズムの初期状態 変数選択 ヒューリスティック S ∪ {xj = vj } S z∗ S S z∗ λ, θ 単体法ソルバー • S, z ∗ での実行可能性を検証 • 整数変数部分を Pseudo-Boolean ソルバーで検証 • 実行不可能であれば S を S 0 に縮小 S0 Pseudo-Boolean ソルバー T • 仮定集合 S := ∅ • 暫定解の目的関数値 z ∗ := ∞ • 緩和問題を単体法ソルバーで検証 z∗ • Bender’s Cust を生成 • 整数解が得られた際には z ∗ を更新 • S をそれ以上縮小できなくなるまで反復 • S をそれ以上縮小できなくなったら S に新たな要素を追加 • S = ∅ で実行不可能となったら終了 • z ∗ が最適値 S を更新しながら Bender’s Cut を生成していれば，いつか最適解が求まる ※有限時間で停止することを保証するには，T の条件や，非有界な整数変数が存在しないといった仮定が必要 16
34. アルゴリズムの気持ち 分枝限定法 提案手法 S • ルートから木を構築 • S → S ∪ {xj = 0}, S ∪ {xj = 1} • 分枝操作は原則取り消すことができない • 木構造を持たない  • S→ S ∪ {x = v } j j S\{xj = vj } • S を縮小することができる • そのかわりに Bender’s Cut を保持 • 気持ちは近傍探索 • 分枝限定法でのリーフに相当する領域を探索 17
35. 背景 – 分枝限定法とその問題点 提案手法 – CDCL を用いた厳密解法 数値実験 まとめと考察 18
36. 前提 実験の条件 • MIPLIB 2017 のうち，一般整数変数を含まない 720 問を SCIP で前処理して使用 • まだ一般整数変数に対応できていないため • まだ前処理を実装していないため • 提案手法と SCIP 10.0.3, cbc 2.10.12 とを比較 • 各インスタンスをメモリ制限 8GB・シングルスレッドで，8 インスタンスを並列で実行 • ハードウェア CPU: Core i7-10700K, メモリ: 64GB, OS: ubuntu 26.04.1 比較に関しての留意事項 • MIP ソルバーは様々な手法を組み合わせたものであり，今回の実験ではそれらの手法の有無が 同一ではないため，純粋に分枝限定法と CDCL とを比較したものにはなっていない 19
37. 【マニア向けの補足】提案手法の実装について • Primal Heuristics • ルートでの Feasibility Pump • 連続変数を含まない場合のみ，Pseudo-Boolean ソルバーを Primal Heuristic としても併用 • Pseudo-Boolean ソルバーの実行時に暫定解を更新できる解が偶然見つかることがある • 以下は実装していない • 切除平面法 • 対称性の検出・削減 • (SCIP で前処理を行った際に簡単な削減がおこなわれている可能性はある) • 単体法ソルバーの性能がやや低い • 独自に実装した単体法ソルバーを使用しており，速度・安定性が SCIP・CBC よりもやや劣っている 20
38. 0-1 変数のみのインスタンスでの比較 0-1 OPTIMAL + INFEASIBLE_or_UNBOUNDED 100 OPTIMAL 100 SCIP 10.0.3 CBC 2.10.12 SCIP 10.0.3 CBC 2.10.12 60 60 60 # solved 80 # solved 80 # solved 80 40 40 40 20 20 20 0 0 100 200 300 time [s] 400 500 600 INFEASIBLE_or_UNBOUNDED 100 SCIP 10.0.3 CBC 2.10.12 0 0 100 200 300 time [s] 400 500 600 0 0 100 200 300 time [s] 400 500 600 21
39. 連続変数を含むインスタンスでの比較 OPTIMAL + INFEASIBLE_or_UNBOUNDED 200 OPTIMAL 200 SCIP 10.0.3 CBC 2.10.12 175 150 150 150 125 125 125 # solved 175 # solved # solved SCIP 10.0.3 CBC 2.10.12 175 100 100 100 75 75 75 50 50 50 25 25 25 0 0 100 200 300 time [s] 400 500 600 INFEASIBLE_or_UNBOUNDED 200 SCIP 10.0.3 CBC 2.10.12 0 0 100 200 300 time [s] 400 500 600 0 0 100 200 300 time [s] 400 500 600 22
40. 背景 – 分枝限定法とその問題点 提案手法 – CDCL を用いた厳密解法 数値実験 まとめと考察 23
41. まとめと考察 • 分枝限定法とその問題点および，提案手法について紹介 • 数値実験を行いオープンソースの分枝限定法ソルバーと比較 • 0-1 変数のみのインスタンスについては同等程度の性能 • 連続変数を含むインスタンスではまだ及ばない • 連続変数を含むインスタンスでの性能差の理由はよくわかっていないが，以下のような要因が 考えられる • 提案手法の限界 • 最適性を証明するために必要な Bender’s Cut の数が多くなりすぎるということは考えられる • 仮定集合 S を拡大・縮小する際の変数選択など，アルゴリズムの詳細部分の調整不足 • 切除平面法などの手法を実装していないこと 24
42. 参考文献 i [1] Roberto J. Bayardo and Robert C. Schrag. Using csp look-back techniques to solve real-world sat instances. In Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Conference on Innovative Applications of Artificial Intelligence, AAAI’97/IAAI’97, pp. 203–208. AAAI Press, 1997. [2] J.P. Marques-Silva and K.A. Sakallah. Grasp: a search algorithm for propositional satisfiability. IEEE Transactions on Computers, Vol. 48, No. 5, pp. 506–521, 1999. [3] D. Chai and A. Kuehlmann. A fast pseudo-boolean constraint solver. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 24, No. 3, pp. 305–317, 2005. 25
43. 参考文献 ii [4] Robert Nieuwenhuis. The intsat method for integer linear programming. In Barry O’Sullivan, editor, Principles and Practice of Constraint Programming, pp. 574–589, Cham, 2014. Springer International Publishing. [5] Robert Nieuwenhuis, Albert Oliveras, and Enric RodrÃguez-Carbonell. Intsat: integer linear programming by conflict-driven constraint learning. Optimization Methods and Software, Vol. 39, No. 1, pp. 169–196, 2024. [6] Jo Devriendt, Ambros Gleixner, and Jakob Nordström. Learn to relax: Integrating 0-1 integer linear programming with pseudo-boolean conflict-driven search. Constraints, Vol. 26, No. 1-4, pp. 26–55, October 2021. 26
44. 参考文献 iii [7] Tobias Achterberg. Conflict analysis in mixed integer programming. Discrete Optimization, Vol. 4, No. 1, pp. 4–20, 2007. Mixed Integer Programming. [8] Gioni Mexi, Timo Berthold, Ambros M. Gleixner, and Jakob Nordström. Improving conflict analysis in mip solvers by pseudo-boolean reasoning. ArXiv, Vol. abs/2307.14166, , 2023. 27