用SAT方法解决二维下料问题，更高效地减少材料浪费。
Solving the Two-dimensional single stock size Cutting Stock Problem with SAT and MaxSAT
- 将每种物品按需求展开，通过变量约束避免同板重叠。
- 在基准测试中比OR-Tools、CPLEX等工具多验证2-3倍最优解。
- 适合需要精确最优解的工业下料场景，尤其支持旋转优化。
从矩形板材中切割满足需求的矩形件以最小化浪费是核心制造任务。二维单尺寸下料问题（2D-CSSP）推广了装箱问题，需处理每种物品的多个副本，导致组合爆炸。本文提出基于SAT的框架：将物品类型按需求展开，每个副本具有板材分配变量，仅当同板时激活非重叠约束；引入不可行方向消除规则，当仅一种方向可适配板材时固定旋转变量。针对最小化板材数量，比较三种方法：非增量SAT结合二分搜索、增量SAT利用迭代间谓词复用、加权部分最大SAT。在Cui--Zhao基准集上，最优SAT配置比OR-Tools、CPLEX和Gurobi能证明2至3倍更多实例为严格最优，并实现更低最优性间隙。不同旋转策略下性能排序不同：无旋转时增量SAT最强，旋转增加时公式规模扩大，非增量SAT表现更优。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。