Beginner: Four TreesSample answers

This puzzle introduces several features not present in the “integer” ones.

First, there is a defined sort. This means we can have variables ranging over the four trees, as well as variables ranging over integers. The tree names “ash”, “oak”, etc can be used in constraints just like “Able”, “Baker” and “Charlie” in the integer problems, but because they are given in an enumeration their interpretation is fixed. We call them the “canonical names” of the objects of the “tree” sort.

Next, we define some vocabulary. The function symbol “position” for instance, has no pre-defined interpretation: we want the solver to work out which function it represents. The declaration lays down that it applies to trees, and that its value for any given tree is an int. By declaring it to be “all_different”, we mean that no two trees can have the same position.

Next, note the way the predicate (or relation symbol) “adjacent” is used. It is a bit complicated to say that two trees are adjacent, as the first and last corners of the square are next to each other so it doesn’t just mean that the difference between positions is 1. By separating the constraint defining adjacency from the rest, we make it easier to read and write the specific clues.

Finally, this encoding nakes use of the keyword “ALL”, represented by the logical symbol “∀”. This is used to abbreviate constraints, so for instance instead of saying position(ash) is in the range 1..4 and so is position(oak) and so is position(elm) and so is position(fir), we simply say that the constraint holds of position(x), and stipulate that this holds for ALL values of the variable x.