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

And finally translate the A/B into proper CNF. The result seems very counterintuitive. At first glance it would appear to be contradictory and unworkable. At first glance it seems to suggest that both A and B need to be true and false at the same time. But it does work, and is actually saying "one or both must be true" and "one or both must be false," and equates to an XOR relationship. This is just one example of the little things you have to get used to when working with low-level SAT expressions.

Mail: (not shown)

Please type this: