Elamur Research⌕
☰
home / papers / 2020 / Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations

Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations

Paper · 2020 · Chandrakana Nandi, Max Willsey, Adam Anderson et al.

Summary

Tools that decompile 3D triangle meshes into Constructive Solid Geometry (CSG) produce flat programs with no loops or functions. Their output is long and repetitive, and its features are often expressed inconsistently and ordered arbitrarily, which makes editing tedious. The authors add a second decompilation stage: Szalinski takes a flat CSG expression and synthesizes an equivalent but smaller Caddy program, where Caddy is CSG augmented with map/fold-style list operators (Fold, Tabulate, Map2, Concat). Szalinski builds on Equality Saturation over E-graphs, using semantics-preserving CAD rewrites together with simple arithmetic solvers that "reroll loops." Reordering lists with associative and commutative rewrites can make E-graphs grow exponentially (the AC-matching problem). To avoid this, the paper introduces inverse transformations, which let solvers speculatively add reordered or regrouped expressions to the E-graph along with an annotation describing how the input was changed. The approach is not specific to CAD. Szalinski works on top of an existing mesh decompiler and shrinks real-world models in seconds. The resulting compact, parametrized programs make edits such as changing tooth counts or hole sizes simple and local.

Key points

  • Szalinski is a roughly 3,000-line Rust prototype with a library of 65 CAD rewrites. Its output language, Caddy, has a Core Caddy subset that corresponds directly to CSG.
  • In the hex wrench holder example, a ~1600 LOC mesh becomes ~50 LOC of CSG after mesh decompilation, and Szalinski reduces that to a ~6 LOC Caddy program.
  • The large-scale evaluation used 2,127 Thingiverse models, grouped by AST size into 769 tiny, 786 small, 374 medium and 198 large.
  • Correctness was checked by comparing meshes. All Hausdorff distances were below 0.01, except for 148 cases where CGAL could not compute the distance and the meshes were compared visually.
  • On the 50 InverseCSG benchmarks, most models lacked repetitive structure. For benchmark 157 (a gear), Szalinski inferred a TranslateSpherical pattern, but only after an unsound rewrite was applied manually. Handling such cases would require geometric reasoning, which the prototype does not support.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of WashingtonSeattle · United States422 works · 213,538 citations🔬Max Planck Institute for Software SystemsSaarbrücken · Germany6 works · 39,162 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksEngineering · 206 worksComputer Graphics and Computer-Aided Design · 19 worksComputational Mechanics · 8 works

Cite

Cite as Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman and Zachary Tatlock. 2020. Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations. arXiv:1909.12252 (PLDI 2020).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/3385412.3386012 · arXiv 1909.12252

@misc{nandi2020synthesizing,
  title = {{Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations}},
  author = {Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman and Zachary Tatlock},
  year = {2020},
  doi = {10.1145/3385412.3386012},
  eprint = {1909.12252},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3385412.3386012}
}

References

