用局部约束提升折叠盒枚举效率，大幅扩展可计算规模。
Unfolding Boxes with Local Constraints
- 将全局约束转为易传播的局部约束，改进SAT求解器性能。
- 可处理面积超150的双盒共用展开图，远超此前88的上限。
- 首次实现面积60内三盒共用展开图的完整枚举，推翻旧猜想。
我们研究如何寻找并枚举能折叠成多个非同构盒子的多连方图形。尽管已有基于SAT、随机算法和决策图的方法，但均难以规模化。现有SAT编码受限于全局约束（如图连通性或无环性），难以有效编码且求解困难。本文提出一种新SAT方法，用简单局部约束替代全局约束，显著改善传播性能。该方法大幅提升共用展开图的计算与枚举能力：(i) 前人仅能处理面积至88的双盒共用展开，本方法轻松扩展至150以上；(ii) 前人仅能枚举面积30以内的双盒共用展开，本方法扩展至60。由此可排除46、54、58作为三盒共用展开最小面积，推翻Xu等（2017）的猜想。
原文摘要 · Abstract (English)
We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been proposed, including SAT, randomized algorithms, and decision diagrams, none has been able to perform at scale. We argue that existing SAT encodings are hindered by the presence of global constraints (e.g., graph connectivity or acyclicity), which are generally hard to encode effectively and hard for solvers to reason about. In this work, we propose a new SAT-based approach that replaces these global constraints with simple local constraints that have substantially better propagation properties. Our approach dramatically improves the scalability of both computing and enumerating common box unfoldings: (i) while previous approaches could only find common unfoldings of two boxes up to area 88, ours easily scales beyond 150, and (ii) while previous approaches were only able to enumerate common unfoldings up to area 30, ours scales up to 60. This allows us to rule out 46, 54, and 58 as the smallest areas allowing a common unfolding of three boxes, thereby refuting a conjecture of Xu et al. (2017).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。