💻 computer science

Solving the Two-dimensional single stock size Cuting Stock Problem with SAT and MaxSAT

本論文は、2 次元単一ストックサイズ切断問題に対して、アイテムの需要展開と非重複制約の条件付活性化、および不適切な向きを排除するルールを組み合わせた SAT/MaxSAT ベースの枠組みを提案し、既存の最適化ソルバーと比較してより多くのインスタンスで最適性を証明し、より高い最適性ギャップの達成を実現したことを示しています。

原著者： Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

公開日 2026-04-03

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

紙の無駄をゼロに！「パズルと魔法の論理」で製造業を革新する研究

こんにちは。今日は、工場で使われる「大きな板（金属やガラス、布など）」から、必要な大きさの部品を切り取るという、一見単純ですが実は非常に難しい問題についてお話しします。

この研究は、**「どうすれば最も少ない枚数の板で、すべての部品を切り取れるか？」**という問いに、最新のコンピュータの「論理パズル」技術を使って答えたものです。

1. 問題の正体：巨大なパズルと「注文の嵐」

想像してみてください。あなたは工場の職人です。
大きな長方形の「板（シート）」が山積みになっています。そこから、長方形の「部品」を切り出さなければなりません。

通常の箱詰め問題（2D-BPP）： 1 種類の部品が 1 つだけある場合。
今回の問題（2D-CSSP）： 1 種類の部品が何十個も必要という場合。

ここがミソです。もし「A 型の部品が 20 個必要」だとしたら、コンピュータは「A 型の 1 番目」「A 型の 2 番目」……と、それぞれを別々のキャラクターとして扱わなければなりません。
これは、**「同じ顔をした双子が 20 人、30 人、40 人……と大勢やってきて、全員が同じパズルを解こうとしている」**ような状態です。

従来の方法では、この「大勢の双子」を一人ずつ処理しようとして、計算量が爆発し、答えが出るまでに時間がかかりすぎたり、最善の答えが見つからなかったりしていました。

2. 解決策：魔法の「論理パズル（SAT）」

この研究のチームは、**「SAT（ブーリアン充足可能性）」**という、コンピュータが「真（True）」か「偽（False）」かを瞬時に判断する技術を使いました。

① 「同じシートに載っているか？」という魔法のルール

従来のやり方では、「すべての部品同士が重ならないように」というルールを、全部品同士に適用しようとしました。しかし、「A 型の 1 番目」と「B 型の 5 番目」が、もし「違うシート」に載っているなら、重なるかどうかは関係ありません。

この研究では、**「もし 2 つの部品が『同じシート』に割り当てられている場合だけ、重ならないルールを適用する」という賢い仕組みを作りました。
まるで、「同じ部屋にいる人同士だけ、ぶつからないように気をつけて」**というルールを、部屋ごとに適用しているようなものです。これにより、計算の負担が劇的に減りました。

② 「回転禁止」の魔法

部品を 90 度回転させると、収まり方が変わります。しかし、もし「縦向きだと板からはみ出してしまう」なら、「回転させない」というルールを最初から固定してしまいます。
これは、**「このパズルピースは、横にすると入りきらないから、縦にするしかないね！」**と、最初から無駄な選択肢を消し去るようなものです。

③ 「記憶力」を活かす 2 つの戦術

答えを探すには、2 つの異なる戦術を試し、どちらが得意かを見極めました。

インクリメンタル SAT（積み重ね戦術）：
「10 枚の板で足りるかな？」と試して失敗したら、その失敗から学んだ教訓（「この組み合わせはダメだ」という記憶）を捨てずに、「11 枚で試す」時にそのまま持ち越す方法です。
- 得意分野： 部品が回転しないシンプルな場合。失敗の記憶が次の試行にそのまま役立ちます。
ノン・インクリメンタル SAT（リセット戦術）：
部品を回転させると、パズルの形が複雑になりすぎて、前の記憶が邪魔になることがあります。そんな時は、**「1 枚ずつ、頭をリセットして fresh にやり直す」**方法です。
- 得意分野： 部品を回転させて複雑な配置をする場合。

