A monad for expressing SAT or QSAT problems using observable sharing. For example, we can express a full-adder with: Longer Examples Included are a couple of examples included with the distribution. Neither are as fast as a dedicated solver for their respective domains, but they showcase how you can solve real world problems involving 10s or 100s of thousands of variables and constraints with ersatz. This solves the "regular crossword puzzle" (grid.pdf) from the 2013 MIT mystery hunt. SPOILER