Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

The board contains sixteen bits of information, each with a unique cartesian coordinate. Now, there is a problem. The SAT solver requires this be mapped onto a one dimensional array. We used to have to do this mapping manually, and it was the most complicated and error prone step of solving. Now there is an automatic term generator that transparently allocated slots on the 1D array and caches the information for re-use. It is called auto_term. But that is a little long (and it'll be called in nearly every line of code) so it is common to use a single-letter function name for it.

Mail: (not shown)

Please type this: