Synthesizing Backward through the Geometry Pipeline

Zach Tatlock
University of Washington

Abstract:

Most physical goods are actually program outputs: designers develop declarative specifications of objects, such specifications are then compiled down to control languages, and finally control programs are executed by fabrication devices to physically implement the design.

Given the rise of “desktop manufacturing” in the form of affordable 3D printers, laser cutters, and mini CNC mills, why does the design-to-prototype workflow still require so much expertise, tinkering, and failure?

We are trying to figure that out. Our key hypothesis is that “designs are just programs” and therefore we can bring all the powerful machinery of modern Programming Languages research to bear on the problem: synthesis, language design, and compiler optimizations all have a role to play.

In this talk, I will focus on our efforts to help users get more-editable designs out of the low-level representations commonly shared online. This “decompilation” starts with a description of an object’s surface as a set of triangles and ends up with high-level CAD program that parameterizes over repetitive design features. Along the way we’ll see some semantics for CAD, domain-specific heuristics for geometry synthesis, and some new techniques that extend equality saturation in addressing the dread “AC matching problem” that makes trouble for all kinds of automated solvers. We’ll highlight how the new egg egraph library enables new kinds of synthesis by specializing egraphs to equality saturation and enables greater flexibility via novel eclass analyses.

Bio:

Zachary Tatlock is an Associate Professor in the Allen School of Computer Science and Engineering at the University of Washington. He earned his PhD from UC San Diego under the brilliant guidance of Sorin Lerner. At UW, Zach tries to keep up with his students working on compilers and runtimes for machine learning frameworks, automatically addressing rounding error in numerical programs, exploring the practical limits of rewrite systems, and extending PL techniques to computational fabrication. He can juggle and solve Rubik’s cubes, but not at the same time.

Talk: