Solving the Two-dimensional single stock size Cuting Stock Problem with SAT and MaxSAT
This work addresses a combinatorial optimization problem in manufacturing for cutting stock planning, offering incremental improvements in solver performance for specific benchmarks.
The authors tackled the Two-Dimensional Single Stock Size Cutting Stock Problem by developing a SAT-based framework with novel constraints and orientation rules, resulting in their best configurations certifying two to three times more instances as provably optimal and achieving lower optimality gaps than existing solvers like OR-Tools, CPLEX, and Gurobi.
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.