Now comes creating the CNF. We are going to cheat here a bit, because this is the really really hard part. You can derive it on your own, but I've made a library for you. One of the most useful functions is called
window(). It takes three arguments: a list of index positions, a minimum of positions to be true and a maximum of positions to be true. So by saying
window(positions, 1, 1) you generate a dozen logical clauses which force exactly one of the four terms to be true. Another function is called
write() and handles properly formatting everything.