42 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Celena Alcock, Nathaniel Hudson, and Parmit K. Chilana. 2016. Barriers to Using, Customizing, and Printing 3D Designs on Thingiverse. In Proceedings of the 19th International Conference on Supporting Group Work (GROUP ’16). ACM, New York, NY, USA, 195–199. https://doi.org/10.1145/2957276.2957301 — [doi:10.1145/2957276.2957301](https://doi.org/10.1145/2957276.2957301) ↗
  2. Sorav Bansal and Alex Aiken. 2008. Binary Translation Using Peephole Superoptimizers. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI’08). USENIX Association, Berkeley, CA, USA, 177–192. http://dl.acm.org/citation. cfm?id=1855741.1855754 ↗
  3. Walid Belkhir and Alain Giorgetti. 2012. Lazy AC-Pattern Matching for Rewriting. Electronic Proceedings in Theoretical Computer Science 82 (Apr 2012), 37–51. https://doi.org/10.4204/eptcs.82.3 — [doi:10.4204/eptcs.82.3](https://doi.org/10.4204/eptcs.82.3) ↗
  4. CGAL. 2018. CGAL. https://www.cgal.org. ↗
  5. Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. 2016. Programmatic and Direct Manipulation, Together at Last. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, New York, NY, USA, 341– 354. https://doi.org/10.1145/29080… — [doi:10.1145/2908080.2908103](https://doi.org/10.1145/2908080.2908103) ↗
  6. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. 2007. All About Maude - a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, Berlin, Heidelberg. find
  7. Customizable. 2019. Thingiverse Customizable. https://www.thingiverse.com/customizable. ↗
  8. Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340. http:… find
  9. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 378– 388. find
  10. David Detlefs, Greg Nelson, and James B. Saxe. 2005. Simplify: A Theorem Prover for Program Checking. J. ACM 52, 3 (May 2005), 365–473. https://doi.org/10.1145/1066100.1066102 — [doi:10.1145/1066100.1066102](https://doi.org/10.1145/1066100.1066102) ↗
  11. Tao Du, Jeevana Priya Inala, Yewen Pu, Andrew Spielberg, Adriana Schulz, Daniela Rus, Armando Solar-Lezama, and Wojciech Matusik. 2018. InverseCSG: automatic conversion of 3D models to CSG trees. 1–16. https://doi.org/10.1145/3272127.3275006 — [doi:10.1145/3272127.3275006](https://doi.org/10.1145/3272127.3275006) ↗
  12. Kevin Ellis, Maxwell I. Nye, Yewen Pu, Felix Sosa, Joshua B. Tenenbaum, and Armando Solar-Lezama. 2019. Write, Execute, Assess: Program Synthesis with a REPL. In NeurIPS.
  13. Kevin Ellis, Daniel Ritchie, Armando Solar-Lezama, and Joshua B. Tenenbaum. 2018. Learning to Infer Graphics Programs from Hand-Drawn Images. https://openreview.net/forum?id=H1DJFybC- ↗
  14. Markus Friedrich, Pierre-Alain Fayolle, Thomas Gabor, and Claudia Linnhoff-Popien. 2019. Optimizing Evolutionary CSG Tree Extraction. In Proceedings of the Genetic and Evolutionary Computation Conference (GECCO ’19). ACM, New York, NY, USA, 1183–1191. https://doi.org/10.1145/3321707.3321771 — [doi:10.1145/3321707.3321771](https://doi.org/10.1145/3321707.3321771) ↗
  15. Nathaniel Hudson, Celena Alcock, and Parmit K. Chilana. 2016. Understanding Newcomers to 3D Printing: Motivations, Workflows, and Barriers of Casual Makers. In Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems (CHI ’16). ACM, New York, NY, USA, 384–396. https://doi.org/10.… — [doi:10.1145/2858036.2858266](https://doi.org/10.1145/2858036.2858266) find
  16. Rajeev Joshi, Greg Nelson, and Keith Randall. 2002. Denali: A Goal-directed Superoptimizer. SIGPLAN Not. 37, 5 (May 2002), 304–314. https://doi.org/10.1145/543552.512566 — [doi:10.1145/543552.512566](https://doi.org/10.1145/543552.512566) ↗
  17. Hélène Kirchner and Pierre-Etienne Moreau. 2001. Promoting Rewriting to a Programming Language: A Compiler for Non-deterministic Rewrite Programs in Associative-commutative Theories. J. Funct. Program. 11, 2 (March 2001), 207–251. http://dl.acm.org/citation.cfm?id=968486.968488 ↗
  18. Niloy J. Mitra, Mark Pauly, Michael Wand, and Duygu Ceylan. 2013. Symmetry in 3D Geometry: Extraction and Applications. Comput. Graph. Forum 32, 6 (Sept. 2013), 1–23. https://doi.org/10.1111/cgf.12010 — [doi:10.1111/cgf.12010](https://doi.org/10.1111/cgf.12010) ↗
  19. P.H. Moon and D.E. Spencer. 1988. Field theory handbook: including coordinate systems, differential equations, and their solutions. Springer-Verlag. https://books.google.com/books?id=EDnvAAAAMAAJ ↗
  20. James R Munkers. 2000. Topology. find
  21. Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, and Zachary Tatlock. 2018. Functional Programming for Compiling and Decompiling Computer-aided Design. Proc. ACM Program. Lang. 2, ICFP, Article 99 (July 2018), 31 pages. https://doi.org/10.1145/3236794 — [doi:10.1145/3236794](https://doi.org/10.1145/3236794) ↗
  22. Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph.D. Dissertation. Stanford, CA, USA. AAI8011683. find
  23. OpenScad. 2019. OpenScad. The Programmers Solid 3D CAD Modeller. http://www.openscad.org/. ↗
  24. Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock. 2015. Automatically Improving Accuracy for Floating Point Expressions. SIGPLAN Not. 50, 6 (June 2015), 1–11. https://doi.org/10.1145/2813885.2737959 ↗
  25. William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings Supercomputing ’91, Albuquerque, NM, USA, November 18-22, 1991. 4–13. https://doi.org/10.1145/125826.125848 ↗
  26. William Pugh and David Wonnacott. 1992. Eliminating False Data Dependences using the Omega Test. In Proceedings of the ACM SIG-PLAN’92 Conference on Programming Language Design and Implementation (PLDI), San Francisco, California, USA, June 17-19, 1992. 140–151. https://doi.org/10.1145/143095.143129 — [doi:10.1145/143095.143129](https://doi.org/10.1145/143095.143129) ↗
  27. C. Ronse. 1990. Regular open or closed sets. find
  28. R. Schnabel, R. Wahl, and R. Klein. 2007. Efficient RANSAC for Point-Cloud Shape Detection. Computer Graphics Forum (2007). https://doi.org/10.1111/j.1467-8659.2007.01016.x — [doi:10.1111/j.1467-8659.2007.01016.x](https://doi.org/10.1111/j.1467-8659.2007.01016.x) ↗
  29. Adriana Schulz, Jie Xu, Bo Zhu, Changxi Zheng, Eitan Grinspun, and Wojciech Matusik. 2017. Interactive Design Space Exploration and Optimization for CAD Models. ACM Trans. Graph. 36, 4, Article 157 (July 2017), 14 pages. https://doi.org/10.1145/3072959.3073688 — [doi:10.1145/3072959.3073688](https://doi.org/10.1145/3072959.3073688) ↗
  30. Gopal Sharma, Rishabh Goyal, Difan Liu, Evangelos Kalogerakis, and Subhransu Maji. 2017. CSGNet: Neural Shape Parser for Constructive Solid Geometry. CoRR abs/1712.08290 (2017). arXiv:1712.08290 http://arxiv.org/abs/1712.08290 — [arXiv:1712.08290](https://arxiv.org/abs/1712.08290) ↗
  31. Benjamin Sherman, Jesse Michel, and Michael Carbin. 2019. Sound and Robust Solid Modeling via Exact Real Arithmetic and Continuity. Proc. ACM Program. Lang. 3, ICFP, Article 99 (July 2019), 29 pages. https://doi.org/10.1145/3341703 — [doi:10.1145/3341703](https://doi.org/10.1145/3341703) ↗
  32. Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. Berkeley, CA, USA. Advisor(s) Bodik, Rastislav. AAI3353225.
  33. Michael Stepp, Ross Tate, and Sorin Lerner. 2011. Equality-Based Translation Validator for LLVM. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 737–742. find
  34. Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality Saturation: A New Approach to Optimization. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09). ACM, New York, NY, USA, 264–276. https://doi.org/10.1145/1480881.1… ↗
  35. Thingiverse. 2019. Thingiverse. https://www.thingiverse.com/. ↗
  36. Yonglong Tian, Andrew Luo, Xingyuan Sun, Kevin Ellis, William T. Freeman, Joshua B. Tenenbaum, and Jiajun Wu. 2019. Learning to Infer and Execute 3D Shape Programs. In International Conference on Learning Representations. find
  37. Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14). ACM, New York, NY, USA, 530–541. https://doi.org/10.1145/2594291.2594340 — [doi:10.1145/2594291.2594340](https://doi.org/10.1145/2594291.2594340) ↗
  38. Sid-Ahmed-Ali Touati and Denis Barthou. 2006. On the Decidability of Phase Ordering Problem in Optimizing Compilation. In Proceedings of the 3rd Conference on Computing Frontiers (CF ’06). ACM, New York, NY, USA, 147–156. https://doi.org/10.1145/1128022.1128042 — [doi:10.1145/1128022.1128042](https://doi.org/10.1145/1128022.1128042) ↗
  39. Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations. SIGPLAN Not. 43, 1 (Jan. 2008), 17–27. https://doi.org/10.1145/1328897.1328444 — [doi:10.1145/1328897.1328444](https://doi.org/10.1145/1328897.1328444) ↗
  40. Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified Validation of Lazy Code Motion. SIGPLAN Not. 44, 6 (June 2009), 316–326. https://doi.org/10.1145/1543135.1542512 — [doi:10.1145/1543135.1542512](https://doi.org/10.1145/1543135.1542512) ↗
  41. Max Willsey, Yisu Remy Wang, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, and Zachary Tatlock. 2020. egg: Easy, Efficient, and Extensible E-graphs. arXiv:cs.PL/2004.03082 find
  42. Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock, and Adriana Schulz. 2019. Carpentry Compiler. ACM Trans. Graph. 38, 6, Article 195 (Nov. 2019), 14 pages. https://doi.org/10.1145/3355089.3356518 — [doi:10.1145/3355089.3356518](https://doi.org/10.1145/3355089.3356518) ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/nandi-2020-synthesizing-structured-cad-models-equality/