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.