Out of Sorts (page 1)Really Advanced Topics
One of the frequently asked questions about our language for puzzle representation is “What is the difference between sorts and predicates?” In terms of the language syntax, there are many differences, starting with the fact that sort expressions are not allowed to occur in constraints, but in fact it turns out that, in a certain sense, sorts can be replaced by predicates. On this page we consider an example of how to do without them altogether.
Almost altogether, that is: we still need some sort because any model of anything requires a non-empty domain of things for the variables to range over. and we’ll need the special sort bool so that we can still write literals, but that will be all.
Here is the sample puzzle from which we are going to eliminate sorts:
THE LION AND THE UNICORN
Lions always tell the truth on Thursday to Sunday, and always lie on Monday to Wednesday. Unicorns are almost the exact opposite: they are truthful on Sunday, Monday, Tuesday and Wednesday but everything they say on Thursday, Friday or Saturday is false.
One day, the lion said to the unicorn, “I was a liar yesterday”. The unicorn replied, “So was I.”
What day was that?
Read through the encoding to the right, and make sure you see how the formulae express the problem. Then proceed to the next page…
Solver
Auto Parser Results
No errors found.