3. 結果：既存の「プロ」を凌駕する性能

このチームは、世界で最も有名なベンチマーク（テスト用データセット）を使って、この方法を**「OR-Tools（Google 製）」「CPLEX」「Gurobi」**といった、業界で使われている最高峰の商業ソフトウェアと比較しました。

結果は驚異的でした。

最適解の証明： 商業ソフトウェアが「これが最適解です」と証明できたのは 1〜7 件でしたが、この SAT 方式は16〜18 件も証明しました。2〜3 倍の成果です。
無駄の少なさ： 見つかった解の「無駄（隙間）」の割合も、既存のソフトよりもはるかに少なかったです。

特に面白いのは、「回転あり・なし」によって、得意な戦術が変わるという点です。

回転なしなら「積み重ね戦術（記憶を活かす）」が最強。
回転ありなら「リセット戦術（頭をリセットする）」が最強。

これは、**「道具は使い分けが重要」**という、職人の知恵をコンピュータが学んだようなものです。

4. まとめ：なぜこれが重要なのか？

この研究は、単に「パズルが速く解ける」だけでなく、**「製造現場の無駄を減らし、コストを下げ、環境にも優しい」**ことを意味します。

金属板、ガラス、布地の切り取りは、材料費が非常に高いです。
1 枚でも板を節約できれば、それは莫大な節約になります。

この「論理パズル」の技術は、従来の「力任せ」の計算方法では届かなかった、**「複雑で大量の注文」**という壁を乗り越える新しい鍵となりました。

「同じ顔の双子が何十人もいても、彼らが『同じ部屋』にいるかどうかだけ気にすれば、パズルは驚くほど簡単になる」。
そんな、シンプルで美しい発想が、工場の未来を変えようとしています。

論文要約：SAT と MaxSAT を用いた 2 次元単一ストックサイズ切断問題の解決

1. 問題の定義

本論文は、**2 次元単一ストックサイズ切断問題（2D-CSSP: Two-Dimensional Single Stock Size Cutting Stock Problem）**に焦点を当てています。

目的: 同一サイズの原材料シートから、複数の種類と需要（個数）を持つ長方形の部品を切り出し、使用するシート数を最小化し、廃棄物を削減することです。
難易度: この問題は、各アイテムタイプに需要（ $d_t \ge 1$ ）が存在する点で、従来の 2 次元ビンパッキング問題（2D-BPP）を一般化したものです。需要の存在により、検索空間が乗法的に膨張し、従来の厳密解法（列生成法や混合整数計画法 MIP）では大規模な需要に対してスケーラビリティが低下するという課題があります。
既存手法の限界: 既存のヒューリスティック手法は大規模インスタンスを処理できますが、最適性の証明（Certificate of Optimality）を提供できません。一方、商用ソルバー（CPLEX, Gurobi, OR-Tools）は中規模インスタンスでも最適性を証明するのに時間がかかるか、失敗することが多いです。

2. 手法と提案システム

著者らは、2D-CSSP に対して初めてSAT（充足可能性問題）および MaxSAT ベースのフレームワークを提案しました。

2.1. SAT エンコーディングの核心

需要によるアイテムの展開: 各アイテムタイプを需要数だけコピー（複製）として展開し、各コピーにシート割り当て変数を割り当てます。
条件付き非重なり制約: 従来のパッキング問題と異なり、非重なり制約は「同じシートに割り当てられたコピーのペア」に対してのみ発動するように設計されています。これにより、異なるシート上のアイテム間の不要な制約を排除しています。
順序符号化（Order Encoding）: 座標変数を整数ではなく、線形数のブール変数で表現する手法を採用し、エンコーディングのコンパクトさを保っています。
対称性の破壊（Symmetry Breaking）:
- 同じタイプのコピー間の順序制約。
- シートの使用順序を固定（シート 1 を先に使うなど）。
- 新規提案: 「実行不可能な向き排除ルール」。シートに収まる向きが 1 つしかない場合、回転変数を固定するルールを導入し、探索空間を削減します。

