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

• Autorzy: Soh T. , Tamura N. , Banbara M. , Inouey K. , Nabeshima H.
• Języki publikacji: EN

Abstrakty

EN

We propose a satisfiability testing (SAT) based exact approach for solving the twodimensional 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.

Słowa kluczowe

EN

Boolean satisfiability; strip packing problem; SAT encoding; constraint satisfaction problems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 3/4
• Strony: 467--487
• Opis fizyczny: Bibliogr. 55 poz., tab., wykr.

Twórcy

autor

Soh T.

autor

Tamura N.

autor

Banbara M.

autor

Inouey K.

autor

Nabeshima H.

• Department of Informatics, Graduate University for Advanced Studies, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan,

Bibliografia

• [1] Alvarez-Valdes, R., Parreno, F., Tamarit, J. M.: A branch and bound algorithm for the strip packing problem, OR Spectrum, 31(2), 2008, 431-459.
• [2] Alvarez-Valdes, R., Parreno, F., Tamarit, J. M.: Reactive GRASP for the strip-packing problem, Computers and Operations Research, 35(4), 2008, 1065-1083.
• [3] Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints, Principles and Practice of Constraint Programming (CP'03), 2003.
• [4] Bailleux, O., Boufkhad, Y.: Full CNF Encoding: The Counting Constraints Case, Proceedings of SAT, 2004.
• [5] Bailleux, O., Boufkhad, Y., Roussel, O.: A Translation of Pseudo Boolean Constraints to SAT, Journal on Satisfiability, Boolean Modeling and Computation, 2, 2006, 191-200.
• [6] Baker, B. S., Coffman Jr., E. G., Rivest, R. L.: Orthogonal Packings in Two Dimensions, SIAM Journal of Computing, 9(4), 1980, 846-855.
• [7] Beasley, J. E.: Algorithms for Unconstrained Two-Dimensional Guillotine Cutting, The Journal of the Operational Research Society, 36(4), 1985, 297-306.
• [8] Beasley, J. E.: An Exact Two-Dimensional Non-Guillotine Cutting Tree Search Procedure, Operations Research, 33(1), 1985, 49-64.
• [9] Bekrar, A., Kacem, I., Chu, C., Sadfi, C.: A Dichotomical Algorithm for Solving the 2D Guillotine Strip Packing Problem, Proceedings of the 37th International Conference on Computers and Industrial Engineering, 2007.
• [10] Bengtsson, B.: Packing Rectangular Pieces - A Heuristic Approach, Computer Journal, 25(3), 1982, 353-357.
• [11] Burke, E. K., Kendall, G., Whitwell, G.: A New Placement Heuristic for the Orthogonal Stock-Cutting Problem, Oper. Res., 52(4), 2004, 655-671.
• [12] Christofides, N., Whitlock, C.: An Algorithm for Two-Dimensional Cutting Problems, Operations Research, 25(1), 1977, 30-44.
• [13] Claessen, K., Sörensson, N.: New Techniques that Improve MACE-style Finite Model Finding, Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003.
• [14] Cravo, G. L., Ribeiro, G. M., Lorena, L. A. N.: A greedy randomized adaptive search procedure for the point-feature cartographic label placement, Computers and Geosciences, 34(4), 2008, 373-386.
• [15] Crawford, J. M., Baker, A. B.: Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems, Proceedings of the Twelfth National Conference on Artificial Intelligence, 1994.
• [16] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving, Communications of the ACM, 5(7), 1962, 394-397.
• [17] DEIS - Operations Research Group Library of Instances, http://www.or.deis.unibo.it/research_pages/ORinstances.htm.
• [18] Dyckhoff, H.: A typology of cutting and packing problems, European Journal of Operational Research, 44(2), January 1990, 145-159.
• [19] Eén, N., Sörensson, N.: An Extensible SAT-solver, Proceedings of SAT, 2919, Springer, 2003.
• [20] Eén, N., Sörensson, N.: Temporal Induction by Incremental SAT Solving, Electronic Notes in Theoretical Computer Science, 89(4), 2003, 543-560.
• [21] Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation, 2, 2006, 1-26.
• [22] Fey, G., Warode, T., Drechsler, R.: Reusing Learned Information in SAT-based ATPG, Proceedings of the 20th International Conference on VLSI Design held jointly with 6th International Conference (VLSID '07), IEEE Computer Society, 2007.
• [23] Garey, M. R., Johnson, D. S., Eds.: Computers and Intractability: A Guide to the Theory of NPCompleteness, W. H. FREEMAN AND COMPANY, NY, USA, 1979.
• [24] Gavanelli, M.: The Log-Support Encoding of CSP into SAT, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP'07), 4741, Springer, 2007.
• [25] Gent, I. P.: Arc Consistency in SAT, Proceedings of the 15th European Conference on Artificial Intelligence (ECAI), IOS Press, 2002.
• [26] Gomes, C., Kautz, H., Sabharwal, A., Selman, B.: Handbook of Knowledge Representation, chapter Satisfiability Solvers, Elsevier, 2008, 89-134.
• [27] Hebrard, E.: Mistral, a Constraint Satisfaction Library, Proceedings of the Third International CSP Solver Competition, 2008.
• [28] Hochbaum, D. S., Maass, W.: Approximation schemes for covering and packing problems in image processing and VLSI, Journal of the ACM, 32(1), 1985, 130-136.
• [29] Hopper, E., Turton, R.: An Empirical Investigation of Meta-heuristic and Heuristic algorithms for a 2D packing problem, European Journal of Operational Research, 128, 2000, 34-57.
• [30] Huang, J.: The Effect of Restarts on the Efficiency of Clause Learning, Proceedings of IJCAI, 2007.
• [31] Inoue, K., Soh, T., Ueda, S., Sasaura, Y., Banbara, M., Tamura, N.: A competitive and cooperative approach to propositional satisfiability, Discrete Applied Mathematics, 154(16), 2006, 2291-2306.
• [32] Jussien, N., Prud'homme, C., Cambazard, H., Rochart, G., Laburthe, F.: choco: an open source Java Constraint Programming Library, Proceedings of the Third International CSP Solver Competition, 2008.
• [33] Lecoutre, C., Tabary, S.: Abscon 112 Toward more Robustness, Proceedings of the Third International CSP Solver Competition, 2008.
• [34] Lee, C.-C., Jiang, J.-H. R., Huang, C.-Y. R., Mishchenko, A.: Scalable exploration of functional dependency by interpolation and incremental SAT solving, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design (ICCAD '07), IEEE Press, 2007.
• [35] Lodi, A., Martello, S., Monaci, M.: Two-dimensional packing problems: A survey, European Journal of Operational Research, 141(2), 2002, 241-252.
• [36] Marques-Silva, J. P., Sakallah, K. A.: GRASP-A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, 48(5), 1999, 506-521.
• [37] Marques-Silva, J. P., Sakallah, K. A., Algoritmos, G., Algos, O. S.: Robust search algorithms for test pattern generation, Proceedings of the Fault-Tolerant Computing Symposium, 1997.
• [38] Martello, S., Monaci, M., Vigo, D.: An Exact Approach to the Strip-Packing Problem, INFORMS Journal on Computing, 15(3), 2003, 310-319.
• [39] Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver, Proceedings of DAC, 2001.
• [40] Nabeshima, H., Nozawa, H., Iwanuma, K.: Effective SAT Planning by Lemma-Reusing, Proceedings of the IASTED International Conference on Artificial Intelligence and Applications (AIA2005), 2003.
• [41] Nabeshima, H., Soh, T., Inoue, K., Iwanuma, K.: Lemma Reusing for SAT based Planning and Scheduling, Proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS'06), 2006.
• [42] Neveu, B., Trombettoni, G.: Strip Packing Based on Local Search and a Randomized Best-Fit, Proceedings of Workshop on Bin Packing and Placement Constraints (BPPC'08), 5 2008.
• [43] O'Mahony, E., Hebrard, E., Holland, A., Nugent, C., O'Sullivan, B.: Using Case-based Reasoning in an Algorithm Portfolio for Constraint Solving, Proceedings of the 19th Conference on Artificial Intelligence and Cognitive Science, 2008.
• [44] Prestwich, S. D.: Local Search on SAT-encoded Colouring Problems, Proceedings of SAT'03, Springer, 2003.
• [45] Pureza, V., Morabito, R.: Some experiments with a simple tabu search algorithm for the manufacturer's pallet loading problem, Computers and Operations Research, 33(3), 2006, 804-819.
• [46] Shtrichman, O.: Pruning Techniques for the SAT-Based Bounded Model Checking Problem, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME '01), LNCS, Springer, 2001.
• [47] Guerra e Silva, L., Silveira, L. M., Marques-Silva, J.: Algorithms for solving Boolean satisfiability in combinational circuits, Proceedings of the Conference on Design, Automation and Test in Europe (DATE '99), ACM, 1999.
• [48] Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints, Proceedings of the Principles and Practice of Constraint Programming (CP'05), 2005.
• [49] Soh, T., Inoue, K., Naoyuki, T., Mutsunori, B., Nabeshima, H.: A SAT-based Method for Solving the Twodimensional Strip Packing Problem, Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 451, CEUR, 2008.
• [50] Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT, Constraints, 14(2), 2009, 254-272.
• [51] Third International CSP Solver Competition, http://cpai.ucc.ie/08/.
• [52] Walsh, T.: SAT v CSP, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP'02), 1894, Springer, 2000.
• [53] Warners, J. P.: A linear-time transformation of linear inequalities into conjunctive normal form, Information Processing Letters, 68(2), 1998, 63-69.
• [54] Wei, L., Zhang, D., Chen, Q.: A least wasted first heuristic algorithm for the rectangular packing problem, Computers and Operations Research, 36(5), 2009, 1608-1614.
• [55] Whittemore, J., Kim, J., Sakallah, K.: SATIRE: a new incremental satisfiability engine, Proceedings of the 38th Conference on Design Automation (DAC '01), ACM, 2001.