Unfolding Boxes with Local Constraints

Bernardo Subercaseaux; Eric Wang; Long Qian; Marijn J. H. Heule

REVIEW 3 major objections 4 minor 12 references

Unfolding Boxes with Local Constraints

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read No three boxes of area 58 or less share one common unfolding net.

desk verdict Refutes a 2017 conjecture with a clever local-constraint SAT encoding; the math is sound, but the exact CNF isn't specified, so the enumeration's correctness rests on public code that a referee should inspect. read the letter →

arxiv 2506.01079 v1 pith:UCPGNLT6 submitted 2025-06-01 cs.CG cs.AI

Long Qian , Eric Wang , Bernardo Subercaseaux , Marijn J. H. Heule This is my paper

classification cs.CGcs.AI MSC 05B5068U05

keywords commonunfoldingsboxespolyominoesSATencodinglocalconstraintsexhaustiveenumerationΨ(3)cutedges

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper aims to settle where the smallest common unfolding of three different boxes lies, and argues that the answer is not 46, the value previously conjectured. The authors build a SAT-based search that replaces hard global constraints—graph connectivity and acyclicity of the cut edges—with local constraints on square orientations and edge directions, including a list of 18 forbidden local patterns. With this encoding they compute and enumerate common unfoldings of two boxes far beyond earlier limits, and use complete enumeration to prove that no three non-isomorphic boxes of area up to 58 share a common unfolding. If correct, the conjecture that the third such value is 46 is false, and the true value is at least 59, while the companion result gives the first area at which three equal-area boxes provably have no common unfolding.

What carries the argument

The machinery is a SAT encoding of cut edges on the boxes themselves, avoiding any explicit 2D net. Two families of local constraints replace the global constraints: square-orientation variables that force many edges to be cut by requiring relative orientations of adjacent uncut squares to be preserved, and edge-direction variables that orient each preserved edge toward a unique sink while forbidding a set of 18 small local patterns—the forbidden subgraphs—that every hole-free connected polyomino avoids. Two boxes are linked by a mapping between their unit squares that preserves cut edges and relative positions, encoded without materializing the net, and symmetry breaking fixes a distinguished pair of squares and orientation to split the search into independent subproblems.

What would settle it

Run an independent implementation of the encoding—or a direct search over cut-edge sets—for area 46 (or 54, 58) and check whether any common unfolding of the three candidate boxes is missed. Finding a single valid common unfolding would disprove Ψ(3)>58; alternatively, extracting and auditing the actual CNF clauses against the abstract forbidden-pattern theorem could reveal a soundness gap in the computed bound.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: no set of three non-isomorphic boxes of surface area 58 or less has a common unfolding, i.e. Ψ(3)>58. The proof is computational but not merely heuristic: for each candidate area (46, 54, 58) the authors completely enumerate all common unfoldings of two of the three boxes using a SAT encoding whose constraints are sound for valid unfoldings, then show by a SAT check per candidate that none of those pairs can be extended to the third box. The same computations yield Δ(3)=46, the first area where a triple of equal-area boxes is proven to have no common unfolding, as well as Δ(2)>86. On the positive side, the approach also finds many previously unknown common unfoldings of two boxes, reaching area 174, and reproduces the only known three-box unfolding at area 532 as a sanity check.

Load-bearing premise

The impossibility proof assumes that the CNF formula used in the computation exactly matches the 18 sound local patterns described in the paper, and that the solver's exhaustive enumeration is bug-free; the authors state in Section 9 that formal verification of the encoding is left for future work.

Editorial extensions

If this is right

The smallest area allowing a common unfolding of three boxes is at least 59, refuting the conjectured value of 46.
The companion result Δ(3)=46 gives the first proven area at which three equal-area boxes cannot share any common unfolding.
The improved two-box bound Δ(2)>86 more than doubles the previous best, and many pairwise common unfoldings up to area 174 are newly identified.
Complete enumeration of common unfoldings now reaches area 58, and all nets of 1×1×n boxes up to n=4 are enumerated for the first time.
The local-constraint approach reproduces the known area-532 three-box unfolding, lending practical support to the encoding's correctness.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

