💻 computer science

Solving the Two-dimensional single stock size Cuting Stock Problem with SAT and MaxSAT

本文提出了一种基于 SAT 和 MaxSAT 的框架来解决二维单规格切割下料问题，通过引入需求展开、非重叠约束激活及不可行方向消除规则，在 Cui-Zhao 基准测试中显著优于 OR-Tools、CPLEX 和 Gurobi，能够证明更多实例的最优性并降低最优性间隙。

原作者： Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

发布于 2026-04-03

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文讲述了一个非常贴近生活的难题：如何用最少的原材料（比如钢板、玻璃或布料），把一堆不同大小的矩形零件完美地切割出来，同时保证不浪费。

想象一下，你是一家家具厂的老板，手里有一堆巨大的矩形木板（这就是“原材料”），你需要从中切出各种尺寸的桌面、椅腿和抽屉面板。你的目标很明确：切出来的废料越少越好，用的木板张数越少越好。

在数学上，这被称为“二维单尺寸切割库存问题”（2D-CSSP）。听起来简单，但当你要切几百个零件，而且每种零件都要切好几个（比如 3 个桌面、5 个椅腿）时，这就变成了一个让超级计算机都头疼的“迷宫”。

这篇论文的作者（来自越南河内）提出了一套新的“解题秘籍”，他们利用了一种叫做 SAT（布尔可满足性） 的计算机逻辑技术，把这个问题变成了一个“逻辑谜题”来解。

以下是用通俗语言和比喻对论文核心内容的解读：

1. 核心挑战：为什么这个问题这么难？

这就好比你要把一堆形状各异的积木塞进几个盒子里。

普通版（2D-BPP）： 每个积木只有一个，只要塞进去就行。
困难版（本文的 2D-CSSP）： 每种积木都有很多个（比如 20 个一样的小方块）。这就产生了两个大麻烦：
1. 数量爆炸： 20 个一样的积木，排列组合的可能性是天文数字。
2. 对称性： 如果你把第 1 个积木和第 2 个积木的位置互换，结果是一模一样的。计算机如果不懂这一点，就会在两个完全一样的解法上浪费大量时间，就像你在迷宫里反复走同一条死胡同。

2. 作者的“魔法武器”：SAT 逻辑引擎

作者没有使用传统的数学规划方法（像 CPLEX 或 Gurobi 这些商业软件常用的方法），而是把问题转化成了逻辑判断题。

比喻： 想象你在玩一个巨大的“填字游戏”或者“逻辑推理游戏”。
- 每个零件的位置、旋转角度、放在哪张板子上，都变成了一个“是”或“否”的开关（0 或 1）。
- 规则变成了逻辑语句：“如果零件 A 和零件 B 在同一张板上，那么它们绝对不能重叠。”
- 计算机（SAT 求解器）就像一个超级侦探，它通过不断的试错和逻辑推理，迅速排除掉所有“不可能”的情况，直到找到那个完美的布局。

3. 三大创新点（他们的独门绝技）

A. “按需复制”与“条件约束”

以前的方法在处理大量重复零件时，会把所有零件都当成独立的个体，导致公式大得吓人。

新做法： 作者让计算机“按需分配”。只有当两个零件被分配到同一张板材上时，才去检查它们是否重叠。如果它们在不同的板上，计算机就自动忽略它们之间的冲突检查。
比喻： 就像学校排座位。如果两个学生坐在不同的教室里，你根本不需要担心他们会不会撞在一起；只有当他们被分到了同一个教室，你才需要检查他们的桌子会不会打架。这大大减少了计算机需要处理的“废话”。

B. “智能旋转”规则

有些零件如果横着放就放不进板子，竖着放才行。

新做法： 作者加了一条规则：如果某个零件只有一种方向能塞进板子，计算机就直接把它“锁死”在那个方向，不再浪费时间尝试另一种不可能的方向。
比喻： 就像你往门里塞一个大箱子，如果横着塞不进去，你就不用再试横着塞了，直接决定“必须竖着塞”。这省去了很多无谓的尝试。

C. 三种“解题策略”的比拼

为了找到最少需要几张板子，作者测试了三种不同的搜索策略：

二分搜索（非增量）： 像猜数字游戏。先猜中间数，不行就猜一半，再不行就猜四分之三。每次猜完都重新开始。
- 适用场景： 当零件可以旋转，问题变得非常复杂时，这种“从头再来”的方法反而更灵活。
增量搜索（Incremental SAT）： 像“滚雪球”。第一次猜需要 5 张板子，失败了，计算机记住了“为什么 5 张不够”的原因（比如“三个大零件挤不下一张板”）。第二次猜 6 张时，它直接利用上次记住的教训，不用重新推导。
- 适用场景： 当零件不能旋转，问题结构比较紧凑时，这种“吸取教训”的方法效率极高，比从头开始快得多。
MaxSAT（最大满足）： 试图一次性算出最优解，而不是猜。
- 结果： 在这个问题上，它表现不如前两种策略，有点像“想一口吃成个胖子”，反而容易消化不良。

