論文の概要: Solving the Two-dimensional single stock size Cuting Stock Problem with SAT and MaxSAT
- arxiv url: http://arxiv.org/abs/2604.01732v1
- Date: Thu, 02 Apr 2026 07:52:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-03 14:21:10.596565
- Title: Solving the Two-dimensional single stock size Cuting Stock Problem with SAT and MaxSAT
- Title(参考訳): SATとMaxSATによる2次元シングルストックサイズカットストック問題の解決
- Authors: Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To,
- Abstract要約: 2次元シングルストックサイズカットストック問題(2D-CSSP)は、各アイテムのコピーを複数必要とすることでビンパッキングを一般化し、強い爆発を引き起こす。
本稿では,各コピーがシート割り当て変数を持ち,同じシートに割り当てられたコピーに対してのみ非オーバーラップ制約が活性化されるSATベースのフレームワークを提案する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Cutting rectangular items from stock sheets to satisfy demands while minimizing waste is a central manufacturing task. The Two-Dimensional Single Stock Size Cutting Stock Problem (2D-CSSP) generalizes bin packing by requiring multiple copies of each item type, which causes a strong combinatorial blow-up. We present a SAT-based framework where item types are expanded by demand, each copy has a sheet-assignment variable and non-overlap constraints are activated only for copies assigned to the same sheet. We also introduce an infeasible-orientation elimination rule that fixes rotation variables when only one orientation can fit the sheet. For minimizing the number of sheets, we compare three approaches: non-incremental SAT with binary search, incremental SAT with clause reuse across iterations and weighted partial MaxSAT. On the Cui--Zhao benchmark suite, our best SAT configurations certify two to three times more instances as provably optimal and achieve lower optimality gaps than OR-Tools, CPLEX and Gurobi. The relative ranking among SAT approaches depends on rotation: incremental SAT is strongest without rotation, while non-incremental SAT is more effective when rotation increases formula size.
- Abstract(参考訳): 廃棄物を最小化しながら、需要を満たすために板紙から長方形のアイテムを切ることが中心的な製造課題である。
2次元シングルストックサイズカットストック問題(2D-CSSP)は、各アイテムのコピーを複数必要とすることでビンパッキングを一般化し、強力な組合せ的爆発を引き起こす。
本稿では,各コピーがシート割り当て変数を持ち,同じシートに割り当てられたコピーに対してのみ非オーバーラップ制約が活性化されるSATベースのフレームワークを提案する。
また、1つの方向しかシートに収まらない場合、回転変数を固定する非実用的指向性除去規則を導入する。
シートの数を最小化するために、非インクリメンタルSATとバイナリサーチ、インクリメンタルSATと反復間の節再利用、重み付きMaxSATの3つのアプローチを比較した。
Cui-Zhaoベンチマークスイートでは、最高のSAT構成により、OR-Tools、CPLEX、Gurobiよりも2~3倍のインスタンスが最適で、低い最適性ギャップを達成できます。
SAT の相対的なランク付けは回転に依存する: 漸進 SAT は回転なしで強いが、非増進 SAT は公式サイズが大きくなるとより効果的である。
関連論文リスト
- Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。
本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。
我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
論文 参考訳(メタデータ) (2024-10-11T18:20:08Z) - Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
論文 参考訳(メタデータ) (2023-12-16T12:44:36Z) - Machine Learning for SAT: Restricted Heuristics and New Graph
Representations [0.8870188183999854]
SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。
大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。
我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
論文 参考訳(メタデータ) (2023-07-18T10:46:28Z) - A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。
この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
論文 参考訳(メタデータ) (2023-06-07T12:19:22Z) - Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits [58.83758257568434]
LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。
そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
論文 参考訳(メタデータ) (2022-10-04T09:19:13Z) - SATformer: Transformer-Based UNSAT Core Learning [0.0]
本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。
SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。
SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。
実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
論文 参考訳(メタデータ) (2022-09-02T11:17:39Z) - DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。
DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
論文 参考訳(メタデータ) (2022-05-27T03:20:42Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Effective Dimension Adaptive Sketching Methods for Faster Regularized
Least-Squares Optimization [56.05635751529922]
スケッチに基づくL2正規化最小二乗問題の解法を提案する。
我々は、最も人気のあるランダム埋め込みの2つ、すなわちガウス埋め込みとサブサンプリングランダム化アダマール変換(SRHT)を考える。
論文 参考訳(メタデータ) (2020-06-10T15:00:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。