This project is a case study for domain-specific combinatorial sketching. Our immediate aim is to extend combinatorial sketching beyond small finite programs and into the domain of structured grid computations. More broadly, we expect to draw some lessons on how to build domain-specific sketching tools.

The programs in this domain produce an output grid as a function of one or more input grids and a few additional parameters. The programs must be able to handle grids of arbitrary sizes (sometimes in the billions of cells), and proving correctness only for a few small sizes may not be enough to guarantee correctness. For this reason, these programs can not be sketched using the simple combinatorial approach in SKETCH.

Our solution strategy is to reduce the original problem down to a small finite problem by taking advantage of domain specific properties. The reduced problem can then be resolved using the original combinatorial search, and the results are then mapped back to the original sketch to produce a full implementation. 

This is joint work Liviu Tacanu, Gilad Arnold and my advisor, Ras Bodik, in collaboration with Sanjit Seshia, Vijay Saraswat.