4. 战绩如何？（实验结果）

作者用了一组包含 30 个复杂案例的“考卷”（Cui-Zhao 基准测试），并让他们的 SAT 方法与目前世界上最强的商业软件（如 Google OR-Tools, IBM CPLEX, Gurobi）进行 PK。

结果惊人：
- 证明最优解的能力： 商业软件通常只能证明 1 到 7 个案例是最优的（即证明“这确实是最省材料的方案，没有更好的了”）。而作者的 SAT 方法证明了 16 到 18 个 案例是最优的！是商业软件的 2 到 3 倍。
- 节省程度： 即使在没有证明“绝对最优”的情况下，SAT 方法找到的方案也比商业软件更节省材料（差距更小）。
- 特别发现： 商业软件（特别是 OR-Tools）经常能找到很好的方案，但无法证明这是最好的方案。而 SAT 方法不仅能找到好方案，还能像法官一样给出“这是绝对最优”的铁证。

5. 总结与启示

这篇论文告诉我们，在处理这种复杂的工业切割问题时，逻辑推理（SAT） 可能比传统的数学优化方法更强大。

核心启示： 面对复杂的排列组合问题，不要试图用蛮力去算所有可能。要学会利用逻辑规则（比如“如果不在同一张板上就不检查”）来剪枝，并且要根据问题的具体情况（能不能旋转）灵活选择搜索策略。
比喻： 以前的方法像是在迷宫里拿着手电筒漫无目的地乱撞；而这篇论文的方法像是给迷宫装上了智能导航，不仅知道哪里是死胡同，还能记住走过的路，甚至能直接画出最短路径。

这项研究不仅能让工厂节省大量的原材料（省钱、环保），也为未来解决更复杂的制造调度问题提供了新的思路。作者甚至把代码开源了，让全世界的研究者都能来使用这个“超级切割助手”。

1. 问题背景 (Problem Definition)

二维单规格切割库存问题 (2D-CSSP) 是制造业中的核心任务，旨在从相同尺寸的原材料（如钢板、玻璃、布料）上切割出多种矩形物品，以满足特定需求数量，同时最小化使用的原材料张数（即最小化浪费）。

输入： $n$ 种物品类型，每种类型 $t$ 具有尺寸 $(w_t, h_t)$ 和需求数量 $d_t$ ；原材料尺寸为 $W \times H$ 。
目标：将所有 $N = \sum d_t$ 个物品副本分配到 $k$ 张板材上，确保无重叠且位于板材边界内，并最小化 $k$ 。
难点：
- 该问题是 NP-hard 问题（当 $d_t=1$ 时退化为二维装箱问题 2D-BPP）。
- 需求带来的组合爆炸：当需求 $d_t$ 较大时，物品副本数量激增，导致搜索空间呈乘积级增长。
- 现有方法的局限：
  - 精确方法（如列生成、MIP）：在处理大需求时扩展性差，变量数量随需求线性甚至指数级增加。
  - 启发式方法：能处理大规模实例，但无法提供最优性证明。
  - 商业求解器（CP/MIP）：在中等规模实例上往往无法在合理时间内证明最优性。

2. 方法论 (Methodology)

作者提出了一种基于 布尔可满足性 (SAT) 和 最大可满足性 (MaxSAT) 的框架，这是首个针对 2D-CSSP 的声明式逻辑编码方案。

2.1 SAT 编码策略

编码的核心在于处理“需求”带来的对称性和条件约束：

变量定义：
- 板材分配： $s_{c,j}$ 表示物品副本 $c$ 是否分配给第 $j$ 张板材。
- 位置编码：采用顺序编码 (Order Encoding) 表示坐标 $(x_c, y_c)$ ，将整数变量转化为线性数量的布尔变量，保持编码紧凑。
- 旋转： $r_c$ 表示是否旋转 90 度。
核心约束：
- 条件非重叠约束 (Conditional Non-overlap)：这是本文的关键创新。非重叠约束仅在两个副本被分配到同一张板材时才被激活。
  - 公式逻辑： $\neg s_{c,j} \lor \neg s_{c',j} \lor \text{no-overlap}(c, c')$ 。
  - 这避免了不同板材上的物品之间产生不必要的几何约束，显著减少了子句数量。