An independent reimplementation or a formal proof of the encoding could turn the computational bound into a verified theorem, a direction the authors flag as future work.
The same recipe—approximating global constraints with local ones and then filtering the results—could apply to other searches over polyominoes, unfoldings of other polyhedra, or planar embeddings where connectivity and acyclicity are the bottleneck.
Because valid unfoldings can have diameter close to the surface area, the earlier small-diameter heuristic could not have resolved the conjecture; the local approach removes an implicit restriction and suggests that previously out-of-reach instances may now be feasible.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's my take on arXiv:2506.01079. The headline result is real: it refutes Xu et al.'s conjecture Ψ(3)=46 by showing Ψ(3)>58, and gives Δ(3)=46 and Δ(2)>86. The key technical move is replacing global connectivity/acyclicity constraints in the SAT encoding with local edge-direction constraints, along with proofs that every genuine unfolding satisfies them. That's a genuine improvement over the BFS-style encodings, and it shows in the numbers: enumeration jumps from area 30 to 58, pairwise existence checks go well past 100.

What I like: the necessity proofs in Appendix A are careful. Theorem 14 shows any true unfolding induces a satisfying assignment of the local constraints, and Theorem 15 does the same for the equivalence mapping. There are no fitted parameters; the main result is an exhaustive enumeration over a superset of candidate cut-edge pairs, which is the right logical structure. The code is public, and they reproduce the known area-532 triple as a sanity check.

Soft spots: the paper never lists the actual CNF clauses used to block the forbidden patterns. The caption for Figure 14 says the white-node-absence condition applies to patterns 7g-7j, but it doesn't show how that's encoded. If the implementation blocked those patterns unconditionally, valid hole-free configurations with the diagonal square present would be rejected, making the enumeration a subset instead of a superset, and the unsat calls would prove nothing. The stress-test note I got raises exactly this scenario. I can't tell from the paper whether it's a real bug; the caption's wording suggests they encoded the condition, and the "two ternary clauses" remark hints at the right construction, but it's not enough to verify. The paper itself says formal verification of the encoding is future work. There's also a smaller gap: the post-filter that classifies nets into simple/touching/overlapping is not specified, so the counts in Table 4 aren't fully reproducible from text alone.

Overall, the central argument holds up if the code matches the stated patterns. The math is sound; the gap is in the encoding specification. This is a strong paper that deserves a serious referee—one who will check the GitHub code, or better, an independent reimplementation. I'd accept it for review, with the expectation that the authors add the clause-level encoding or a machine-checked proof. It should be published after that.

Referee Report

3 major / 4 minor

Summary. The paper presents a SAT-based approach to finding and enumerating polyomino nets that fold into two or more non-isomorphic boxes. The method replaces global connectivity/acyclicity constraints with local constraints on square orientations and edge directions, and it encodes the equivalence of two boxes through an implicit mapping rather than through an explicit 2D net. The main results are Theorem 1 (Ψ(3)>58), the companion statement Δ(3)=46, the bound Δ(2)>86, and exhaustive enumeration of common unfoldings for several box pairs, which together refute the Xu et al. conjecture Ψ(3)=46. The central impossibility argument reduces the statement to an all-sat enumeration of a CNF formula over a superset of the true common unfoldings, followed by unsat checks for the third box.

Significance. If the main enumeration is correct, the paper resolves a published conjecture, establishes a new lower bound for Ψ(3), and provides the first area for which three equal-area boxes provably have no common unfolding although pairs among them do. The public code repository, the successful reproduction of the area-532 common unfolding, and the carefully argued necessity lemmas in Appendix A are concrete strengths. The paper also makes a genuinely interesting methodological claim: that local constraints can substitute for global graph constraints in this search. However, the central theorem is only as strong as the exact CNF encoding, and the manuscript does not currently provide a clause-level or machine-checked correctness argument for that encoding; the authors themselves defer formal verification to future work. The significance is therefore conditional on closing that gap.

