Affiliations: Department of Informatics, Graduate University for Advanced Studies, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan. [email protected] | Principles of Informatics Division, National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan. [email protected] | Information Science and Technology Center, Kobe University, 1-1 Rokkodai-cho, Nada-ku, Kobe 657-8501, Japan. {tamura, banbara}@kobe-u.ac.jp | Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi, 4-3-11, Takeda, Kofu 400-8511, Japan. [email protected]
Note: [] Address for correspondence: Department of Informatics, Graduate University for Advanced Studies, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan
Note: [] Also works: Department of Informatics, Graduate University for Advanced Studies, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo, 101-8430, Japan
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 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.
Keywords: Boolean satisfiability, Strip packing problem, SAT encoding, Constraint satisfaction problem