- 边界约束：确保物品在分配的板材内。
对称性破缺 (Symmetry Breaking)：
- 大物品约束：若两个物品在任何方向组合下都无法并排，则强制其相对位置。
- 同尺寸物品排序：对于同一类型的多个副本，强制按索引顺序排列，打破 $d_t!$ 的排列对称性。
- 不可行方向消除：如果某种旋转方向无法放入板材，则通过单位子句固定旋转变量。
- 板材排序：强制板材按索引顺序使用（第 1 张满后再用第 2 张），消除 $k!$ 的板材重标号对称性。

2.2 求解策略

为了最小化板材数量 $k$ ，作者比较了三种策略：

非增量 SAT + 二分搜索：每次测试中间值 $m$ 时重新构建公式。
增量 SAT + 二分搜索：构建最大可能板材数 $UB$ 的公式，通过假设（Assumptions）禁用多余的板材。
- 优势：在 $k-1$ 次尝试中学习的冲突子句（Conflict Clauses）可以保留并用于 $k$ 次尝试，特别适用于需求结构导致的几何冲突。
加权部分 MaxSAT：将目标函数（最小化使用板材数）编码为软子句，单次调用求解器直接优化。

3. 主要贡献 (Key Contributions)

首个 2D-CSSP 的 SAT 编码：提出了基于需求扩展的编码层，实现了基于板材分配的条件非重叠约束，解决了传统装箱问题编码无法处理的“多副本”对称性问题。
不可行方向消除规则：推广了现有的正方形物品固定规则，提出了一种通用的规则：当且仅当一种旋转方向能放入板材时，强制固定旋转变量。
增量 SAT 与需求结构的交互研究：首次系统研究了增量 SAT 在处理具有大量相同物品副本的问题时的表现，发现冲突子句在需求副本间具有高度的可复用性。
大规模基准测试与对比：在 Cui-Zhao 基准套件（30 个实例）上，将 SAT 方法与 OR-Tools、CPLEX、Gurobi 等工业级求解器进行了全面对比。

4. 实验结果 (Experimental Results)

实验在 Cui-Zhao 基准套件上进行（30 个实例，需求 1-45，板材尺寸 100x100 至 4000x3000），时间限制为 1800 秒。

4.1 性能对比

最优性证明能力：
- 无旋转场景：增量 SAT（带对称性破缺）证明了 16 个实例的最优性，是商业求解器（最佳为 7 个）的 2 倍以上。
- 有旋转场景：非增量 SAT 证明了 18 个实例的最优性，是商业求解器（最佳为 6 个）的 3 倍。
最优性间隙 (Gap)：
- SAT 方法的平均间隙显著低于商业求解器。
- 无旋转最佳间隙：9.71% (SAT) vs 12.03% (OR-Tools)。
- 有旋转最佳间隙：3.24% (SAT) vs 4.63% (OR-Tools)。
商业求解器表现：
- OR-Tools CP 经常能找到与已知最优解 (BKS) 匹配的解，但往往无法证明其最优性。
- MIP 求解器（CPLEX, Gurobi）虽然找到解的速度较快，但在证明最优性和缩小间隙方面表现较差。

4.2 策略选择分析

无旋转时：增量 SAT 表现最佳。因为相同物品的副本产生了几何上相同的子问题，在 $k-1$ 次失败尝试中学习的冲突子句（如“某类宽物品无法共存”）在 $k$ 次尝试中依然有效，极大地剪枝了搜索空间。
有旋转时：非增量 SAT 表现略优或持平。旋转引入了额外的变量，导致子句数量激增（约 3 倍），使得增量 SAT 中保留的大量子句变得冗余，稀释了学习到的知识。此时，每次重新构建公式（非增量）反而更有效。

5. 意义与结论 (Significance & Conclusion)

理论突破：证明了基于 CDCL（冲突驱动子句学习）的 SAT 求解器在处理具有强对称性和大规模需求的二维切割问题时，比传统的 MIP 和 CP 方法更具优势。SAT 引擎能够自动推导出几何冲突并跨迭代复用，这是其他精确方法难以做到的。
实际应用价值：该方法不仅能提供高质量的解，还能提供严格的最优性证明，这对于高价值材料（如航空航天、精密玻璃）的切割排样至关重要。
未来方向：包括结合列生成（用 SAT 解决定价子问题）、 tighter 的下界推导以及扩展到异质板材尺寸问题。

总结：本文通过创新的 SAT 编码和增量求解策略，在二维单规格切割库存问题上取得了超越当前工业界主流求解器的性能，特别是在证明最优性方面展现了显著优势。