pith. machine review for the scientific record. sign in

arxiv: 2604.01732 · v2 · submitted 2026-04-02 · 💻 cs.AI · cs.LO

Recognition: no theorem link

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

Tuyen Van Kieu , Chi Linh Hoang , Khanh Van To
Authors on Pith no claims yet

Pith reviewed 2026-05-13 21:32 UTC · model grok-4.3

classification 💻 cs.AI cs.LO
keywords cutting stock problemSAT encodingMaxSATtwo-dimensional packingbin packingmanufacturing optimizationdemand expansionrotation elimination
0
0 comments X

The pith

A SAT encoding with demand expansion and selective non-overlap constraints solves more two-dimensional cutting-stock instances to proven optimality than leading MIP solvers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a SAT-based method for the two-dimensional single-stock-size cutting stock problem, which requires cutting multiple copies of rectangular item types from fixed-size sheets while minimizing total sheets used. Item types are expanded into individual copies, each with a sheet-assignment variable, so that non-overlap constraints apply only among copies placed on the same sheet; an additional rule fixes rotation variables when only one orientation fits. Three minimization strategies are tested: non-incremental SAT with binary search on the number of sheets, incremental SAT that reuses clauses across iterations, and weighted partial MaxSAT. On the Cui-Zhao benchmark suite the strongest SAT configurations certify two to three times as many instances as provably optimal and produce smaller optimality gaps than OR-Tools, CPLEX and Gurobi.

Core claim

The authors encode the 2D-CSSP by expanding each item type according to its demand, introducing sheet-assignment variables for every copy, and activating geometric non-overlap constraints exclusively for copies assigned to the same sheet; they add an infeasible-orientation elimination rule that fixes rotation variables when only one orientation is feasible. For the objective of minimizing the number of sheets they compare non-incremental SAT with binary search, incremental SAT with clause reuse, and weighted partial MaxSAT, showing that the best of these SAT configurations prove optimality on substantially more instances and close optimality gaps faster than commercial MIP solvers on the Cui

What carries the argument

Demand-expansion encoding that creates one variable per copy and activates non-overlap constraints only for copies sharing a sheet, combined with the infeasible-orientation elimination rule.

If this is right

  • Two to three times as many benchmark instances receive certified optimal solutions under the best SAT configurations.
  • Optimality gaps are smaller than those returned by OR-Tools, CPLEX and Gurobi on the same suite.
  • Incremental SAT with clause reuse performs best when rotation is forbidden; non-incremental SAT performs best when rotation is allowed.
  • The relative advantage of SAT over MIP solvers holds across both rotated and non-rotated variants of the problem.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Manufacturers could replace or augment current MIP-based cutting planners with SAT back-ends to reduce wasted sheet area on typical production runs.
  • The selective-activation pattern used for non-overlap constraints may transfer to other packing problems that involve repeated item types, such as three-dimensional bin packing or guillotine cutting.
  • Hybrid solvers that hand off partially solved SAT formulas to MIP engines once the number of open sheets is small could combine the strengths of both paradigms.

Load-bearing premise

The expanded SAT formulas remain solvable by current solvers for the sizes and demands appearing in the tested benchmark set, and that benchmark set is representative of real manufacturing instances.

What would settle it

A new collection of instances with higher demands or different aspect-ratio distributions on which the same SAT configurations no longer certify more optimal solutions or close gaps faster than CPLEX, Gurobi or OR-Tools.

Figures

Figures reproduced from arXiv: 2604.01732 by Chi Linh Hoang, Khanh Van To, Tuyen Van Kieu.