major comments (3)

[Section 4.2 / Figure 14 / Theorem 16] The CNF formula Φ(B1,B2) is not specified at clause level, and this gap is load-bearing for the main impossibility result. The second-row patterns of Figure 14 (and Figure 7g–7j) are forbidden only when the white node is not present in the net, and that absence condition is part of the necessity proof in Theorems 3, 12, and 14. The variables defined in Section 4.2 (e_s1,s2, d_s1,s2, and square orientations) do not by themselves express whether the diagonal cell of a 2×2 pattern is present in the planar net. If the implementation blocks the three black directed edges unconditionally, then a valid hole-free configuration with the diagonal cell present would be rejected, making the all-sat enumeration of Table 4 a strict subset of the true common unfoldings; in that case the unsat checks in Theorem 16 would not rule out a triple. The paper should provide the exact clause schemata (or the generated CNF for the enumerated rows) and prove that they implement precisely the white-node-absent patterns.
[Section 7 / Table 4 / Theorem 14] The soundness proof in Appendix A applies to hole-free connected polyominoes: Theorem 12 uses the hypothesis h(U)=0, and Lemma 11 explicitly assumes a connected polyomino without holes. Yet Section 7 and Table 4 count 'touching' and 'overlapping' nets as solutions of the enumeration. If those non-standard nets are part of the set S′ on which the Ψ(3)>58 argument is run, the necessity of the local constraints has not been established for them, so the superset guarantee may fail. The paper should clarify whether Theorem 1 concerns only standard simply connected nets; if so, it should state that the touching/overlapping counts are informational and not used in the impossibility argument, and if not, it should extend the soundness proof to cover them.
[Section 7 / Table 3 / Δ(2)>86] The text says that 'we were able to compute unfoldings between all pairs of boxes with equal area up to 86', but the local constraints are necessary conditions, not sufficient ones. No validation step is described that turns a satisfying assignment of the necessary constraints into an explicit non-overlapping net that folds into both boxes. Section 9 mentions discarding solutions that do not satisfy the original constraints, but the manuscript does not say how this was performed for the entries in Table 3. Without such a check, the claim Δ(2)>86 is not established from the material presented.

minor comments (4)

[Appendix A.2] The cross-references in the appendix are inconsistent with the lemma numbering: the proof of Lemma 10 refers to 'Theorem 9' and 'Theorem 8', and the proof of Lemma 11 refers to 'Theorem 4'. These should point to the corresponding lemmas (or the numbering should be unified).
[Table 3 caption] The 'First' column mixes citation labels, checkmarks, and empty fields without a legend. A checkmark presumably means that the common unfolding was first found in this paper, but the caption should say so explicitly.
[Table 4 caption] The caption should distinguish 'all satisfying assignments' from 'all unique common unfoldings'. The text uses both #SAT and Unique, but the deduplication criterion (e.g., by cut-edge pair or by net shape) is not described.
[Figure 11] The caption refers to green and yellow squares, but the figure is printed in grayscale; the description should be adjusted to the actual rendering.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the impossibility proof rests on soundness theorems plus exhaustive enumeration, with no fitted parameter or load-bearing self-reference.

full rationale

