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

Tuyen Van Kieu; Chi Linh Hoang; Khanh Van To

cs.AIApr 2, 2026

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

Authors: Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Organizations: VNU University of Engineering and Technology, Hanoi, Vietnam

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.

Figures & tables

Panel of Figure 1 — Figure 1: A 2D-CSSP instance: sheet size $6{\times}4$ , two item types ( $t_{1}{:}\;3{\times}2$ , $d_{1}{=}3$ ; $t_{2}{:}\;2{\times}2$ , $d_{2}{=}3$ ), optimal packing on $k^{*}{=}2$ sheets. Hatched regions are waste.

Panel of Figure 2 — Figure 2: SB4: the left assignment ( $a_{1}{=}\text{false},a_{2}{=}\text{true}$ ) violates $\neg a_{2}\lor a_{1}$ and is eliminated; the right is the canonical labelling.

Config	#Opt	#Feas	Avg TTB (s)	Tot. Vars ( $\times 10^{3}$ )	Tot. Cls ( $\times 10^{6}$ )	Gap (%)
Non-Incremental SAT with Binary Search
CSP	15	3	59.1	485.0	171.6	10.55
CSP_SB	15	3	56.7	485.2	158.2	10.78
Incremental SAT with Binary Search
CSP_INC	15	3	42.6	489.2	209.6	10.55
CSP_INC_SB	16	3	105.9	489.2	192.9	9.71

Table 1: SAT/MaxSAT performance on the Cui–Zhao benchmark (no rotation). Best values per column are in bold .

Config	#Opt	#Feas	Avg TTB (s)	Tot. Vars ( $\times 10^{3}$ )	Tot. Cls ( $\times 10^{6}$ )	Gap (%)
Non-Incremental SAT with Binary Search
CSP_R	18	4	99.2	611.0	525.2	3.24
CSP_R_SB	18	4	162.0	611.4	536.2	3.24
Incremental SAT with Binary Search
CSP_INC_R	18	2	87.7	614.2	622.2	3.77
CSP_INC_R_SB	18	2	133.2	614.2	609.8	3.77

Table 2: SAT/MaxSAT performance on the Cui–Zhao benchmark (with rotation). Best values per column are in bold .

Config	#Opt	#Feas	Avg TTB (s)	Gap (%)
No Rotation
CSP_INC_SB	16	3	105.9	9.71
OR-TOOLS_CP_SB	7	8	139.1	12.03
GUROBI_MIP_SB	7	0	264.3	21.09
CPLEX_MIP_SB	7	0	264.5	21.27
OR-TOOLS_MIP_SB	5	1	46.3	22.11

Table 3: Best SAT/MaxSAT configurations vs. commercial solvers. Best values per block are in bold .

	CSP				CSP_SB				CSP_INC				CSP_INC_SB				CSP_MS				CSP_MS_SB
Instance	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB
		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)
2 (2)	2 ∗	3.0	0.09	0.3	2 ∗	3.0	0.08	0.6	2 ∗	3.0	0.09	0.3	2 ∗	3.0	0.08	0.3	2 ∗	3.0	0.09	0.2	2 ∗	3.0	0.08	0.2
3 (18)	24	12.5	4.5	–	24	12.5	3.5	–	24	12.7	5.4	–	24	12.7	4.3	–	24	12.9	5.6	–	24	12.9	4.4	–
A1 (17)	23	12.4	4.3	–	23	12.4	3.2	–	23	12.7	5.2	–	23	12.7	3.9	–	23	12.8	5.4	–	23	12.8	4.0	–
A2 (11)	11 †	9.8	2.0	32.2	11 †	9.8	1.7	29.9	11 †	9.9	2.4	16.7	11 †	9.9	2.0	43.9	12	10.0	2.5	–	12	10.0	2.0	–

Table 4: Per-instance results for SAT/MaxSAT configurations without rotation. ∗ = certified optimal; † = feasible matching BKS; unmarked = timeout. – denotes timeout (1 800 s).

	CSP_R				CSP_R_SB				CSP_INC_R				CSP_INC_R_SB				CSP_MS_R				CSP_MS_R_SB
Instance	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB	$k$	#Var	#Cls	TTB
		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)		( $10^{3}$ )	( $10^{6}$ )	(s)