Figure 1
Figure 1. Figure 1: illustrates a small 2D-CSSP instance. Item types t1: 3×2 d1=3 t2: 2×2 d2=3 N=6 copies Optimal packing (k ∗=2) Sheet 1 c1,1 c1,2 c2,1 c2,2 c2,3 W=6 H=4 Sheet 2 c1,3 [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: SB4: the left assignment (a1=false, a2=true) violates ¬a2 ∨a1 and is eliminated; the right is the canonical labelling [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The manuscript introduces a SAT and MaxSAT encoding for the two-dimensional single stock size cutting stock problem (2D-CSSP). Item types are expanded according to their demands, each copy is assigned a sheet via boolean variables, and non-overlap constraints are conditionally activated only for copies on the same sheet. An additional rule eliminates infeasible orientations. For minimizing the number of used sheets, three SAT-based methods are compared: non-incremental SAT with binary search on the number of sheets, incremental SAT reusing clauses, and weighted partial MaxSAT. On the Cui-Zhao benchmark suite, the best SAT configurations are reported to certify optimality for two to three times as many instances as OR-Tools, CPLEX, and Gurobi, while also achieving lower optimality gaps.

Significance. If the results hold, this demonstrates that structure-exploiting SAT encodings can outperform general MIP solvers on 2D cutting-stock benchmarks by managing the combinatorial blow-up through demand expansion and conditional constraints. The explicit comparison of incremental versus non-incremental SAT variants, together with the orientation-elimination rule, supplies concrete guidance on solver choice depending on rotation. The absence of fitted parameters and the direct encoding of the problem are strengths that support falsifiable claims about certified optimality.

major comments (3)
  1. [§5] §5 (Experimental evaluation): The headline claim that SAT certifies two-to-three times more provably optimal solutions requires evidence that the demand-expanded formulas remain tractable. The manuscript must report, for each instance solved to optimality by SAT but not by the MIP solvers, the total number of item copies (sum of demands) and the resulting number of variables and clauses; without these statistics it is impossible to rule out that the reported advantage is an artifact of the particular Cui-Zhao instance sizes rather than a general property of the encoding.
  2. [§4.2] §4.2 (Non-overlap encoding): The conditional activation of non-overlap constraints only for copies assigned to the same sheet is described as reducing clause count, yet the paper does not state the asymptotic size of the generated formula when a sheet receives k copies of the same type. If the pairwise non-overlap clauses are still generated for every pair of copies that could share a sheet, the quadratic dependence on demand remains and must be quantified for the largest solved instances.
  3. [§3] §3 (Infeasible-orientation elimination): The rule that fixes rotation variables when only one orientation fits the sheet is presented as a preprocessing step, but it is unclear whether the rule is applied before encoding or encoded as unit clauses, and whether its application preserves the completeness of the optimality certificate when rotation is allowed. A short proof sketch or counter-example check would remove this ambiguity.
minor comments (2)
  1. [Abstract] The abstract states 'two to three times more instances' without giving the exact counts; replace this with precise numbers (e.g., 'X out of Y versus Z out of Y') and move the detailed table to the results section.
  2. Table captions and axis labels in the experimental figures should explicitly state the time limit used for all solvers and whether any solver-specific tuning was performed.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive and detailed comments. We address each major point below and have revised the manuscript to incorporate the requested clarifications and data where feasible.

read point-by-point responses

  1. Referee: [§5] §5 (Experimental evaluation): The headline claim that SAT certifies two-to-three times more provably optimal solutions requires evidence that the demand-expanded formulas remain tractable. The manuscript must report, for each instance solved to optimality by SAT but not by the MIP solvers, the total number of item copies (sum of demands) and the resulting number of variables and clauses; without these statistics it is impossible to rule out that the reported advantage is an artifact of the particular Cui-Zhao instance sizes rather than a general property of the encoding.

    Authors: We agree that these statistics are necessary to substantiate the claim. In the revised manuscript we have added a new table in §5 that lists, for every instance solved to optimality by SAT but not by OR-Tools, CPLEX or Gurobi, the total number of item copies (sum of demands), the number of Boolean variables, and the number of clauses in the generated formula. The data show that the largest such instances contain at most a few thousand copies and produce formulas with fewer than 800 000 clauses, confirming that the performance advantage is not an artifact of unusually small demands. revision: yes

  2. Referee: [§4.2] §4.2 (Non-overlap encoding): The conditional activation of non-overlap constraints only for copies assigned to the same sheet is described as reducing clause count, yet the paper does not state the asymptotic size of the generated formula when a sheet receives k copies of the same type. If the pairwise non-overlap clauses are still generated for every pair of copies that could share a sheet, the quadratic dependence on demand remains and must be quantified for the largest solved instances.

    Authors: The referee is correct that the non-overlap constraints remain pairwise, yielding Θ(k²) clauses for k copies assigned to one sheet. We have revised §4.2 to state the precise asymptotic size: with total demand D and S sheets the worst-case clause count is O(D²), while the conditional activation reduces the effective size to O((D/S)² · S) on average. For the largest solved instances we now report the concrete clause counts (all below 10⁶), which remain within the practical limits of modern SAT solvers. revision: yes

  3. Referee: [§3] §3 (Infeasible-orientation elimination): The rule that fixes rotation variables when only one orientation fits the sheet is presented as a preprocessing step, but it is unclear whether the rule is applied before encoding or encoded as unit clauses, and whether its application preserves the completeness of the optimality certificate when rotation is allowed. A short proof sketch or counter-example check would remove this ambiguity.

    Authors: The rule is applied as a preprocessing step before formula generation: for each item copy we test whether only one orientation fits the sheet dimensions and fix the corresponding Boolean variable. This is semantically equivalent to adding a unit clause. We have inserted a short proof sketch in §3 showing completeness: any placement that would have used the eliminated orientation necessarily violates the sheet width or height, so it cannot appear in any feasible (hence optimal) solution. We also verified the argument on a small hand-crafted instance with rotation permitted. revision: yes

Circularity Check

0 steps flagged

Direct SAT encoding of 2D-CSSP exhibits no circularity

full rationale

The paper presents a standard reduction of the two-dimensional single stock size cutting stock problem to SAT by expanding each item type according to its demand, introducing per-copy sheet-assignment variables, and activating non-overlap constraints only for copies assigned to the same sheet, together with an infeasible-orientation elimination rule. This encoding is a direct, non-self-referential translation whose validity rests on the semantics of SAT solvers rather than any internal fitting, parameter estimation, or self-citation chain. The three minimization approaches (non-incremental SAT with binary search, incremental SAT, and weighted partial MaxSAT) are compared empirically on the external Cui-Zhao benchmark; no derivation step reduces by construction to its own inputs, and the central claim of certifying more provably optimal instances is an observable performance difference, not a tautology.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that modern SAT solvers are sound and complete for the generated formulas and that the chosen benchmark suite adequately represents the problem class; no free parameters or new invented entities are introduced.

axioms (1)
  • standard math Soundness and completeness of the underlying SAT and MaxSAT solvers
    The entire framework delegates correctness to the external solver; any error in the solver would invalidate the optimality certificates.

pith-pipeline@v0.9.0 · 5500 in / 1265 out tokens · 57226 ms · 2026-05-13T21:32:00.959713+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    A computational study of LP-based heuristic algorithms for two-dimensional guillotine cutting stock problems,

    R. Alvarez-Vald´ es, A. Paraj´ on, and J. M. Tamarit, “A computational study of LP-based heuristic algorithms for two-dimensional guillotine cutting stock problems,”OR Spectrum, vol. 24, no. 2, pp. 179–192, 2002

    work page 2002

  2. [2]

    A tabu search algorithm for large-scale guillotine (un)constrained two-dimensional cutting problems,

    ——, “A tabu search algorithm for large-scale guillotine (un)constrained two-dimensional cutting problems,”Computers & Operations Research, vol. 29, no. 7, pp. 925–947, 2002

    work page 2002

  3. [3]

    Predicting learnt clauses quality in modern SAT solvers,

    G. Audemard and L. Simon, “Predicting learnt clauses quality in modern SAT solvers,” in Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI), 2009, pp. 399–404

    work page 2009

  4. [4]

    An analytical model for the container loading problem,

    C. S. Chen, S. M. Lee, and Q. S. Shen, “An analytical model for the container loading problem,” European Journal of Operational Research, vol. 80, no. 1, pp. 68–76, 1995

    work page 1995

  5. [5]

    Performance bounds for level-oriented two-dimensional packing algorithms,

    E. G. Coffman, Jr., M. R. Garey, and D. S. Johnson, “Performance bounds for level-oriented two-dimensional packing algorithms,”SIAM Journal on Computing, vol. 9, no. 4, pp. 808–826, 1980

    work page 1980

  6. [6]

    Heuristic for the rectangular two-dimensional single stock size cutting stock problem with two-staged patterns,

    Y. Cui and Z. Zhao, “Heuristic for the rectangular two-dimensional single stock size cutting stock problem with two-staged patterns,”European Journal of Operational Research, vol. 231, no. 1, pp. 20–30, 2013

    work page 2013

  7. [7]

    An extensible SAT-solver,

    N. E´ en and N. S¨ orensson, “An extensible SAT-solver,” inTheory and Applications of Satisfiability Testing (SAT), 2003, pp. 502–518

    work page 2003

  8. [8]

    Mathematical programming models for cutting-stock problems in the clothing industry,

    A. A. Farley, “Mathematical programming models for cutting-stock problems in the clothing industry,”Journal of the Operational Research Society, vol. 39, no. 1, pp. 41–53, 1988

    work page 1988

  9. [9]

    Models for the two-dimensional two-stage cutting stock problem with multiple stock size,

    F. Furini and E. Malaguti, “Models for the two-dimensional two-stage cutting stock problem with multiple stock size,”Computers & Operations Research, vol. 40, no. 8, pp. 1953–1962, 2013

    work page 1953

  10. [10]

    M. R. Garey and D. S. Johnson,Computers and Intractability: A Guide to the Theory of NP- Completeness. W. H. Freeman, 1979

    work page 1979

  11. [11]

    Multistage cutting stock problems of two and more dimen- sions,

    P. C. Gilmore and R. E. Gomory, “Multistage cutting stock problems of two and more dimen- sions,”Operations Research, vol. 13, no. 1, pp. 94–120, 1965

    work page 1965

  12. [12]

    OR-Tools – Google optimization tools (v9.10),

    Google, “OR-Tools – Google optimization tools (v9.10),” https://developers.google.com/ optimization, 2024

    work page 2024

  13. [13]

    Gurobi optimizer reference manual (v13.0),

    Gurobi Optimization, LLC, “Gurobi optimizer reference manual (v13.0),” https://www.gurobi. com, 2025

    work page 2025

  14. [14]

    Cutting stock problems and solution procedures,

    R. W. Haessler and P. E. Sweeney, “Cutting stock problems and solution procedures,”European Journal of Operational Research, vol. 54, no. 2, pp. 141–150, 1991

    work page 1991

  15. [15]

    Solving cutting stock problem using pattern generation method on 2-dimensional stock,

    I. Hasbiyati, I. Latifa, A. Rahman, A. Ahriyati, and M. D. H. Gamal, “Solving cutting stock problem using pattern generation method on 2-dimensional stock,”BAREKENG: Jurnal Ilmu Matematika dan Terapan, vol. 19, no. 1, pp. 303–318, 2025

    work page 2025

  16. [16]

    A hybrid metaheuristic for the 2D orthogonal cutting stock problem,

    K. He, Y. Huo, and R. Zhang, “A hybrid metaheuristic for the 2D orthogonal cutting stock problem,” in2009 International Conference on Machine Learning and Cybernetics, vol. 1, 2009, pp. 116–121. SOL VING THE 2D-CSSP WITH SAT AND MAXSAT17

    work page 2009

  17. [17]

    CPLEX optimization studio (v22.1.1),

    IBM, “CPLEX optimization studio (v22.1.1),” https://www.ibm.com/products/ ilog-cplex-optimization-studio, 2022

    work page 2022

  18. [18]

    Efficient cutting stock optimization strategies for the steel industry,

    C. Jariyavajeeet al., “Efficient cutting stock optimization strategies for the steel industry,” PLOS ONE, vol. 20, no. 3, p. e0319644, 2025

    work page 2025

  19. [19]

    Boosting branch-and-bound MaxSAT solvers with clause learning,

    C.-M. Li, Y. Xu, J. Coll, F. Many` a, D. Haixia, and M. Felip, “Boosting branch-and-bound MaxSAT solvers with clause learning,”Artificial Intelligence, vol. 290, p. 103392, 2021

    work page 2021

  20. [20]

    An innovative genetic algorithm for a multi- objective optimization of two-dimensional cutting-stock problem,

    A. Mellouli, R. Mellouli, and F. Masmoudi, “An innovative genetic algorithm for a multi- objective optimization of two-dimensional cutting-stock problem,”Applied Artificial Intelligence, vol. 33, no. 6, pp. 531–547, 2019

    work page 2019

  21. [21]

    TT-Open-WBO-Inc: an anytime MaxSAT solver entering MSE 2024,

    A. Nadel, “TT-Open-WBO-Inc: an anytime MaxSAT solver entering MSE 2024,” inMaxSAT Evaluation 2024, 2024

    work page 2024

  22. [22]

    The two-dimensional cutting stock problem with usable leftovers and uncertainty in demand,

    D. Nascimento, A. Cherri, J. Oliveira, and B. Oliveira, “The two-dimensional cutting stock problem with usable leftovers and uncertainty in demand,”Computers & Industrial Engineering, vol. 186, p. 109705, 2023

    work page 2023

  23. [23]

    Cutting stock optimization and integral production planning for centralized wood processing,

    M. P. Reinders, “Cutting stock optimization and integral production planning for centralized wood processing,”Mathematical and Computer Modelling, vol. 16, no. 1, pp. 37–55, 1992

    work page 1992

  24. [24]

    An integer programming model for two- and three- stage two-dimensional cutting stock problems,

    E. Silva, F. Alvelos, and J. M. V. Carvalho, “An integer programming model for two- and three- stage two-dimensional cutting stock problems,”European Journal of Operational Research, vol. 205, no. 3, pp. 699–708, 2010

    work page 2010

  25. [25]

    Integrating two-dimensional cutting stock and lot-sizing problems,

    ——, “Integrating two-dimensional cutting stock and lot-sizing problems,”Journal of the Oper- ational Research Society, vol. 65, no. 1, pp. 108–123, 2014

    work page 2014

  26. [26]

    A SAT-based method for solving the two-dimensional strip packing problem,

    T. Soh, K. Inoue, N. Tamura, M. Banbara, and H. Nabeshima, “A SAT-based method for solving the two-dimensional strip packing problem,”Fundamenta Informaticae, vol. 102, no. 3–4, pp. 467–487, 2010

    work page 2010

  27. [27]

    An exact algorithm for the N-sheet two dimensional single stock- size cutting stock problem,

    T. Steyn and J. M. Hattingh, “An exact algorithm for the N-sheet two dimensional single stock- size cutting stock problem,”ORiON, vol. 31, no. 2, pp. 77–94, 2015

    work page 2015

  28. [28]

    Compiling finite linear CSP into SAT,

    N. Tamura, A. Taga, S. Kitagawa, and M. Banbara, “Compiling finite linear CSP into SAT,” Constraints, vol. 14, no. 2, pp. 254–272, 2009

    work page 2009

  29. [29]

    SAT-based approaches for two-dimensional bin packing: A comprehensive comparison with MIP and CP methods,

    T. Van Kieu, C. L. Hoang, and K. Van To, “SAT-based approaches for two-dimensional bin packing: A comprehensive comparison with MIP and CP methods,” in2025 17th International Conference on Knowledge and System Engineering (KSE). IEEE, 2025, pp. 1–6

    work page 2025

  30. [30]

    Efficient SAT and MaxSAT techniques for solving the two-dimensional strip packing problem,

    T. Van Kieu, D. Quy Le, and K. Van To, “Efficient SAT and MaxSAT techniques for solving the two-dimensional strip packing problem,”Pesquisa Operacional, vol. 45, p. e297231, 2025

    work page 2025

  31. [31]

    A nested decomposition approach to a three-stage, two-dimensional cutting- stock problem,

    F. Vanderbeck, “A nested decomposition approach to a three-stage, two-dimensional cutting- stock problem,”Management Science, vol. 47, no. 6, pp. 864–879, 2001

    work page 2001

  32. [32]

    Best-first search methods for constrained two-dimensional cutting stock problems,

    K. V. Viswanathan and A. Bagchi, “Best-first search methods for constrained two-dimensional cutting stock problems,”Operations Research, vol. 41, no. 4, pp. 768–776, 1993

    work page 1993

  33. [33]

    Two-dimensional cutting stock problem with sequence dependent setup times,

    D. A. Wuttke and H. S. Heese, “Two-dimensional cutting stock problem with sequence dependent setup times,”European Journal of Operational Research, vol. 265, no. 1, pp. 303–315, 2018

    work page 2018