Score 0. The paper's central claim Ψ(3)>58 is established by a two-part chain that is not circular. Part (1) (Theorems 14 and 15) proves that any actual common unfolding induces a satisfying assignment of the SAT encoding: orientations follow from Lemma 13 (orientation preservation under grid-line folding motions), and the forbidden directed patterns are proved necessary for hole-free connected polyominoes in Theorems 12 and 14. Part (2) (Theorem 16) uses an exhaustive allsat enumeration of the two-box encoding, and for every enumerated pair shows that the third-box constraints are unsatisfiable. The enumeration is deliberately over-approximate (S' ⊇ S), so even if local constraints admit extra assignments, the unsat result still rules out all real common unfoldings. Nothing in the encoding is fitted to the 46/54/58 triples, and the target theorem is not used as an assumption. The only caveat flagged by the authors themselves—that the intricate encoding is not yet formally verified (Section 9)—is a completeness/implementation risk, not a circularity. The self-citation to [8] appears only as a future-verification suggestion and is not load-bearing. No step reduces, by construction or by self-reference, to its own inputs.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No free parameters are fitted. The work rests on standard geometric and folding assumptions, on the correctness of the SAT toolchain, and on the paper's own necessity proofs. The authors themselves note that formally defining unfoldings is a challenging part of any future verification.

assumptions (5)

domain assumption Unfolding is a sequence of orientation-preserving transformations acting along grid-lines (Lemma 13).
Used to prove that relative square orientations are invariant across uncut edges. The authors do not give a formal definition of folding/unfolding, citing Demaine and O'Rourke Ch. 11 and 15.
domain assumption A valid net for a box is a connected, hole-free polyomino, and cut edges correspond exactly to non-adjacent square pairs when the net is folded (properties P1-P4).
Standard definition in the field, invoked throughout Sections 3 and 4 and in Theorem 14.
standard math Jordan curve theorem and the ray-crossing lemma (Lemma 2).
Used in Appendix A.1 to show that an F-avoidant oriented polyomino containing a directed cycle must have a hole.
standard math The square adjacency graph of a box is bipartite and has maximum degree 4.
Used in Lemma 10 to justify the parity-based distance arguments for edge orientations.
domain assumption The SAT solver CaDiCaL and the allsat extension terminate and return correct results for every instance used.
All computational results depend on solver correctness; no certificates are shipped, and the paper calls for formal verification.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Unfolding Boxes with Local Constraints." pith.science (2026). https://pith.science/paper/UCPGNLT6

@misc{pith2026250601079,
  author       = {Pith},
  title        = {Pith review of: Unfolding Boxes with Local Constraints},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UCPGNLT6}},
  note         = {Machine review of arXiv:2506.01079}
}

read the original 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).

Figures

Figures reproduced from arXiv: 2506.01079 by the authors.

