Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations

PLDI 2020, March 2020
BibTeX 
@inproceedings{2020-pldi-szalinski,
  title = {Synthesizing Structured {CAD} Models with Equality Saturation and Inverse Transformations},
  author = {
    Chandrakana Nandi and
    Max Willsey and
    Adam Anderson and
    James R. Wilcox and
    Eva Darulova and
    Dan Grossman and
    Zachary Tatlock
  },
  year = {2020},
  isbn = {9781450376136},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3385412.3386012},
  doi = {10.1145/3385412.3386012},
  booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages = {31–44},
  numpages = {14},
  keywords = {Program Synthesis, Equality Saturation, Computer-Aided Design, Decompilation},
  location = {London, UK},
  series = {PLDI 2020},
}
Existing mesh decompilers turn triangle meshes into CSG expressions. Szalinski robustly synthesizes smaller, structured Caddy programs from CSG expressions. This can ease customization by simplifying edits: small, mostly local changes yield usefully different models. The photo shows the 3D printed hex wrench holder after customizing hole sizes.

Abstract

Recent program synthesis techniques help users customize CAD models (e.g., for 3D printing) by decompiling low-level triangle meshes to Constructive Solid Geometry (CSG) expressions. Without loops or functions, editing CSG can require many coordinated changes, and existing mesh decom-pilers use heuristics that can obfuscate high-level structure.

This paper proposes a second decompilation stage to robustly “shrink” unstructured CSG expressions into more editable programs with map and fold operators. We present Szalinski, a tool that uses Equality Saturation with semantics-preserving CAD rewrites to efficiently search for smaller equivalent programs. Szalinski relies on inverse transformations, a novel way for solvers to speculatively add equivalences to an E-graph. We qualitatively evaluate Szalinski in case studies, show how it composes with an existing mesh decompiler, and demonstrate that Szalinski can shrink large models in seconds.

Overview Video