=Paper=
{{Paper
|id=Vol-451/paper-12
|storemode=property
|title=A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
|pdfUrl=https://ceur-ws.org/Vol-451/paper16soh.pdf
|volume=Vol-451
|dblpUrl=https://dblp.org/rec/conf/rcra/SohITBN08
}}
==A SAT-based Method for Solving the Two-dimensional Strip Packing Problem==
https://ceur-ws.org/Vol-451/paper16soh.pdf
A SAT-based Method for Solving the
Two-dimensional Strip Packing Problem
Takehide Soh1 , Katsumi Inoue12 , Naoyuki Tamura3 , Mutsunori Banbara3 ,
and Hidetomo Nabeshima4
1
Department of Informatics, Graduate University for Advanced Studies,
soh@nii.ac.jp
2
National Institute of Informatics, ki@nii.ac.jp
3
Kobe University, {tamura, banbara}@kobe-u.ac.jp
4
University of Yamanashi, nabesima@yamanashi.ac.jp
Abstract
We propose a satisfiability testing (SAT) based exact approach
for solving the two-dimensional strip packing problem (2SPP). In this
problem, we are given a set of rectangles and one large rectangle called
a strip. The goal of the problem is to pack all rectangles without over-
lap, into the strip by minimizing the overall height of the packing. We
show the method solves a 2SPP by translating it to SAT problems
through a SAT encoding called order encoding. Generated SAT prob-
lems tend to be large, then we show techniques to reduce the search
space by utilizing symmetries and relations of rectangles. To solve a
2SPP, that is, to compute the minimum height of a 2SPP, we need to
repeatedly solve similar SAT problems. We then reuse learned clauses,
assumptions, and models, which are obtained from previously solved
SAT problems, to efficiently compute the minimum height. We at-
tempt to solve 38 instances from the literature and obtain the total of
29 optimal solutions, including the solutions of two open problems.
1 Introduction
Packing problems have many practical applications such as truck loading,
LSI layouts and assignments of newspaper articles. There has been a great
deal of research on these problems, for example, knapsack problems and bin
packing problems. In this paper, we consider a satisfiability testing (SAT)
based exact approach for solving the two-dimensional strip packing problem.
(2SPP) [2]. This problem is NP-hard in the strong sense because the one-
dimensional bin packing problem which is strongly NP-hard can easily be
transformed into a 2SPP [8].
The input of the 2SPP is a set R = {r1 , . . . , rn } of n rectangles. Each
rectangle has a width wi and a height hi . We are also given a large rectangle,
called a strip, of width W . The goal is to pack all rectangles without overlap
into the strip by minimizing the height H. Although rectangles are allowed
Proceedings of the 15th International RCRA workshop (RCRA 2008):
Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
Udine, Italy, 12–13 December 2008
to be rotated by 90 degrees in the general case of the 2SPP, we assume that
rectangles cannot be rotated according to convention of previous research [1,
4, 13, 19]. Furthermore, we assume that only integer values are allowed for
wi , hi , W, and H.
The 2SPP has been well studied in the last decade. There are two types
of methods to solve the 2SPP: the exact method and the incomplete method.
The exact method can get the optimal solution of the problem. Martello et
al. solve relatively small 38 instances and obtained 27 optimal solutions [13].
The incomplete method cannot prove the optimality of the solution, i.e., the
obtained minimum height H. The method can only confirm the solution
as optimum provided that the solution corresponds to the lower bound of
the problem. The method can pack over thousand rectangles with keeping
quality of solutions [1, 4, 15, 19]. Although both types of methods have
been well studied, it is difficult to reach the optimal height even so small
problems that have up to 200 rectangles as inputs.
For the problem, we propose a SAT-based method for solving the 2SPP.
Recent advance of SAT technologies has been tremendous. Many SAT
solvers have been developed and solve SAT problems. Most state-of-the-
art solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) al-
gorithm [5] and use a clause learning technique [12]. With this technique,
SAT solvers generate learned clauses when a conflict is reached and avoid en-
countering the same conflict in the later search. These techniques make SAT
solvers applicable to huge problems which have over millions of clauses. The
main advantage of using SAT solvers is that it make possible to use several
SAT techniques.
In order to solve the 2SPP with a SAT solver, we represent the prob-
lem as a constraint satisfaction problem (CSP) and solve the CSP as a SAT
problem through a SAT encoding called order encoding [16]. The feature
of the encoding is that a CSP comparison x ≤ a is encoded into a Boolean
variable and it enable a compact encoding for the 2SPP. However, generated
SAT problems have to grow with the number of input rectangles. Then we
propose techniques to reduce the search space. These techniques utilize sym-
metries and relations of rectangles. To reach the optimal solution, we have
to repeatedly solve similar sub-problems. For solving these problems effi-
ciently, we reuse learned clauses generated from previously solved problem.
We also reuse assumptions and models which are obtained from previously
solved sub-problems. In computational experiments, we evaluate techniques
to reduce the search space and attempted to solve 38 instances from the
literature [13].
The remainder of the paper is organized as follows. Section 2 provides
a necessarily brief perspective on the 2SPP and related concepts. Section 3
describes how to encode the 2SPP into SAT problems. Section 4 explains
how to solve the optimal height of a 2SPP and several techniques to solve
problems efficiently. Section 5 shows computational results. Section 6 dis-
2
cusses related works. Finally, Section 7 concludes the paper.
2 Preliminaries
In this section, we give preliminaries to take a SAT-based approach to the
2SPP. In the following, N denotes the set of natural numbers and Z denotes
the set of integers.
2.1 2SPP and 2OPP
We consider a SAT-based approach to the two-dimensional strip packing
problem (2SPP). Although we want to obtain the optimal height of a 2SPP,
SAT solvers can only determine the satisfiability of a given problem. We thus
approach to the 2SPP by solving a sequence of two-dimensional orthogonal
packing problems (2OPPs), which are decision problems of the 2SPP with
a fixed height of the strip. We give more details of this method in Section
4.1. Here, we define the 2SPP and the 2OPP as follows [2].
Two-dimensional strip packing problem (2SPP)
Input. A set R = {r1 , . . . , rn } of n rectangles. Each rectangle ri ∈ R has a
width wi and a height hi (wi , hi ∈ N). A Strip of width W ∈ N.
Constraints. Each rectangle cannot overlap with the others and the edges
of the strip and parallel to the horizontal and the vertical axis.
Question. What is the minimum height such that the set of rectangles can
be packed in the given strip?
Two-dimensional orthogonal packing problem (2OPP)
Input. A set R = {r1 , . . . , rn } of n rectangles. Each rectangle ri ∈ R has
width wi and height hi (wi , hi ∈ N). A Strip of width W and height H
(W, H ∈ N).
Constraints. Each rectangle cannot overlap with the others and the edges
of the strip and parallel to the horizontal and the vertical axis.
Question. Can the set of rectangles be packed in the given strip?
2.2 CSP formulation of 2OPP
We now represent the 2OPP as a constraint satisfaction problem (CSP). A
CSP is a triple hV, D, Ci, where V is a finite subset of integer variables, D
is a function which maps every variable in V to a subset of Z. We use D(x)
as the subset of Z mapped from x ∈ V and call the set D(x) the domain of
x. C is a finite set of constraints over a subset of variables in V .
3
The CSP formulation of the 2OPP is as follows. Let xi and yi be integer
variables such that the pair (xi , yi ) of variables represents the position of
lower left coordinates of the rectangle ri in the strip. The domains of xi and
yi are as follows.
D(xi ) = {a ∈ N | 0 ≤ a ≤ W − wi }
(1)
D(yi ) = {a ∈ N | 0 ≤ a ≤ H − hi }
These domains represent possible values of the coordinates of the rectangle
ri and guarantee that ri must not overlap with edges of the strip. For each
pair of rectangles ri and rj (1 ≤ i < j ≤ n), we associate the non-overlapping
constraints.
(xi + wi ≤ xj ) ∨ (xj + wj ≤ xi ) ∨ (yi + hi ≤ yj ) ∨ (yj + hj ≤ yi ) (2)
2.3 Order Encoding
There have been several studies on translation methods which encode a
CSP into a SAT problem, e.g., direct encoding, log encoding [18], support
encoding [10] and log support encoding [9]. Among them, order encoding [16]
aims to make a more natural explanation of the order relation of integers. In
order encoding, there are two encoding steps. Let x be an integer variable,
and c be an integer value. At the first step, a constraint with comparison is
translated into primitive comparisons which are in the form of x ≤ c. At the
next step, a primitive comparison is encoded into a Boolean variable px,c .
Due to space limitation, we illustrate the encoding method with a simple
constraint x1 + 1 ≤ x2 (x1 , x2 ∈ {0, 1, 2, 3}). This constraint is encoded into
the set of primitive comparisons as follows:
¬(x2 ≤ 0), (x1 ≤ 0) ∨ ¬(x2 ≤ 1), (x1 ≤ 1) ∨ ¬(x2 ≤ 2), (x1 ≤ 2)
Then, these constraints are translated into the following formula of a SAT
problem:
¬px2,0 , px1,0 ∨ ¬px2,1 , px1,1 ∨ ¬px2,2 , px1,2
where pxi,c denotes xi ≤ c for a simple expression. In order encoding, the
following axiom clauses are also added:
¬px1,0 ∨ px1,1 , ¬px1,1 ∨ px1,2 , ¬px2,0 ∨ px2,1 , ¬px2,1 ∨ px2,2
3 From 2OPP into SAT Problems
In this section, we explain how to translate a 2OPP into a SAT problem
with order encoding. Let ri , rj ∈ R (i 6= j) be two rectangles in a 2OPP.
Let e and f be any integer. Then, the SAT encoding of a 2OPP uses four
4
y y
r1 r2 3 3
r4
(w4, h4) = (1, 1),
2 2
(x4, y4) = (3, 2) r3
r3 r4 1 1 r2 r1
r4
0 1 2 3 x 0 1 2 3 x
Input rectangles Strip (W=4, H=4)
a. Example of 2SPP b. One placement of 2SPP
Figure 1: Example of a 2SPP
kinds of atoms, lri,j , udi,j , pxi,e , and pyi,f . lri,j is true if ri are placed at
the left to the rj . udi,j is true if ri are placed at the downward to the rj .
pxi,e is true if ri are placed at less than or equal to e. pyi,f is true if ri are
placed at less than or equal to f . Then, inputs and constraints of a 2OPP
can be encoded into a SAT problem as follows.
For each rectangle ri , and integer e and f such that 0 ≤ e < W − wi and
0 ≤ f < H − hi , we have the 2-literal axiom clauses due to order encoding,
¬pxi,e ∨ pxi,e+1
(3)
¬pyi,f ∨ pyi,f +1
For each rectangles ri , rj (i < j), we have the following 4-literal clauses as
the non-overlapping constraints (2):
lri,j ∨ lrj,i ∨ udi,j ∨ udj,i (4)
For each rectangles ri , rj (i < j), and integer e and f such that 0 ≤ e <
W − wi and 0 ≤ f < H − hj , we also have the following 3-literal clauses as
the non-overlapping constraints (2):
¬lri,j ∨ pxi,e ∨ ¬pxj,e+wi
¬lrj,i ∨ pxj,e ∨ ¬pxi,e+wj
(5)
¬udi,j ∨ pyi,f ∨ ¬pyj,f +hi
¬udj,i ∨ pyj,f ∨ ¬pyi,f +hj
Example. Consider the simple example of 2OPP shown in Figure 1a.
We are given four rectangles (w1 , h1 ) = (1, 2), (w2 , h2 ) = (1, 2), (w3 , h3 ) =
(2, 1), (w4 , h4 ) = (1, 1) and a strip (W, H) = (4, 4). We obtain the SAT-
encoded 2OPP shown in Figure 2. This SAT problem is satisfiable and the
figure of packed rectangles corresponding to a model is shown in Fig. 1b.
In this case, Boolean variables of the SAT problem are assigned as follows.
px1,0 = F, px1,1 = T, px2,0 = T, px3,1 = F, px3,2 = T, px4,1 = F, px4,2 = T
py1,0 = T, py2,0 = T, py3,0 = F, py3,1 = T, py4,0 = T
5
Variables
px1,0 , . . . , px1,3 py1,0 , . . . , py1,3 px2,0 , . . . , px2,2 py2,0 , . . . , py2,3
px3,0 , . . . , px3,3 py3,0 , . . . , py3,2 px4,0 , . . . , px4,3 py4,0 , py4,1
Order Constraint (3)
¬px1,0 ∨ px1,1 , ¬px1,1 ∨ px1,2 , ¬px1,2 ∨ px1,3
..
.
¬py4,0 ∨ py4,1 , ¬py4,1 ∨ py4,2 , ¬py4,2 ∨ py4,3
Non-overlapping Constraint (4), (5)
lr1,2 ∨ lr2,1 ∨ ud1,2 ∨ ud2,1
..
.
lr3,4 ∨ lr4,3 ∨ ud3,4 ∨ ud4,3
¬lr1,2 ∨ ¬px2,0 ¬lr1,2 ∨ px1,0 ∨ ¬px2,1 ¬lr1,2 ∨ px1,1 ∨ ¬px2,2 ¬lr1,2 ∨ px1,2
..
.
¬ud3,4 ∨ ¬py3,0 ¬ud3,4 ∨ py4,0 ∨ ¬py3,1 ¬ud3,4 ∨ py4,1 ∨ ¬py3,2 ¬ud3,4 ∨ py4,2
Figure 2: Example of SAT-encoded 2OPP
These assignments are converted into the following assignments of the 2OPP:
x1 = 1, x2 = 0, x3 = 2, x4 = 2
y1 = 0, y2 = 0, y3 = 1, y4 = 0
4 Solving 2SPP with a SAT Solver
In Section 3, we explained how to translate a 2OPP into a SAT problem. In
this section, we show how to compute the optimal height of a 2SPP with a
SAT solver by repeatedly solving SAT-encoded 2OPP problems.
4.1 Searching Optimum Height of 2SPP
Let ub and lb be upper and lower bounds of a solution of a 2SPP, respectively.
In practice, the lower bound is given by exact methods and the upper bound
is given by either exact or incomplete methods. Let o be an integer value
such that lb ≤ o ≤ ub−1. We introduce a new Boolean variable pho which is
true if all rectangles are packed at the downward to the height o. Then, to
solve a 2SPP, for each rectangle ri , and a height o such that lb ≤ o ≤ ub − 1,
we have the 2-literal clauses:
¬pho ∨ pyi,o−hi (6)
Furthermore, for each o (lb ≤ o ≤ ub − 1), we have the 2-literal clauses due
to order encoding:
¬pho ∨ pho+1 (7)
6
Let Ψ be the set of clauses consisting of all clauses obtained from (3),
(4), (5), (6) and (7). Then, we can decide the satisfiability of a 2OPP with
the height H by solving the set of clauses1 :
Ψ ∪ {phH } (8)
Note that Ψ is common in all 2OPPs associated with a 2SPP.
The optimal height of a 2SPP can be obtained by repeatedly solving
SAT-encoded 2OPPs. The bisection method, as used in previous studies [11,
14], is useful for efficiently finding the optimal height. First, we set the
lower and upper bounds. Then we solve the height which is at the half of
the region. If we obtain the satisfiability of the 2OPP, then upper bound
updated by the height, or if we obtain the unsatisfiability of the 2OPP, then
lower bound updated by the height. We execute these operations repeatedly
until the optimal height, which is the boundary between the satisfiable and
unsatisfiable problems, is obtained. For example, let us consider the 2SPP
which has the optimal height 140. To compute the optimal height, suppose
that the lower bound is 48 and that the upper bound is 393. Then the height
would change as: 48 (UNSAT), 393 (SAT), 221 (SAT), 134 (UNSAT), 178 (SAT),
157 (SAT),. . . . The solution area becomes more and more constrained until
the optimal height is obtained.
4.2 Reducing Techniques
Now, we propose techniques which enhance the SAT-based approach. Sup-
posing that W = H, the size of clauses of a SAT-encoded 2OPP are O(n2 ),
where n is the number of rectangles. Generated SAT problems have to grow
with the number of input rectangles. We thus propose four techniques to
reduce the search space. We give evaluation of these techniques in Section
5.
Domain reduction. To prune the search space, we reduce the domain of
the maximum rectangle defined by wm and hm with symmetry (see Figure 3).
There are three cases wherein maximum means maximum width, maximum
height, or maximum area. We choose the maximum width and obtain a new
domain for the maximum rectangle in the horizontal direction:
W − wm
D(xm ) = {a ∈ N | 0 ≤ a ≤ b c}
2
Figure 3. shows the original D(rm ) with dots and reduced one with circles,
that is, the domain D(xm ) becomes from {0, 1, 2, 3} to {0, 1}.
1
That is, we use phH to restrict the upper bound of y-coordinate of each rectangle
instead of restricting the domain of each rectangle that was defined in Section 2.2.
7
rj
rm
ri
rm
a. Overlap in Horizontal Direction
a. Original b. Point Symmetry
ri
rm
rm rm
c. Reflective Symmetry d. Reflective Symmetry
b. Overlap with Large Rectangular
( horizontal ) ( vertical )
Figure 3: Domain Removal Figure 4: Overlap Condition
W − wm
By applying this reduction, if wi satisfies wi > b c, we can assign
2
lri,m = f alse, that is, we can remove literals lri,m and the clauses including
¬lri,m from the SAT problem. In Figure 4b, we can see that the ri , which
has wi = 2, cannot be packed to the left to rm . This reduction is also
available in the vertical direction.
Large Rectangles. If we are given large rectangles ri and rj which satisfy
wi + wj > W , we can assign lri,j = f alse and lrj,i = f alse by using a size
relation of the pair of rectangles. Thereby, we can remove literals lri,j , lrj,i
and the clauses including either ¬lri,j or ¬lrj,i from the SAT problem. The
condition wi + wj > W means we cannot pack rectangles ri and rj in the
horizontal direction (see Fig. 4a). This reduction technique is also available
in the vertical direction.
Same Rectangles. If we are given rectangles ri and rj which have the
same dimension (wi , hi ) = (wj , hj ), we can fix the positional relation of
rectangles. Thereby, we can assign lrj,i = f alse and add lri,j ∨ ¬udj,i .
One Pair of Rectangles. We can fix the positional relation between only
one pair of rectangles. See Figure 4, by using symmetry, we can restrict the
positional relation between ri and rj . Hereby, we can assign lrj,i = f alse and
udj,i = f alse. Note that, this technique cannot use with domain reduction
simultaneously.
8
4.3 Reusing Clauses for Incremental Solving
To solve the 2SPP, we use Minisat [6] which is the one of the state-of-
the-art solvers. Minisat is based on the DPLL algorithm. On the ba-
sis of DPLL, Minisat efficiently implements conflict learning [12]. When
the current assignment leads to a conflict, a new clause indicating the
incompatible assignment is generated as a learned clauses. For example,
when (x1 , x2 , x3 ) = (true, true, f alse) is the source of a conflict, the clause
¬(x1 ∧ x2 ∧ ¬x3 ) = ¬x1 ∨ ¬x2 ∨ x3 is generated. Such a learned clause is
utilized to prevent the solver from retrying the same portion of assignments.
Note that all learned clauses can be deduced from the initial set of clauses.
Our SAT encoding approach generates a sequence of SAT problems.
These SAT problems are similar to each other, that is, Po+1 includes Po
except for some clauses. This kind of problem is called an incremental SAT
problem [7]. Now we propose methods to reuse learned clauses, assumptions,
and models for solving incremental SAT problems efficiently.
Learning Clauses. Nabeshima et.al. [14] show the effectiveness of reusing
learned clauses for solving a job-shop scheduling problem. Eén and Sörensson
also report a similar technique in solving incremental SAT [7]. To solve an
incremental SAT problem efficiently, we here use their technique to reuse
learned clauses for solving the 2SPP as follows. Let P and Q be SAT
problems such that “all non-unit clauses of P are included in Q” (lemma-
reusability condition). Then by the lemma-reusability theorem by [14], the
set S of all learned clauses generated in solving P can be used to solve Q.
That is, instead of solving Q, we can solve Q ∪ S, which results in pruning
a large portion of the search space in many cases. In solving a 2SPP, two
2OPPs in the form (8) differ only in their unit clauses phH , which satisfies
the lemma-reusability condition above. By this way, we can reuse learned
clauses produced in solving previous 2OPPs in subsequent 2OPPs.
Reusing Assumptions. In Section 4.1, we show how to decide the sat-
isfiability at any height of 2SPP, and we need to add unit clause phH to
the problem. If Ψ ∪ {phH } is unsatisfied, we cannot continue the bisection
method without removing phH from the problem.
To resolve this issue, Eén and Sörensson proposed a particular set of a
unit clauses called assumptions [7]. An assumption is added before solving
the problem, and then removed from the problem. Adding phH as an as-
sumption, we can do bisection method until the optimal height is obtained.
To solve incremental SAT efficiently, we propose to reuse assumptions.
Generally, we solve the problems which are the conjunction of Ψ and at
most one phH . Using our method, we can reuse assumptions to next sub-
problems in bisection method. For example, let Ψ be an encoded 2SPP with
lb = 4, ub = 10 and the optimal height 6. First we give Ψ and {ph7 } as an
9
y y y
r3
3 3 3
r4 r3
2 2 2
r4 r3
1 r2 r1 1 r2 r1 1 r2 r1
r4
0 1 2 3 x 0 1 2 3 x 0 1 2 3 x
a. H=4 b. H=3 c. H=2
Figure 5: Reusing Models
assumption to the solver and it returns SAT. Now we reuse assumptions by
adding {ph7 } to Ψ. Next the SAT solver is given Ψ ∪ {ph7 } and {ph5 } as an
assumption, and returns UNSAT. Finally, the SAT solver is given Ψ ∪ {ph7 } ∪
{¬ph5 } and {ph6 } as an assumption, and returns SAT. Using this way, we
avoid redundant search space.
Reusing Models. When a SAT-encoded 2OPP is satisfiable, a SAT solver
outputs a model which represents a placement of all rectangles within a
given height H. In solving a 2SPP, a part of the previously obtained model
might correspond to a model of next sub-problem. Let us consider a simple
example of a 2SPP which has the optimal height H = 2. Suppose that we
found a model of the 2OPP with H = 4 as that shown in Figure 5a. This
model partially corresponds to a model with H = 3 because the two models
share the truth assignment that lr2,1 = true, lr1,4 = true, ud4,3 = true.
We thus propose to reuse a partial model to solve the next sub-problem
efficiently. A SAT solver assigns either true or f alse to a variable chosen
by some heuristic if there is no unit clause, for example, Minisat [6] tries to
assign f alse to such a decision variable preferentially. On the other hand,
our proposed method assigns a decision variable the value which is found in
a model of a previous satisfiable problem. By this reusing method, we can
help the decision making of a SAT solver.
5 Experimental Results
The presented methods are run on a Xeon 2.6GHz with 2GB of memory
within 3600 seconds and we use Minisat 2.0 [6] as a SAT solver. We use the
benchmark set and those lower bounds shown in the literature by Martello et
al. [13]: HT01-HT09, BENG01-BENG10, CGCUT01-CGCUT03, GCUT01-
GCUT04, and NGCUT01-NGCUT12. All 38 instances are available at
“DEIS - Operations Research Group Library of Instances” [17]. These
benchmark sets include some problems which are very hard to solve. In
10
Table 1: Number of Solved Optimal Values with Reducing Techniques
Instance normal domain large same pair
HT01-09 7 9 7 8 8
CGCUT01-03 1 1 1 1 1
GCUT01-04 2 2 2 2 2
NGCUT01-12 12 12 12 12 12
BENG01-10 2 2 2 4 2
Total # of Opt. 24 26 24 27 25
Table 2: Comparison with previous studies
Instance Proposed method Optimum or best known value
Incomp. Exact.
Name n W LB normal C1 C2 Prop.
[1, 15, 19] [13]
HT01(c1p1) 16 20 20 20 20 20 op [1, 15] op op
HT02(c1p2) 17 20 20 20 20 20 op [1, 15] op op
HT03(c1p3) 16 20 20 20 20 20 op [1, 15] op op
HT04(c2p1) 25 40 15 15 15 15 op [1, 15] op op
HT05(c2p2) 25 40 15 15 15 15 op [1, 15] op op
HT06(c2p3) 25 40 15 15 15 15 op [1, 15] op op
HT07(c3p1) 28 60 30 31 30 30 op [1] 31 op
HT08(c3p2) 29 60 30 31 31 30 31 [1, 15] 31 op
HT09(c3p3) 28 60 30 30 30 30 op [1, 15] op op
CGCUT01 16 10 23 23 23 23 op [1, 15, 19] op op
CGCUT02 23 70 63 67 67 65 65 [1, 15, 19] 67 65
CGCUT03 62 70 636 671 671 671 658 [15] 670 671
GCUT01 10 250 1016 1016 1016 1016 op [1, 15, 19] op op
GCUT02 20 250 1133 1196 1196 1196 1187 [15] 1208 1196
GCUT03 30 250 1803 1803 1803 1803 op [1, 15, 19] op op
GCUT04 50 250 2934 3056 3056 3056 3002 [1] 3077 3056
NGCUT01 10 10 23 23 23 23 op [1, 15, 19] op op
NGCUT02 17 10 30 30 30 30 op [1, 15, 19] op op
NGCUT03 21 10 28 28 28 28 op [1, 15, 19] op op
NGCUT04 7 10 20 20 20 20 op [1, 15, 19] op op
NGCUT05 14 10 36 36 36 36 op [1, 15, 19] op op
NGCUT06 15 10 31 31 31 31 op [1, 15, 19] op op
NGCUT07 8 20 20 20 20 20 op [1, 15, 19] op op
NGCUT08 13 20 33 33 33 33 op [1, 15] op op
NGCUT09 18 20 49 50 50 50 50 [1, 15, 19] 50 op
NGCUT10 13 30 80 80 80 80 op [1, 15, 19] op op
NGCUT11 15 30 50 52 52 52 op [1, 15] op op
NGCUT12 22 30 79 87 87 87 op [1, 15, 19] op op
BENG01 20 25 30 30 30 30 op [1, 15, 19] op op
BENG02 40 25 57 58 57 57 op [1, 15] 58 op
BENG03 60 25 84 85 84 85 op [1, 15, 19] 85 op
BENG04 80 25 107 108 108 108 op [1, 15, 19] 108 108
BENG05 100 25 134 135 134 134 op [1, 15, 19] op op
BENG06 40 40 36 36 36 36 op [1, 15, 19] 37 op
BENG07 80 40 67 68 68 68 op [1, 15, 19] op 68
BENG08 120 40 101 102 102 102 op [1, 15, 19] op 102
BENG09 160 40 126 130 130 130 op [1, 15, 19] op 130
BENG10 200 40 156 158 158 158 op [1, 15, 19] op 158
Total # of Opt. 24 28 28 32 27 29
11
particular, HT08, CGCUT02, 03, GCUT02, 04, NGCUT09 are still open.
We evaluate the reducing techniques shown in Section 4.2. Table 1 shows
the number of solved optimal values with each reducing technique. normal
represents the method without reducing techniques. domain represents a do-
main reduction technique. large represents a reduction technique with large
rectangles. same represents a reduction technique with same rectangles.
pair represents a reduction technique with the one pair of rectangles. Table
1 shows that same computes the largest number of optimal values. Fur-
thermore, all techniques compute the instance group “NGCUT” completely.
This means that all these techniques can close open problem NGCUT09.
To compute problems more efficiently, we combine reducing and reusing
techniques. Table 2 shows a comparison with our combined methods with
previous methods. Due to space limitation, we show top two of 36 combina-
tions that we tried. Columns 1–4 show the characteristics of each instance
such as the instance name, the number of input rectangles, the strip width
W , and lower bounds from the literature [13]. Columns 5–7 show the best
value obtained by the normal method and the top two combined methods.
“C1” denotes results of the following combination: reducing with domain,
large and same, reusing learned clauses and assumptions. “C2” denotes re-
sults of the following combination: reducing with large and pair, reusing
learned clauses and assumptions. Columns 8–10 show a comparison with
previous methods. “Incomp.” describes the best value by incomplete meth-
ods from the literature [1, 15, 19]. All of those methods are reported recently
in 2008. “Exact.” describes the best value by Martello et al. [13]. “Prop.”
describes the best value by our methods. “op” denotes that the method
obtain the optimal value.
Table 1, 2 show effectiveness of our proposed methods. Our SAT-based
method with no reducing and no reducing techniques, can solve 24 optimums
including the one open problem. Moreover, the combined methods can solve
28 optimums and close the open problem HT08. Table 2 also shows that our
exact methods are competitive with the state-of-the-art incomplete methods.
As a result, our methods compute a optimal solution of the instance HT08
(see Figure 7) and proves the optimum of NGCUT09 to be 50. In other
words, we prove that the height of 49 has no solution in NGCUT09.
6 Discussion
There are a few report of methods which solve an optimization problem
through encoding which translates a problem to decision problems. Bekrar
et al. [3] reported an approach to the two-dimensional guillotine strip pack-
ing problem which is a variant of the 2SPP. They represent the problem as
CSPs and solve the optimum with bisection method. The difference from
our work is that they directly solve CSPs. On the other hand, we propose
12
6 6
5 5
4 x x x
ri 4 ri
3 x x x 3
2 x x x 2
1 1
0 1 2 3 4 5 6 0 1 2 3 4 5 6
a. Direct Encoding b. Order Encoding
Figure 6: Representation of Conflicts Figure 7: New Solution of HT08
the SAT-based method for the 2SPP. Thereby we can apply several incre-
mental SAT techniques and use the state-of-the-art SAT solver that have
been widely studied. There are several works on a SAT-based method for
other optimization problems. Inoue et al. [11] propose “Multisat” which
can execute several SAT solvers in parallel and apply Multisat to SAT plan-
ning and the job-shop scheduling problem. The solvers included in Multisat
exchange lemmas derived by conflict analysis among different SAT solvers
for solving the problems efficiently. Nabeshima et al. [14] report another
approach to the problems. Their method shares a learned clauses between
sub-problems. Our SAT-based approach enhances these works with reusing
assumptions and models, along with reusing learned clauses and is newly
applied to the 2SPP.
In our method, we use the order encoding as a SAT encoding. How-
ever, there have been well studied about SAT encoding. Here, we consider
a difference between direct encoding and order encoding. Let (wi , hi ) =
(2, 2), (wj , hj ) = (2, 2) and place ri at (xi , yi ) = (3, 3) (see Figure 6). We
can represent overlap constraint of CSP between ri and rj as follows:
(xj ≤ 1) ∨ (xj ≥ 5) ∨ (yj ≤ 1) ∨ (yj ≥ 5)
To see difference between order encoding and the others, we compare
the SAT clauses encoded with direct encoding [18] and those with order
encoding. In the direct encoding, we assign to a SAT variable as pxa = true
if and only if the CSP variable x has the domain value a, and constraints
are encoded to conflict clauses. The encoded clauses are as follows:
CSP : (xj ≤ 1) ∨ (xj ≥ 5) ∨ (yj ≤ 1) ∨ (yj ≥ 5)
SAT (direct) : ¬pxj 2 ∨ ¬pyj 2 ¬pxj 2 ∨ ¬pyj 3 ¬pxj 2 ∨ ¬pyj 4
¬pxj 3 ∨ ¬pyj 2 ¬pxj 3 ∨ ¬pyj 3 ¬pxj 3 ∨ ¬pyj 4
¬pxj 4 ∨ ¬pyj 2 ¬pxj 4 ∨ ¬pyj 3 ¬pxj 4 ∨ ¬pyj 4
SAT (order) : pxj 1 ∨ ¬pxj 4 ∨ pyj 1 ∨ ¬pyj 4
In direct encoding, constraints are represented as conflict points (see
Figure 6a). On the other hand, order encoding represents constraints as
13
a conflict region (see Figure 6b). This indicates SAT-based approach with
order encoding is suitable not only 2SPP but also geometric problems such
as shop scheduling problem.
7 Conclusion
We presented a SAT-based exact method to solve the two-dimensional strip
packing problem. Our method solves the problem through order encoding
and the bisection method. As far as the authors know, this is the first article
that solves the 2SPP with a SAT solver. Our approach solved two open
problems in 2SPP. This indicates that, while SAT-based approaches have
been widely studied, there is still remaining challenging problems, especially
OR problems like 2SPP.
There are several important future topics. Comparing other SAT-encoding
methods is important to evaluate the effect of the order encoding. It is also
interesting to compare this method with CSP solvers. Consideration of rota-
tion of input rectangles and applying to other packing problems are worth-
while. There is a possibility that a hybrid system which includes incomplete
methods as well as exact methods to solve larger problems.
Acknowledgments
This work was supported in part by Grant-in-Aid for Scientific Research
No.20240003 in Japan Society for the Promotion of Science and the Joint
Research Project funded by National Institute of Informatics in Japan. We
would like to thank Ateet Bhalla and Koji Iwanuma for their kind suggestion
and comments.
References
[1] R. Alvarez-Valdés, F. Parreno, and J. M. Tamarit. Reactive GRASP
for the strip-packing problem. Computers and Operations Research,
35(4):1065–1083, 2008.
[2] B. S. Baker, E. G. Coffman Jr., and R. L. Rivest. Orthogonal packings
in two dimensions. SIAM Journal of Computing, 9(4):846–855, 1980.
[3] A. Bekrar, I. Kacem, C. Chu, and C. Sadfi. A dichotomical algorithm
for solving the 2D guillotine strip packing problem. In Proceedings of
CIE’07, pages 1216–1224, 2007.
[4] E. K. Burke, G. Kendall, and G. Whitwell. A new placement heuris-
tic for the orthogonal stock-cutting problem. Operations Research,
52(4):655–671, 2004.
14
[5] M. Davis, G. Logemann, and D. Loveland. A machine program for
theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
[6] N. Eén and N. Sörensson. An extensible SAT-solver. In SAT, volume
2919 of LNCS, pages 502–518, 2003.
[7] N. Eén and N. Sörensson. Temporal induction by incremental SAT
solving. Electronic Notes in Theoretical Computer Science, 89(4):543–
560, 2003.
[8] M. R. Garey and D. S. Johnson, editors. Computers and Intractability:
A Guide to the Theory of NP-Completeness. FREEMAN, 1979.
[9] M. Gavanelli. The log-support encoding of CSP into SAT. In Proceed-
ings of CP’07, volume 4741 of LNCS, pages 815–822. 2007.
[10] I. P. Gent. Arc consistency in SAT. In Proceedings of ECAI’02, pages
121–125, 2002.
[11] K. Inoue, T. Soh, S. Ueda, Y. Sasaura, M. Banbara, and N. Tamura.
A competitive and cooperative approach to propositional satisfiability.
Discrete Applied Mathematics, 154(16):2291–2306, 2006.
[12] J. P. Marques-Silva and K. A. Sakallah. GRASP—A search algo-
rithm for propositional satisfiability. IEEE Transactions on Computers,
48(5):506–521, 1999.
[13] S. Martello, M. Monaci, and D. Vigo. An exact approach to the strip-
packing problem. Journal on Computing, 15(3):310–319, 2003.
[14] H. Nabeshima, T. Soh, K. Inoue, and K. Iwanuma. Lemma reusing for
sat based planning and scheduling. In Proceedings of ICAPS’06, pages
103–112, June 2006.
[15] B. Neveu and G. Trombettoni. Strip packing based on local search and
a randomized Best-Fit. In Workshop on BPPC’08, May 2008.
[16] N. Tamura, A. Taga, S. Kitagawa, and M. Banbara. Compiling finite
linear CSP into SAT. In Proceedings of CP’06, volume 4204 of LNCS,
pages 590–603. 2006.
[17] http://www.or.deis.unibo.it/research_pages/ORinstances.htm.
[18] T. Walsh. SAT v CSP. In Proceedings of CP’02, volume 1894 of LNCS,
pages 441–456. 2000.
[19] L. Wei, D. Zhang, and Q. Chen. A least wasted first heuristic algo-
rithm for the rectangular packing problem. Computers and Operations
Research, 2008.
15