Something: examplesReally Advanced Topics

Often in logic puzzles we want to know the identity of a particular thing (such as “the driver” or whatever). As you have seen, the way to do this is to introduce it as a function symbol and write some clauses about it.

It can happen that a puzzle requires some item to satisfy a description but we don’t care which particular one. Perhaps one of the conditions is that “at least one of the dwarves has exactly 10 coins” but it does not matter which dwarf (or dwarves) that is. The natural way to express such a condition is to use the existential quantifier to say “SOME d (Coins(d) = 10)”, but if we wish to write everything in clause form, how do we proceed?

It’s exactly like asking for the driver’s name! Just declare a “nonce” constant and use it as a name in the clauses. Printing of the constant can be suppressed by putting “hidden” in the function description. This technique is particularly useful for saying that some universal condition does not hold. For instance, suppose we want to say that not all of the dwarves have the same number of coins. We can write this:

Sorts:

dwarf {cardinality = 7}

Vocabulary:

function Coins(dwarf): nat {}

name A: dwarf {hidden}

name B: dwarf {hidden}

Constraints:

Coins(x) > 0.

Coins(x) < 20.

Coins(A) < Coins(B).

Here we want to ensure that at least two of the hoards of coins are of different sizes (i.e. they are not all the same). So we declare A and B to be any two dwarves and stipulate that the number of coins of one is less than that of the other. To make things sensible, we might as well say that the numbers of coins are all positive and less than a reasonable upper bound (20, for instance). Note that the free variable x can be used to state this universal constraint.

Of course, there is no unique solution to this puzzle specification, since there are 893871720 ways of choosing the seven numbers so that at least two of them are different! If we run the solver on this, it will simply stop when it finds three solutions as usual.

Perhaps even more frequent in real problems is the case in which we need to say that for every thing of some kind there is some thing related to it in a given way. Examples are “Every metal has a melting point” or “Every phone has a number” or “Each dwarf has an axe”.

With quantifiers, it’s easy of course: “ALL x SOME y …”. In clause form, it’s not quite that simple. Our technique is an extension of the idea above. Instead of declaring constants like “A” and “B” above, we declare a function from metals to their melting points, phones to their numbers or dwarves to axes:

Vocabulary:

function MP(metal): temperature {hidden}

function N(phone): nat {hidden}

function Weapon(dwarf): axe {hidden}

We then write a clause,

m melts_at MP(m)

for instance, to say what the new function is for.

A dwarf d may have several axes, even though only one of them is picked out as Weapon(d), and perhaps several dwarves might share the same axe. On the other hand, each metal has exactly one melting point – though different metals may have the same one. The “number” function is more likely to be one-to-one. These are matters to be made explicit by adding more clauses as required.