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.

翻译：从板材上切割矩形件以满足需求并最小化废料是制造领域的核心任务。二维单规格板材切割排样问题（2D-CSSP）通过要求每种零件类型具有多个副本而泛化了装箱问题，这导致了强烈的组合爆炸。我们提出了一种基于SAT的框架，其中按需求展开零件类型，每个副本具有一个板材分配变量，且仅对分配到同一板材的副本激活非重叠约束。我们还引入了一种不可行方向消除规则，当仅有一种方向可适配板材时固定旋转变量。为最小化板材数量，我们比较了三种方法：带二分查找的非增量SAT、跨迭代重用子句的增量SAT以及加权部分MaxSAT。在Cui-Zhao基准测试套件上，我们的最佳SAT配置比OR-Tools、CPLEX和Gurobi多验证两至三倍的实例为可证明最优，并实现了更低的最优性差距。SAT方法间的相对排名取决于旋转：无旋转时增量SAT最强，而当旋转增加公式规模时非增量SAT更为有效。