2 (2)	2 ∗	3.6	0.2	0.7	2 ∗	3.6	0.2	0.8	2 ∗	3.6	0.2	0.8	2 ∗	3.6	0.2	0.7	2 ∗	3.6	0.2	0.3	2 ∗	3.6	0.2	0.5
3 (18)	19	15.6	15.1	–	19	15.6	15.2	–	19	15.6	16.1	–	19	15.6	12.6	–	19	15.6	16.1	–	19	15.6	12.6	–
A1 (17)	17 †	15.4	13.5	126	17 †	15.5	13.6	187	18	15.8	18.6	–	18	15.8	16.6	–	22	15.8	18.6	–	22	15.8	16.6	–
A2 (11)	11 †	12.5	6.7	83.6	11 †	12.5	6.7	82.9	11 †	12.6	8.1	42.6	11 †	12.6	8.1	34.8	12	12.6	8.1	–	12	12.6	8.1	–

Table 5: Per-instance results for SAT/MaxSAT configurations with rotation. ∗ = certified optimal; † = feasible matching BKS; unmarked = timeout. – denotes timeout (1 800 s).

	CPLEX CP				CPLEX MIP				GUROBI MIP				OR-TOOLS CP				OR-TOOLS MIP
	w/o R		w/ R		w/o R		w/ R		w/o R		w/ R		w/o R		w/ R		w/o R		w/ R
Instance	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB	$k$	TTB
		(s)		(s)		(s)		(s)		(s)		(s)		(s)		(s)		(s)		(s)
2 (2)	2 ∗	4.1	2 †	0.0	2 ∗	2.1	2 ∗	2.6	2 ∗	0.9	2 ∗	0.4	2 ∗	0.3	2 ∗	10.3	2 ∗	4.1	2 ∗	20.3
3 (18)	24	–	19	–	24	–	19	–	23	–	19	–	23	–	19	–	24	–	19	–
A1 (17)	23	–	22	–	23	–	22	–	23	–	23	–	23	–	17 †	107	23	–	18	–

Table 6: Per-instance results for commercial/OR solver configurations. ∗ = certified optimal; † = feasible matching BKS; unmarked = timeout. – denotes timeout (1 800 s).

Boolean Satisfiability

See all 22 papers

On inferring cumulative constraints
Feb 17, 2026Konstantin SidorovResource-Constrained Project Scheduling Constraint Programming
Faculty of Electrical Engineering, Mathematics & Computer Science, Delft University of Technology, Delft, The Netherlands
Solving Max-Cut to Global Optimality via Feasibility-Preserving Graph Neural Networks
May 8, 2026Hao Chen, Chendi Qian, Christopher Morris +2Max-Cut Semidefinite Programming
1Davidson School of Chemical Engineering, Purdue University · Faculty of Computer Science, RWTH Aachen University · 3Jacobs Technion-Cornell Institute, Cornell Tech
Graph Coarsening Enables Escaping Local Optima in Compute-Constrained Nonconvex MAX-CUT
Oct 13, 2026M. Harper Langston, Pierre-David Letourneau, Dalton Jones +7Max-Cut Combinatorial Optimization
Qualcomm AI Research

Feb 17, 2026J/K move · Enter open · S save

On inferring cumulative constraints

Konstantin Sidorov

Faculty of Electrical Engineering, Mathematics & Computer Science, Delft University of Technology, Delft, The Netherlands

Resource-Constrained Project Scheduling Constraint Programming Combinatorial Optimization Constraint Propagation

Open paper AskPDF arXiv

Cumulative constraints are central in scheduling with constraint programming, yet propagation is typically performed per constraint, missing multi-resource interactions and causing severe slowdowns on some benchmarks. I present a preprocessing method for inferring additional cumulative constraints that capture such interactions without search-time probing. This approach interprets cumulative constraints as linear inequalities over occupancy vectors and generates valid inequalities by (i) discovering covers, the sets of tasks that cannot run in parallel, (ii) strengthening the cover inequalities for the discovered sets with lifting, and (iii) injecting the resulting constraints back into the scheduling problem instance. Experiments on standard RCPSP and RCPSP/max test suites show that these inferred constraints improve search performance and tighten objective bounds on favorable instances, while incurring little degradation on unfavorable ones. Additionally, these experiments discover 25 new lower bounds and five new best solutions; eight of the lower bounds are obtained directly from the inferred constraints.

Abstract

Boolean Satisfiability

Explore similar work

On inferring cumulative constraints

Solving Max-Cut to Global Optimality via Feasibility-Preserving Graph Neural Networks

Graph Coarsening Enables Escaping Local Optima in Compute-Constrained Nonconvex MAX-CUT