SAT


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

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.

Name:
Mail: (not shown)

Please type this: