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

Feb 17, 2026

On inferring cumulative constraints

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.

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

Ask PDF

May 8, 2026

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

Exact solution of hard combinatorial optimization problems often relies on strong convex relaxations, but solving these relaxations repeatedly inside a branch-and-bound algorithm can be prohibitively expensive. Hence, we consider this challenge for Max-Cut, where branch and bound commonly uses semidefinite programming (SDP) relaxations to bound subproblems. We propose a Max-Cut-specific graph neural network that serves as a principled, lightweight neural proxy for these SDP solvers and can be plugged directly into an exact branch-and-bound framework. The proposed architecture has update steps of complexity

\mathcal{O}(n^2 + ne)

, and predicts both primal- and dual-feasible SDP solutions. The primal SDP solutions yield feasible Max-Cut solutions via the Goemans--Williamson algorithm. In addition, it is trained in a self-supervised fashion without requiring solved SDP relaxations as labels. Empirically, we show that our architecture can substantially reduce the cost of bounding in exact Max-Cut solving by up to

10.6 \times

compared with using the state-of-the-art SDP solver Mosek. Our work highlights the potential of learned, validity-preserving surrogates for accelerating exact optimization over structured convex relaxations.

Hao Chen, Chendi Qian, Christopher Morris +2

1Davidson School of Chemical Engineering, Purdue University · Faculty of Computer Science, RWTH Aachen University · 3Jacobs Technion-Cornell Institute, Cornell Tech

Max-Cut Semidefinite Programming Graph Neural Networks Branch and Bound Combinatorial Optimization Global Optimization+2

Ask PDF

Oct 13, 2026

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

Because its binary optimization landscape contains exponentially many local optima, MAX-CUT is highly sensitive to initialization. We study Particle Polynomial Relaxation (PPR), a moment-based nonconvex continuous reformulation possessing an advantageous optimization landscape. We warm-start PPR with Combinatorial Multigrid (CMG), a spectral graph-coarsening method that produces structure-aware initial solutions in near-linear time without training data. On t2g20 (

n=400

), benchmark instance with known exact optimum, the combined CMG+PPR pipeline reaches

97.5\%

of optimum on average and

98.4\%

on the best run. An extended variant with discrete local-search refinement reaches the published optimum on all sixty Biq Mac instances evaluated by a recent neural branch-and-bound method. Using a sparse CSR representation, the same approach scales to G-set instances with up to

20{,}000

vertices reducing memory requirements by up to

3333\times

while maintaining a consistent improvement over the CMG warm start. Gains are largest on sparse weighted graphs; on dense graphs we complement the pipeline with spectral sparsification.

M. Harper Langston, Pierre-David Letourneau, Dalton Jones +7

Qualcomm AI Research

Max-Cut Combinatorial Optimization Nonconvex Optimization

Ask PDF

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