{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:47Z","timestamp":1754161847885,"version":"3.41.2"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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).<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_38","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:58Z","timestamp":1753789678000},"page":"736-754","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Unfolding Boxes with Local Constraints"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1567-3948","authenticated-orcid":false,"given":"Long","family":"Qian","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-6636-4541","authenticated-orcid":false,"given":"Eric","family":"Wang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2295-1299","authenticated-orcid":false,"given":"Bernardo","family":"Subercaseaux","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"38_CR1","unstructured":"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 Geometry, Toronto, Ontario, Canada, August 10-12, 2011 (2011), http:\/\/www.cccg.ca\/proceedings\/2011\/papers\/paper49.pdf"},{"key":"38_CR2","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133\u2013152. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"38_CR3","doi-asserted-by":"publisher","unstructured":"Brown, S.T., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.A.: Bridges-2: A Platform for Rapidly-Evolving and Data Intensive Research. In: Practice and Experience in Advanced Research Computing. PEARC \u201921, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3437359.3465593","DOI":"10.1145\/3437359.3465593"},{"key":"38_CR4","doi-asserted-by":"crossref","unstructured":"Demaine, E., O\u2019Rourke, J.: Geometric Folding Algorithms: Linkages, Origami, Polyhedra. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511735172"},{"key":"38_CR5","doi-asserted-by":"crossref","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: SAT Modulo Graphs: Acyclicity. In: Ferm\u00e9, E., Leite, J. (eds.) Logics in Artificial Intelligence. pp. 137\u2013151. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-11558-0_10"},{"key":"38_CR6","unstructured":"Mitani, J., Uehara, R.: Polygons folding to plural incongruent orthogonal boxes. In: The 20th Canadian Conference on Computational Geometry (CCCG\u201908) (2008)"},{"key":"38_CR7","unstructured":"Qian, L., Wang, E., Subercaseaux, B., Heule, M.J.H.: Unfolding boxes with local constraints (2025), https:\/\/arxiv.org\/abs\/2506.01079"},{"key":"38_CR8","unstructured":"Shirakawa, T., Uehara, R.: Common developments of three different orthogonal boxes. In: The 24th Canadian Conference on Computational Geometry (CCCG\u201912) (2012)"},{"key":"38_CR9","doi-asserted-by":"publisher","unstructured":"Subercaseaux, B., Nawrocki, W., Gallicchio, J., Codel, C., Carneiro, M., Heule, M.J.H.: Formal Verification of the Empty Hexagon Number. In: 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 309, pp. 35:1\u201335:19. Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.35","DOI":"10.4230\/LIPIcs.ITP.2024.35"},{"key":"38_CR10","unstructured":"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"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"Uehara, R.: A survey and recent results about common developments of two or more boxes. In: Origami $$^6$$: proceedings of the sixth international meeting on origami science, mathematics, and education (2015)","DOI":"10.1090\/mbk\/095.1\/08"},{"key":"38_CR12","doi-asserted-by":"publisher","unstructured":"Xu, D., Horiyama, T., Shirakawa, T., Uehara, R.: Common developments of three incongruent boxes of area 30. Computational Geometry 64, 1\u201312 (2017). https:\/\/doi.org\/10.1016\/j.comgeo.2017.03.001","DOI":"10.1016\/j.comgeo.2017.03.001"},{"key":"38_CR13","doi-asserted-by":"publisher","unstructured":"Zhou, N.F., Wang, R., Yap, R.H.C.: A Comparison of SAT Encodings for Acyclicity of Directed Graphs. In: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0271, pp. 30:1\u201330:9. Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.30","DOI":"10.4230\/LIPIcs.SAT.2023.30"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:48:01Z","timestamp":1753789681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}