Unfolding Boxes with Local Constraints

TL;DR

This paper introduces a new SAT-based method with local constraints for efficiently finding and enumerating polyomino unfoldings into boxes, significantly improving scalability over previous approaches.

Contribution

It replaces global constraints with local ones in SAT encodings, enabling scalable enumeration of polyomino unfoldings and refuting a prior conjecture.

Findings

Scales beyond area 150 for common unfoldings of two boxes

Enumerates common unfoldings up to area 60, surpassing previous limits

Refutes the conjecture on minimal areas for three-box unfoldings

Abstract

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).