Einstein's Riddle (Alloy Solution)

einsteinsRiddle.als

open util/ordering[House]
  
enum Color {Red, White, Blue, Green, Yellow}
enum Pet {Birds, Cats, Dogs, Fish, Horses}
enum Cigar {Blend, BlueMaster, Dunhill, PallMall, Prince}
enum Beverage {Beer, Coffee, Milk, Tea, Water}

sig House {
    color: disj Color
}

abstract sig Owner {
    house: disj House,
    pet: disj Pet,
    cigar: disj Cigar,
    beverage: disj Beverage
}

one sig Brit extends Owner {}
one sig Swede extends Owner {}
one sig Dane extends Owner {}
one sig Norwegian extends Owner {}
one sig German extends Owner {}

fact constraints {
    one b: Brit | b.house.color = Red
    one s: Swede | s.pet = Dogs
    one d: Dane | d.beverage = Tea

    // The Green house is exactly to the left of the White house.
    one disj h1, h2: House | h1.next = h2 && h1.color = Green && h2.color = White

    // The owner of the Green house drinks Coffee.
    one p: Owner | p.house.color = Green && p.beverage = Coffee

    // The person who smokes Pall Mall rears Birds.
    one p: Owner | p.cigar = PallMall && p.pet = Birds

    // The owner of the Yellow house smokes Dunhill.
    one p:Owner | p.house.color = Yellow && p.cigar = Dunhill

    // The man living in the centre house drinks Milk.
    one p: Owner | p.house = first.next.next && p.beverage = Milk

    // The man who smokes Blends lives next to the one who keeps Cats.
    one p1, p2: Owner | p1.cigar = Blend && p2.pet = Cats && p1.house = p2.house.next

    // The man who keeps Horses lives next to the man who smokes Dunhill.
    one p1, p2: Owner | p1.pet = Horses && p2.cigar = Dunhill && (p2.house.next = p1.house || p2.house.prev = p1.house)

    // The man who smokes Blue Master drinks Beer.
    one p: Owner | p.cigar = BlueMaster && p.beverage = Beer

    // German smokes Prince
    one g: German | g.cigar = Prince

    // 1) The Norwegian lives in the first house. 2) The Norwegian lives next to the Blue house.
    one n: Norwegian, h: House | h.color = Blue && n.house = first && n.house = h.prev

    // The man who smokes Blends has a neighbour who drinks Water.
    one p1, p2: Owner | p1.cigar = Blend && p2.beverage = Water && (p1.house = p2.house.next || p1.house = p2.house.prev)
    
    #House = 5
}

run {} for 5