A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
复制标题
DOI：
10.3233/fi-2010-314
复制
发表时间：
2010-08
期刊：
影响因子：
--
通讯作者：
Takehide Soh;Katsumi Inoue;Naoyuki Tamura;Mutsunori Banbara;Hidetomo Nabeshima
中科院分区：
文献类型：
--
作者：
Takehide Soh;Katsumi Inoue;Naoyuki Tamura;Mutsunori Banbara;Hidetomo Nabeshima
提出了一种基于可满足性检验（SAT）的二维带排样问题（2SPP）的精确求解方法。在这个问题中，我们给出了一组矩形和一个称为条带的大矩形。问题的目标是通过最小化包装的总高度将所有矩形无重叠地包装成条带。尽管运筹学对2SPP进行了研究，但仍有一些问题难以解决。我们的方法解决了2SPP通过SAT编码称为顺序编码将其转化为SAT问题。翻译SAT问题往往是大的，因此，我们采用几种技术，以减少搜索空间的对称性破缺和位置关系的矩形。为了求解2SPP，即计算2SPP的最小高度，我们需要重复求解类似的SAT问题。因此，我们重新使用从以前解决的SAT问题的学习条款和假设。为了评估我们的方法，我们从文献中获得了38个实例的结果，并与约束满足求解器和ad-hoc 2SPP求解器进行了比较。
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.