Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: RCRA 2008 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
Article type: Research Article
Authors: Soh, Takehide | Inoue, Katsumi | Tamura, Naoyuki | Banbara, Mutsunori | Nabeshima, Hidetomo
Affiliations: Department of Informatics, Graduate University for Advanced Studies, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan. soh@nii.ac.jp | Principles of Informatics Division, National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan. ki@nii.ac.jp | 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. nabesima@yamanashi.ac.jp
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
DOI: 10.3233/FI-2010-314
Journal: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 467-487, 2010
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl