Sketch a SAT example

[fritzo]

pair coded with @eb8680

This attempts to implement answer set programming and a SAT example.

Blocking issues include:

• AdjointTape and Approximate seem a bit awkward in representing these abstractions. Maybe they conflate two concepts like (product of marginals, joint distributions); maybe we should separate those concepts.
• It would be nice to have a Stream funsor. Currently Funsor objects eagerly compute metadata, but a Stream would need lazily computed length. Thus as part of Support Python immutable datatypes without subclassing Funsor #526 we may want to make funsor.meta(-) lazier.
• This requires intricate use of Delta and we may want to first decide whether Scatter should replace Delta Replace Delta with Scatter? #528