2.2. 3 つの求解アプローチ

最小シート数 $k$ を求めるために、以下の 3 つのアプローチを比較・評価しました。

非増分 SAT（Binary Search）: 各 $k$ に対して独立して SAT 問題を生成し、二分探索で最適値を求めます。
増分 SAT（Incremental SAT）: 最大シート数 $UB$ 分の公式を一度生成し、仮定（Assumptions）を用いて使用しないシートを無効化します。 $k-1$ で失敗した際に学習された矛盾節（Conflict Clauses）を $k$ の探索で再利用します。
重み付き部分 MaxSAT: 目的関数（使用シート数の最小化）をソフト節として直接エンコードし、1 回のソルバー呼び出しで最適化を行います。

3. 主要な貢献

2D-CSSP 初の SAT エンコーディング: 需要によるアイテム複製と、シート割り当てに基づく条件付き非重なり制約を統合した新しいエンコーディングを提案。
実行不可能な向きの排除ルール: 正方形アイテムだけでなく、シートサイズに対して収まる向きが一意に定まる場合の回転変数の固定を一般化したルールを提案。
大規模ベンチマークでの実証: 30 個の Cui-Zhao ベンチマークインスタンスを用い、商用ソルバー（OR-Tools, CPLEX, Gurobi）との包括的な比較を行った。
回転の有無による手法の優劣の解明:
- 回転なし: 増分 SAT が最も高性能（節の再利用が需要構造と相性が良い）。
- 回転あり: 非増分 SAT が優位（回転により公式が巨大化し、増分 SAT の節データベースが膨大になり、無関係な節が学習を阻害するため）。

4. 実験結果

Cui-Zhao ベンチマーク（30 インスタンス）における結果は以下の通りです。

最適性の証明数:
- 提案された SAT 手法（回転あり）は18 件の最適性を証明。
- 最善の商用ソルバー（OR-Tools CP）は6 件のみ。
- SAT 手法は商用ソルバーの2〜3 倍多くのインスタンスで最適性を証明しました。
最適性ギャップ（Gap）:
- SAT 手法（回転あり）の平均ギャップは3.24%。
- 最善の商用ソルバーは4.63%（OR-Tools CP）またはそれ以上（MIP ソルバーは 13% 以上）。
手法間の比較:
- 回転なし: 増分 SAT（CSP INC SB）が 16 件の最適性を証明し、9.71% のギャップ。
- 回転あり: 非増分 SAT（CSP R）が 18 件の最適性を証明し、3.24% のギャップ。回転により節数が 3 倍に増えるため、増分 SAT の利点が相殺され、非増分 SAT が有利になりました。
商用ソルバーとの対比:
- OR-Tools CP は多くのインスタンスで最良既知解（BKS）を見つけるが、最適性の証明に失敗する傾向が強く見られました。
- MIP ソルバー（CPLEX, Gurobi）は解を見つける速度は速い場合もありますが、証明能力とギャップの面で SAT 手法に劣りました。

5. 意義と結論

本論文は、需要を持つ 2 次元切断問題に対して、SAT ベースのアプローチが従来の MIP や CP ソルバーよりも圧倒的に優れた証明能力と解の質を持つことを実証しました。

理論的意義: 需要による対称性と条件付き制約を扱うための新しい SAT エンコーディングと、回転の有無によって最適な求解戦略が変化するという知見を提供しました。
実用的意義: 製造現場（鋼板、ガラス、家具、衣料など）における材料効率化において、より少ないシート数での最適カットパターンを、短時間で「証明付き」で得られる可能性を示しました。
将来展望: より Tight な下限値の導出、列生成法とのハイブリッド化（SAT を価格付け部分問題に利用）、異種ストックサイズ問題への拡張などが挙げられています。

総じて、この研究は、複雑な幾何学的制約と需要構造を持つ組み合わせ最適化問題において、現代の SAT ソルバー（CDCL エンジン）が非常に強力なツールとなり得ることを示す重要な成果です。