Program synthesis for declarative building design
summary
Claims that program synthesis plus SMT makes parametric building design verifiable and automatable with concrete results: uses SMT solvers (Z3) and SAT/DPLL(T) extensions, embeds a geometry constraint solver, and rigs Rosette + Rhino for prototypes. Built examples include a solved Send+More+Money encoding and a trellis with mixed short/long beams that the solver finds configurations for. Works for toy problems but exposes real limits: encoding sensitivity, opaque performance swings, and uninterpretable unsat cores that hamper debugging.
AI-written summary · about
chapters (28)
- 0:00Introduction
- 0:14Agenda
- 0:38Shanghai Tower
- 1:34Buildings are important
- 2:27Architects and software engineers
- 2:43Architecture and construction
- 3:25Building code
- 4:17Parking
- 5:41Safety
- 6:26Exteriors
- 8:01Geometric constraint solving
- 10:26Building are largely geometric
- 10:36The problem is one of choice
- 12:26Boolean satisfiability
- 12:46Search problem
- 13:07Search algorithm
- 16:12Improvements
- 17:53Safety Glazing
- 18:38Satisfiability Modulo
- 20:50Theory solver
- 21:47Requirements
- 22:20DPL for theories
- 25:22Theories
- 26:24Purifying
- 30:25Rhino
- 32:50Trellis
- 36:31Challenges
- 38:11Resources
related talks
18mBodystorming Human-Robot Interactions
19mAssembly-aware Design of Printable Electromechanical Devices
43mProgramming Languages for the Future of Design Computation
30mUsing AI to Create Better Requirements and Designs
19mReprise: A Design Tool for Specifying, Generating, and Customizing 3D Printable Adaptations on ...
33mBuilding an Agentic Design System
49mSquish Meets Structure – Designing with Shoggoth
10mProgramming Space and Habitats