Feedback / improvements for the 5-houses puzzle model

Hello! (First of all, I’m unsure if this forum is a good place to ask for suggestions. Please redirect me somewhere if not :pray:)

I’m trying out Alloy 6, and as one of my first models I’ve been solving the Five houses puzzle. (I plan to try some of the temporal logic stuff next, and then go try it on some Actual Work Stuff :tm:.)

Here is my model:

sig House {
  position: one Position,
  color:    one Color,
  person:   one Person,
  drink:    one Drink,
  smoke:    one Smoke,
  pet:      one Pet,
  leftNeighbour:  lone House,
  rightNeighbour: lone House,

enum Color    { Red, White, Green, Yellow, Blue              }
enum Position { First, Second, Third, Fourth, Fifth          }
enum Person   { Brit, Swede, Dane, Norwegian, German         }
enum Drink    { Tea, Coffee, Milk, Beer, Water               }
enum Smoke    { PallMall, Dunhill, BlueMaster, Prince, Blend }
enum Pet      { Dogs, Birds, Cats, Horses, Fish              }

fact house_count { #House = 5 }

fact left_neighbours {
  all h1,h2: House |
    (h1.position = First  and h2.position = Second or
     h1.position = Second and h2.position = Third  or
     h1.position = Third  and h2.position = Fourth or
     h1.position = Fourth and h2.position = Fifth)
      iff h2.leftNeighbour = h1

fact right_neighbours { all h1,h2: House | h1.leftNeighbour = h2 implies h2.rightNeighbour = h1 }

fact all_distinct {
  all disj h1,h2: House | 
    h1.position != h2.position and
    h1.color    != h2.color    and
    h1.person   != h2.person   and
    h1.drink    != h2.drink    and
    h1.smoke    != h2.smoke    and      !=

fact hints {
  all h: House | 
    (h.person = Brit implies h.color = Red) and
    (h.person = Swede implies = Dogs) and
    (h.person = Dane implies h.drink = Tea) and
    (h.color = Green implies h.leftNeighbour.color = White) and
    (h.color = Green implies h.drink = Coffee) and
    (h.smoke = PallMall implies = Birds) and
    (h.color = Yellow implies h.smoke = Dunhill) and
    (h.position = Third implies h.drink = Milk) and
    (h.person = Norwegian implies h.position = First) and
    (h.smoke = Blend implies = Cats or = Cats) and
    ( = Horses implies h.leftNeighbour.smoke = Dunhill or h.rightNeighbour.smoke = Dunhill) and
    (h.smoke = BlueMaster implies h.drink = Beer) and
    (h.person = German implies h.smoke = Prince) and
    (h.person = Norwegian implies h.leftNeighbour.color = Blue or h.rightNeighbour.color = Blue) and
    (h.smoke = Blend implies h.leftNeighbour.drink = Water or h.rightNeighbour.drink = Water)

run {} for 5

It is working already! (In the sense that one of the valid instances is a solution to the puzzle.) But things could be improved.
Could you give me some feedback on better ways to represent aspects of the solution?

Things I’ve been struggling with

(sorry for imprecise descriptions of what went wrong - I mostly just remember “hm, that didn’t help”)

1. More succintly represent neighbours and facts about "exactly of the two neighbours is …"

Currently in the hints fact I need to do things like:

h.smoke = Blend implies = Cats or = Cats

This seems like it could be shortened to

h.smoke = Blend implies h.(leftNeighbour + rightNeighbour).pet = Cats

but that didn’t seem to help.

I’ve also tried to add a property to House:

neighbour: some House

combined with a fact:

neighbour = leftNeighbour + rightNeighbour

but this seemed to make things worse.

I’ve also tried to express it differently (it is neighbour if it is left neighbour or it is right neighbour) but didn’t succeed there either.
(I can try to give concrete Alloy code if needed, I don’t have those iterations saved anymore)

2. Somehow the rules about neighbours allow for loops / multiple left neighbours / being my own neighbour

Screenshot 2022-03-19 at 13.37.58

I’d have thought the rules left_neighbours and right_neighbours disallow this but apparently not. Any ideas on what I’m missing?

3. Somehow using relation arrows for First->Second->Third->Fourth->Fifth?

The rule left_neighbours seems quite wordy. Is there a way to express this order easier? I haven’t checked ordering module yet, I just know that it exists…

These are things I know about, but I’ll be glad if you point out more things to improve or aspects where you see my mental model about Alloy is wrong.

1 Like

Update: by trying to resolve the self-cycle I believe I’ve fixed most other non-symmetric neighbour relationships:

fact right_neighbours { all h1,h2: House | h1.leftNeighbour = h2 iff h2.rightNeighbour = h1 }

(changed from implies to iff)

I think your modeling style is essentially OK, even if there are other possible approaches. In my version of this problem, I had the following differences wrt your model:

First, houses are combined with their color, and similarly for persons with their nationality. I also moved some relations in Person.

abstract sig House { owner : one Person }
one sig Red, White, Green, Yellow, Blue extends House {}
abstract sig Person {
  drink:    one Drink,
  smoke:    one Smoke,
  pet:      one Pet, }
one sig Brit, Swede, Dane, Norwegian, German extends Person {}

Second, I specified that all fields are bijections (that is, they are one in both directions), e.g.:

fact {
  owner in House one -> Person
  drink in Person one -> Drink

Finally, I imposed a total order on House with open util/ordering[House]. This automatically adds various functions, such as first, prev and next (no need for a left or right neighbor function or field). Also, notice this module imposes an exact bound on house.

Alloy will infer by itself that the cardinality of House is 5 because it is abstract and extended by 5 one sigs.

Using all this eases the specification of constraints and the addition of a neighbors relation, e.g.:

fun neighbors : House -> House { next + prev }

fact hints {
  owner.Brit = Red = Dogs
  Green = White.prev

Hope this helps.
EDIT: rewrote the part on ordering and the scope of House (it was wrong as stated).

1 Like

Did you see Alloy model of the Einstein puzzle - Stack Overflow ?