A SAT-based Method for Solving the Two-dimensional Strip Packing Problem

被引：13

作者：

Soh, Takehide ^{[1
]}

Inoue, Katsumi ^{[1
,2
]}

Tamura, Naoyuki ^{[3
]}

Banbara, Mutsunori ^{[3
]}

Nabeshima, Hidetomo ^{[4
]}

机构：

[1] Grad Univ Adv Studies, Dept Informat, Chiyoda Ku, Tokyo 1018430, Japan

[2] Natl Inst Informat, Principles Informat Div, Chiyoda Ku, Tokyo 1018430, Japan

[3] Kobe Univ, Informat Sci & Technol Ctr, Nada Ku, Kobe, Hyogo 6578501, Japan

[4] Univ Yamanashi, Interdisciplinary Grad Sch Med & Engn, Kofu, Yamanashi 4008511, Japan

来源：

FUNDAMENTA INFORMATICAE | 2010年 / 102卷 / 3-4期

关键词：

Boolean satisfiability; Strip packing problem; SAT encoding; Constraint satisfaction problem; SEARCH ALGORITHM; GRASP;

D O I：

10.3233/FI-2010-314

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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 overlapping, into the strip by minimizing the overall height of the packing. Although the 2SPP has been studied in Operations Research, some instances are still hard to solve. Our method solves the 2SPP by translating it into a SAT problem through a SAT encoding called order encoding. The translated SAT problems tend to be large; thus, we apply several techniques to reduce the search space by symmetry breaking and positional 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 thus reuse learned clauses and assumptions from the previously solved SAT problems. To evaluate our approach, we obtained results for 38 instances from the literature and made comparisons with a constraint satisfaction solver and an ad-hoc 2SPP solver.

引用

页码：467 / 487

页数：21