Alloy Practice Problem: Halmos’s Handshake Puzzle

The puzzle is about 5 couples. We’re going to single out one of the couples and call them Alice and Bob. The names don’t really matter so replace them with whatever names you think are appropriate. The puzzle is about shaking hands. Instead of spelling it out I’ll just present the Alloy model and call out the assumptions in the puzzle as they come up.

We are working with people and couples so let’s define those

// Don't know why ordering the couples speeds up the solution so much
open util/ordering[Couple]

// There are people and they can shake hands with other people
some sig Person { handshake: set Person }

// Alice and Bob are people
one sig Alice, Bob extends Person { }

// Couples consist of 2 different people
abstract sig Couple { a: Person, b: Person } {
  // No one is coupled to themselves
  a != b
  // All the couples are disjoint
  all c': Couple - this | no (a + b) & c'.(@a + @b)
  // Couples don't shake hands with each other
  (a -> b) not in handshake
}

// First couple C1 = Alice and Bob
one sig C1 extends Couple { } {
  a = Alice
  b = Bob
}

// Handshaking is symmetric but not reflexive
fact {
  no iden & handshake
  handshake = ~handshake
}

Like it says in the comment I have no idea idea why ordering the couples makes things faster but it does so it’s in there even though the ordering is not used. I think it’s because of symmetry breaking.

The assumptions are hopefully obvious. People can shake hands and shaking hands is a symmetric and non-reflexive relation, i.e. if A shakes hands with B then B shakes hands with A and no person shakes their own hand. Along with those restrictions we also assume people that are a couple don’t shake hands since they already know each other.

// Rest of the couples
one sig C2, C3, C4, C5 extends Couple { }

// Statement of the puzzle
pred puzzle() {
  all disj p, p': (Person - Alice) | #p.handshake != #p'.handshake
}

The statement of the puzzle is pretty simple. Alice goes around and asks everyone how many hands each person shook and she gets back 9 different answers so that’s what the above predicate encodes. We want to know how many hands Bob shook

run puzzle for 10 Person, 5 Int

I won’t spoil the answer. Presumably there is also a purely logical argument for finding the answer but I didn’t think up the logical argument because Alloy finds the answer in less than 200 milliseconds. If you think of the logical argument then let me know.