**Figure 2.** Two non-isomorphic boxes that can be folded from the same net. For a positive integer 𝑠 representing a surface area, let 𝑃(𝑠) be the set of all triples (𝑎, 𝑏, 𝑐) with 𝑎 ≤ 𝑏 ≤ 𝑐 such that 𝑠 = 2(𝑎𝑏+ 𝑎𝑐 + 𝑏𝑐). In other words, 𝑃(𝑠) is the set of all possible integer dimensions of a box with surface area 𝑠. For example, 𝑃(22) = {(1, 1, 5), (1, 2, 3)}, and as shown in [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗

**Figure 3.** A common unfolding of area 174. In this work, we show that Ψ(3) > 58, that Δ(3) = 46. We show as well that Δ(2) > 86, and using heuristics we manage to compute solutions for certain very large areas (see [PITH_FULL_IMAGE:figures/full_fig_p002_3.png] view at source ↗

Figures from the paper (14 more)

**Figure 4.** Figure 4: The correspondence between cuts in a box and its folding nets. present some brief elements in comparison with previous research. In 2011, Abel et al. [1] enumerated all common unfoldings for boxes 1×1×5 and 1×2×3 in about 10 hours [11], whereas our approach allows a co…

**Figure 5.** Figure 5: Illustration of the necessity of the cut-corners property [PITH_FULL_IMAGE:figures/full_fig_p005_5.png]

**Figure 6.** Figure 6: Square orientations, labels, and relative orientations [PITH_FULL_IMAGE:figures/full_fig_p006_6.png]

**Figure 7.** Figure 7: The set F of forbidden subgraphs. The blue edges represent that the graph belongs to F regardless of the orientation of its blue edges. For the forbidden patterns 7g to 7j, the white node must not be present in the graph. Blocking the patterns 7a to 7b requires one bin…

**Figure 8.** Figure 8: shows how the search for a common net can be done explicitly by enforcing equivalence on the resulting 2D unfoldings, which is costly and introduces additional auxiliary variables. In contrast, we achieve this by encoding an equivalence mapping 𝑀 : 𝐵2 → 𝐵1 directly on …

**Figure 9.** Figure 9: Constraints on 𝑀 with relative change in orientation 𝜌. • Auxiliary variables 𝜌𝑠,𝑑 for 𝑠 ∈ 𝐵1, 𝑑 ∈ {1, 2, 3, 4} that encode a function 𝜌: 𝐵1 → [4] indicating the change in orientation between 𝑠 and the unique 𝑠 ′ ∈ 𝐵2 where 𝑀(𝑠 ′ ) = 𝑠. I.e. 𝑜(𝑠 ′ ) = 𝑜(𝑠) + 𝜌(𝑠) holds…

**Figure 10.** Figure 10: Image of pairs of squares under 𝑀, mapping the (black, red) pair on 𝐵2 to the (black, red) pair on 𝐵1 [PITH_FULL_IMAGE:figures/full_fig_p010_10.png]

**Figure 11.** Figure 11: Overlapping net (left) and touching net (right) of 1×1×11 [PITH_FULL_IMAGE:figures/full_fig_p011_11.png]

**Figure 12.** Figure 12: Common unfolding of 3 boxes at area 532 [7]. References [1] Abel, Z., Demaine, E.D., Demaine, M.L., Matsui, H., Rote, G., Uehara, R.: Common developments of several different orthogonal boxes. In: Proceedings of the 23rd Annual Canadian Conference on Computational Geo…

**Figure 13.** Figure 13: Example of an oriented polyominio. The hole number of an oriented polyomino 𝑃, denoted ℎ(𝑃), corresponds intuitively to the number of holes in the polyomino. Formally, ℎ(𝑃) is the number of connected components of the subgraph of G induced by 𝑉 (G) \ 𝑉 (𝑃) minus one. …

**Figure 14.** Figure 14: The set F of forbidden subgraphs. The blue edges represent that the graph belongs to F regardless of the orientation of its blue edges. For the forbidden patterns in the second row to match a subgraph, the white node must not be present in the graph. There is a total …

**Figure 15.** Figure 15: Illustration of the proof of Theorem 3. 𝑥-coordinate 𝑀, and reaches ℓ at 𝑥-coordinate 𝑚, then at some point in 𝜋 ′ there is at lease one edge going left and arriving to a vertex 𝑣 ′ := (𝑚, 𝑦𝑣 ′ ), with 𝑦𝑣 ≠ 𝑦𝑣 ′ . Among these, take the 𝑣 ′ that minimizes | 𝑦𝑣 − 𝑦𝑣 ′ |…

**Figure 16.** Figure 16: Forbidden pattern for the proof of Theorem 10. In what follows, we will consider undirected and connected graphs with no self-loops, and use notation 𝑑(𝑢, 𝑣) for the distance between two vertices 𝑢, 𝑣 in the graph, defined as the length of the shortest path between 𝑢 …

**Figure 17.** Figure 17: Top: A common unfolding of area 46 for boxes 1×1×11 (faces shown) and 1×2×7. The diameter of this net is 41, the largest among all solutions. Bottom: A common unfolding for boxes 1×1×20 and 1×2×13 [PITH_FULL_IMAGE:figures/full_fig_p022_17.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

12 extracted references · 9 canonical work pages

[1]

Abel, Z., Demaine, E.D., Demaine, M.L., Matsui, H., Rote, G., Uehara, R.: Common developments of several diﬀerent orthogonalboxes.In: Proceedingsofthe23rdAnnualCanadianConferenceonComputationalGeometry,Toronto,Ontario, Canada,August10-12,2011(2011),http://www.cccg.ca/proceedings/2011/papers/paper49.pdf

work page 2011
[2]

LectureNotesinComputerScience,vol.14681,pp.133–152.Springer(2024).https://doi.org/10.1007/978-3-031-65627-9_7 UNFOLDING BOXES WITH LOCAL CONSTRAINTS 15

Biere,A.,Faller,T.,Fazekas,K.,Fleury,M.,Froleyks,N.,Pollitt,F.: CaDiCaL2.0.In: Gurﬁnkel,A.,Ganesh,V.(eds.)Computer AidedVeriﬁcation-36thInternationalConference,CAV2024,Montreal,QC,Canada,July24-27,2024,Proceedings,PartI. LectureNotesinComputerScience,vol.14681,pp.133–152.Springer(2024).https://doi.org/10.1007/978-3-031-65627-9_7 UNFOLDING BOXES WITH LOCAL...

doi:10.1007/978-3-031-65627-9_7 2024
[3]

Brown,S.T.,Buitrago,P.,Hanna,E.,Sanielevici,S.,Scibek,R.,Nystrom,N.A.: Bridges-2: APlatformforRapidly-Evolving andDataIntensiveResearch.In: PracticeandExperienceinAdvancedResearchComputing.PEARC’21,Associationfor ComputingMachinery,NewYork,NY,USA(2021).https://doi.org/10.1145/3437359.3465593

arXiv 2021
[4]

Demaine,E.,O’Rourke,J.: GeometricFoldingAlgorithms: Linkages,Origami,Polyhedra.CambridgeUniversityPress(2007)

work page 2007
[5]

In: Fermé, E., Leite, J

Gebser, M., Janhunen, T., Rintanen, J.: SAT Modulo Graphs: Acyclicity. In: Fermé, E., Leite, J. (eds.) Logics in Artiﬁcial Intelligence.pp.137–151.SpringerInternationalPublishing,Cham(2014)

work page 2014
[6]

In: The 20th Canadian Conference on ComputationalGeometry(CCCG’08)(2008)

Mitani, J., Uehara, R.: Polygons folding to plural incongruent orthogonal boxes. In: The 20th Canadian Conference on ComputationalGeometry(CCCG’08)(2008)

work page 2008
[7]

Shirakawa,T.,Uehara,R.: Commondevelopmentsofthreediﬀerentorthogonalboxes.In: The24thCanadianConferenceon ComputationalGeometry(CCCG’12)(2012)

work page 2012
[8]

Subercaseaux, B., Nawrocki, W., Gallicchio, J., Codel, C., Carneiro, M., Heule, M.J.H.: Formal Veriﬁcation of the Empty HexagonNumber.In: 15thInternationalConferenceonInteractiveTheoremProving(ITP2024).LeibnizInternationalPro- ceedingsinInformatics(LIPIcs),vol.309,pp.35:1–35:19.Dagstuhl,Germany(2024).https://doi.org/10.4230/LIPIcs.ITP.2024.35

doi:10.4230/lipics.itp.2024.35 2024

Show all 12 references

[9]

Tadaki, R., Amano, K.: Search for developments of a box having multiple ways of folding by SAT solver (2020), https: //arxiv.org/abs/2005.02645

2020 arXiv
[10]

Uehara,R.: Asurveyandrecentresultsaboutcommondevelopmentsoftwoormoreboxes.In: Origami 6: proceedingsof thesixthinternationalmeetingonorigamiscience,mathematics,andeducation(2015)

2015
[11]

Xu,D.,Horiyama,T.,Shirakawa,T.,Uehara,R.: Commondevelopmentsofthreeincongruentboxesofarea30.Computational Geometry64,1–12(2017).https://doi.org/10.1016/j.comgeo.2017.03.001

2017 doi
[12]

forbidden subgraphs

Zhou,N.F.,Wang,R.,Yap,R.H.C.: AComparisonofSATEncodingsforAcyclicityofDirectedGraphs.In: 26thInternational ConferenceonTheoryandApplicationsofSatisﬁabilityTesting(SAT2023).LeibnizInternationalProceedingsinInformatics (LIPIcs),vol.271,pp.30:1–30:9.Dagstuhl,Germany(2023).https:/...

2023 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Abel, Z., Demaine, E.D., Demaine, M.L., Matsui, H., Rote, G., Uehara, R.: Common developments of several diﬀerent orthogonalboxes.In: Proceedingsofthe23rdAnnualCanadianConferenceonComputationalGeometry,Toronto,Ontario, Canada,August10-12,2011(2011),http://www.cccg.ca/proceedings/2011/papers/paper49.pdf

work page 2011

[2] [2]

LectureNotesinComputerScience,vol.14681,pp.133–152.Springer(2024).https://doi.org/10.1007/978-3-031-65627-9_7 UNFOLDING BOXES WITH LOCAL CONSTRAINTS 15

Biere,A.,Faller,T.,Fazekas,K.,Fleury,M.,Froleyks,N.,Pollitt,F.: CaDiCaL2.0.In: Gurﬁnkel,A.,Ganesh,V.(eds.)Computer AidedVeriﬁcation-36thInternationalConference,CAV2024,Montreal,QC,Canada,July24-27,2024,Proceedings,PartI. LectureNotesinComputerScience,vol.14681,pp.133–152.Springer(2024).https://doi.org/10.1007/978-3-031-65627-9_7 UNFOLDING BOXES WITH LOCAL...

doi:10.1007/978-3-031-65627-9_7 2024

[3] [3]

Brown,S.T.,Buitrago,P.,Hanna,E.,Sanielevici,S.,Scibek,R.,Nystrom,N.A.: Bridges-2: APlatformforRapidly-Evolving andDataIntensiveResearch.In: PracticeandExperienceinAdvancedResearchComputing.PEARC’21,Associationfor ComputingMachinery,NewYork,NY,USA(2021).https://doi.org/10.1145/3437359.3465593

arXiv 2021

[4] [4]

Demaine,E.,O’Rourke,J.: GeometricFoldingAlgorithms: Linkages,Origami,Polyhedra.CambridgeUniversityPress(2007)

work page 2007

[5] [5]

In: Fermé, E., Leite, J

Gebser, M., Janhunen, T., Rintanen, J.: SAT Modulo Graphs: Acyclicity. In: Fermé, E., Leite, J. (eds.) Logics in Artiﬁcial Intelligence.pp.137–151.SpringerInternationalPublishing,Cham(2014)

work page 2014

[6] [6]

In: The 20th Canadian Conference on ComputationalGeometry(CCCG’08)(2008)

Mitani, J., Uehara, R.: Polygons folding to plural incongruent orthogonal boxes. In: The 20th Canadian Conference on ComputationalGeometry(CCCG’08)(2008)

work page 2008

[7] [7]

Shirakawa,T.,Uehara,R.: Commondevelopmentsofthreediﬀerentorthogonalboxes.In: The24thCanadianConferenceon ComputationalGeometry(CCCG’12)(2012)

work page 2012

[8] [8]

Subercaseaux, B., Nawrocki, W., Gallicchio, J., Codel, C., Carneiro, M., Heule, M.J.H.: Formal Veriﬁcation of the Empty HexagonNumber.In: 15thInternationalConferenceonInteractiveTheoremProving(ITP2024).LeibnizInternationalPro- ceedingsinInformatics(LIPIcs),vol.309,pp.35:1–35:19.Dagstuhl,Germany(2024).https://doi.org/10.4230/LIPIcs.ITP.2024.35

doi:10.4230/lipics.itp.2024.35 2024