kach/recreational-rosette

             o--o                        o                 o 
             |   |                       |  o              | 
             O-Oo  o-o  o-o o-o o-o  oo -o-   o-o o-o   oo | 
             |  \  |-' |    |   |-' | |  |  | | | |  | | | | 
             o   o o-o  o-o o   o-o o-o- o  | o-o o  o o-o-o 
                                                             
                                                             
                      o--o               o   o      
                      |   |              |   |      
                      O-Oo  o-o o-o o-o -o- -o- o-o 
                      |  \  | |  \  |-'  |   |  |-' 
                      o   o o-o o-o o-o  o   o  o-o 


In CS and in life, it is often easier to make the rules than it is to find a
way to follow them. It is much easier to explain the game of Sudoku to a
beginner than it is to solve a difficult puzzle yourself; it is much easier to
critique a dish than it is to cook; it is much easier to describe a good human
being than it is to be one.

Surprisingly, however, it turns out that sometimes a problem's description (in
the form of a solution-checking program) is all you need to get a solution! For
some problems, with some cleverness, we can automagically turn solution-checker
into a solution-finder; that is, we can turn a metaphorical critic into a
metaphorical chef.

Rosette [0] is a language in which we can define solution-checkers for our
problems. On the surface, a Rosette program is an ordinary Scheme (well,
Racket) program, and indeed you can run your Rosette program with a purported
"solution" to check whether or not it solves your problem.

The magic is that we can run Rosette programs without any input at all. Using
some clever tricks, Rosette can work backwards from your checker and invent a
brand-new input that will pass all of your checks. That is, once you have
written a Sudoku-checker, you can get a Sudoku-solver for free!

Internally, Rosette works by converting your Racket checks into a very large
Boolean circuit, and then using a highly-optimized SAT solver to find
true-or-false values for each variable in the circuit. Rosette then converts
the SAT solver's solution back into Racket-ey values.

Yes, there are scalability and efficiency concerns. Some problems are hard to
find solutions to. Some of those problems are inherently tricky -- you can't
reverse hashes with Rosette. Other problems can be rewritten to be easier for
Rosette to solve, though it may not be obvious how to do this.

But for small problems, this is rarely an issue! Computers are fast these days:
even an inefficient program to solve a small problem can run fast enough to be
practical. That is why I find Rosette exciting: because, at least in my toy
domains, it lets me think about programming as a way to specify a problem
rather than a solution.

This repository, then, contains some small examples of small problems, where a
small solution-checker is all that is needed to get Rosette to find a small
solution.

Enjoy!

[0] http://emina.github.io/rosette/