The Einstein Riddle

From the web:
<<It’s famously known as the Einstein Riddle because it was supposedly created by Einstein as a young man for fun.

But there are some claims online that it actually was invented by the author of Alice’s Adventures in Wonderland, Lewis Carrol.

It’s highly unlikely that it was written by Einstein, but that doesn’t really matter.

There are 5 houses painted five different colors.
In each house lives a person with a different nationality.
These five owners drink a certain type of beverage, smoke a certain brand of cigar, and keep a certain pet.
No owners have the same pet, smoke the same brand of cigar, or drink the same beverage.

  1. The Brit lives in the red house
    
  2. The Swede keeps dogs as pets
    
  3. The Dane drinks tea
    
  4. The green house is on the left of the white house
    
  5. The person who smokes Pall Malls rears birds
    
  6. The owner of the yellow house smokes Dunhill
    
  7. The green house’s owner drinks coffee
    
  8. The man living in the center house drinks milk
    
  9. The Norwegian lives in the first (leftmost) house
    
  10. The man who smokes Blends lives next to the one who keeps cats
    
  11. The man who keeps horses lives next to the man who smokes Dunhill
    
  12. The owner who smokes BlueMaster drinks beer
    
  13. The German smokes Princes
    
  14. The Norwegian lives next to the blue house
    
  15. The man who smokes Blends has a neighbor who drinks water
    

Now to solve, tell me who owns the fish?
Exactly as stated on the website: I solved it, but it did take me a bit of scribbling on paper.
Then I thought if and how it was possible to make Julia do it.
I actually found it much less challenging to do with pen and paper, but in the end (after understanding the syntax of the @variableS macro, for example, one of the main difficulties) I managed to come up with a script that works (I think).

I still have doubts about the interpretation of rule 4 and whether it is possible to write the constraints I used in a more concise way.
I would also be curious to hear about different models of the problem

E.riddle
using JuMP
using HiGHS
using Random

begin
quiz5case = Model(HiGHS.Optimizer)
set_silent(quiz5case)
begin
N=shuffle(["NO","DK","UK","DE","SE"])
A=shuffle(["cats","horses","birds","fishs","dog"])
C=shuffle(["yellow","blue","red","green","white"])
D=shuffle(["water","the","milk","coffee","beer"])
S=shuffle(["Dunhill","Blends","PallMall","Prince","BlueMaster"])
end
@variables(quiz5case,begin
                xn[j in 1:5, k in N], Bin
                xa[j in 1:5, k in A], Bin
                xc[j in 1:5, k in C], Bin
                xd[j in 1:5, k in D], Bin
                xs[j in 1:5, k in S], Bin
end)


@constraints(quiz5case, begin

    [n in N], sum(xn[:,n])==1
    [a in A], sum(xa[:,a])==1
    [c in C], sum(xc[:,c])==1
    [d in D], sum(xd[:,d])==1
    [s in S], sum(xs[:,s])==1
    
    [i in 1:5], sum(xn[i,:])==1
    [i in 1:5], sum(xa[i,:])==1
    [i in 1:5], sum(xc[i,:])==1
    [i in 1:5], sum(xd[i,:])==1
    [i in 1:5], sum(xs[i,:])==1
    

    r1[i in 1:5], xn[i,"UK"]==xc[i,"red"]
    r2[i in 1:5], xn[i,"SE"]==xa[i,"dog"]
    r3[i in 1:5], xn[i,"DK"]==xd[i,"the"]
    #r4[i in 2:5], xc[i,"green"] .<= 1 .- xc[1:i-1,"white"]
    r4a, xc[5,"green"]==0
    r4b[i in 1:4], xc[i,"green"] <=  xc[i+1,"white"]
    r5[i in 1:5], xc[i,"green"]==xd[i,"coffee"]
    r6[i in 1:5], xs[i,"PallMall"]==xa[i,"birds"]
    r7[i in 1:5], xc[i,"yellow"]==xs[i,"Dunhill"]
    r8[i=3], xd[i,"milk"]==1
    r9[i=1], xn[i,"NO"]==1
    r10a[i =1], xs[i,"Blends"]<=xa[i+1,"cats"] 
    r10b[i=5], xs[i,"Blends"]<=xa[i-1,"cats"] 
    r10c[i in 2:4], xs[i,"Blends"]<=xa[i+1,"cats"] + xa[i-1,"cats"] 
    r11a[i=1], xs[i,"Dunhill"]<=xa[i+1,"horses"] 
    r11b[i=5], xs[i,"Dunhill"]<=xa[i-1,"horses"] 
    r11c[i in 2:4], xs[i,"Dunhill"]<=xa[i+1,"horses"] + xa[i-1,"horses"]
    r12[i in 1:5], xs[i,"BlueMaster"]==xd[i,"beer"] 
    r13[i in 1:5], xn[i,"DE"]==xs[i,"Prince"]
    r14a[i=1], xn[i,"NO"]<=xc[i+1,"blue"] 
    r14b[i=5], xn[i,"NO"]<=xc[i-1,"blue"] 
    r14c[i in 2:4], xn[i,"NO"]<=xc[i+1,"blue"] + xc[i-1,"blue"] 
    #r14[i=2], xc[i,"blue"]==1
    r15a[i=1], xs[i,"Blends"]<=xd[i+1,"water"] 
    r15b[i=5], xs[i,"Blends"]<=xd[i-1,"water"] 
    r15c[i in 2:4], xs[i,"Blends"]<=xd[i+1,"water"] + xd[i-1,"water"] 
end);


# 1. L’inglese vive in una casa rossa
# 2. Lo svedese ha un cane
# 3. Il danese beve the
# 4. La casa verde è a sinistra della casa bianca
# 5. Il padrone della casa verde beve caffè
# 6. La persona che fuma Pall Mall ha gli uccellini
# 7. Il padrone della casa gialla fuma sigarette Dunhill’s
# 8. L’uomo che vive nella casa centrale beve latte
# 9. Il norvegese vive nella prima casa
# 10. L’uomo che fuma Blends vive vicino a quello che ha i gatti
# 11. L’uomo che ha i cavalli vive vicino all’uomo che fuma le Dunhill’s
# 12. L’uomo che fuma le Blue Master beve birra
# 13. Il tedesco fuma le Prince
# 14. Il norvegese vive vicino alla casa blu
# 15. L’uomo che fuma le Blends ha un vicino che beve acqua

optimize!(quiz5case)
solution_summary(quiz5case)

f(x, R)=getindex.(Ref(R),[findfirst(==(1),r) for r in eachrow(x.data)])

permutedims(hcat([f(value.(x),R)  for (x,R) in zip([xn,xa,xc,xd,xs],[N,A,C,D,S])]...))

end

#  "NO"      "DE"     "SE"     "DK"      "UK"
#  "birds"   "fish"   "dog"    "cat"     "horse"
#  "green"   "blue"   "white"  "yellow"  "red"
#  "coffee"  "water"  "milk"   "the"     "beer"
#  "PM"      "Pr"     "Bl"     "Du"      "BM"

# "NO"      "DE"     "SE"      "UK"     "DK"
# "fish"    "cat"    "dog"     "horse"  "birds"
# "green"   "blue"   "yellow"  "red"    "white"
# "coffee"  "water"  "milk"    "beer"   "the"
# "Bl"      "Pr"     "Du"      "BM"     "PM"

# "NO"        "DE"      "SE"      "DK"       "UK"
# "birds"     "cats"    "dog"     "fishs"    "horses"
# "green"     "blue"    "white"   "yellow"   "red"
# "coffee"    "water"   "milk"    "the"      "beer"
# "PallMall"  "Prince"  "Blends"  "Dunhill"  "BlueMaster"


# green vicino white a sinistra
# "NO"       "DK"      "UK"        "DE"      "SE"
# "cats"     "horses"  "birds"     "fishs"   "dog"
# "yellow"   "blue"    "red"       "green"   "white"
# "water"    "the"     "milk"      "coffee"  "beer"
# "Dunhill"  "Blends"  "PallMall"  "Prince"  "BlueMaster"
possible objective function

This objective function would smooth out all interpretations of rule 4

@objective(quiz5case, Min, sum(xc[:,"white"].*[1:5...]) - sum(xc[:,"green"].*[1:5...]) )
8 Likes

Here’s how I solved your model. It might give you ideas:

using JuMP
import HiGHS
N = ["NO", "DK", "UK", "DE", "SE"]
A = ["cats", "horses", "birds", "fish", "dog"]
C = ["yellow", "blue", "red", "green", "white"]
D = ["water", "tea", "milk", "coffee", "beer"]
S = ["Dunhill", "Blends", "PallMall", "Prince", "BlueMaster"]
model = Model(HiGHS.Optimizer)
set_silent(model)
@variables(model,begin
    1 <= xn[N] <= 5, Int
    1 <= xa[A] <= 5, Int
    1 <= xc[C] <= 5, Int
    1 <= xd[D] <= 5, Int
    1 <= xs[S] <= 5, Int
end)
@constraints(model, begin
    xn in MOI.AllDifferent(5)
    xa in MOI.AllDifferent(5)
    xc in MOI.AllDifferent(5)
    xd in MOI.AllDifferent(5)
    xs in MOI.AllDifferent(5)
    # The Brit lives in the red house
    xn["UK"] == xc["red"]
    # The Swede keeps dogs as pets
    xn["SE"] == xa["dog"]
    # The Dane drinks tea
    xn["DK"] == xd["tea"]
    # The green house is on the left of the white house
    xc["green"] <= xc["white"]
    # The person who smokes Pall Malls rears birds
    xs["PallMall"] == xa["birds"]
    # The owner of the yellow house smokes Dunhill
    xc["yellow"] == xs["Dunhill"]
    # The green house’s owner drinks coffee
    xc["green"] == xd["coffee"]
    # The man living in the center house drinks milk
    xd["milk"] == 3
    # The Norwegian lives in the first (leftmost) house
    xn["NO"] == 1
    # The man who smokes Blends lives next to the one who keeps cats
    #   !!! note
    #       We want
    #           | xs["Blends"] - xa["cats"] | == 1
    #       This is tricky constraint, so we add
    #           | xs["Blends"] - xa["cats"] | <= 1
    #       and
    #           xs["Blends"] != xa["cats"]
    #       Since JuMP doesn't support `!=`, we use AllDifferent.
    -1 <= xs["Blends"] - xa["cats"] <= 1
    [xs["Blends"], xa["cats"]] in MOI.AllDifferent(2)
    # The man who keeps horses lives next to the man who smokes Dunhill
    -1 <= xa["horses"] - xs["Dunhill"] <= 1
    [xa["horses"], xs["Dunhill"]] in MOI.AllDifferent(2)
    # The owner who smokes BlueMaster drinks beer
    xs["BlueMaster"] == xd["beer"]
    # The German smokes Princes
    xn["DE"] == xs["Prince"]
    # The Norwegian lives next to the blue house
    -1 <= xn["NO"] - xc["blue"] <= 1
    [xn["NO"], xc["blue"]] in MOI.AllDifferent(2)
    # The man who smokes Blends has a neighbor who drinks water     
    -1 <= xs["Blends"] - xd["water"] <= 1
    [xs["Blends"], xd["water"]] in MOI.AllDifferent(2)
end);
optimize!(model)
@assert is_solved_and_feasible(model)
sort_values(x, keys) = keys[sortperm(round.(Int, value.(x).data))]
solution = hcat(
    1:5,
    sort_values(xn, N),
    sort_values(xa, A),
    sort_values(xc, C),
    sort_values(xd, D),
    sort_values(xs, S),
)

Yields:

5×6 Matrix{Any}:
 1  "NO"  "birds"   "green"   "coffee"  "PallMall"
 2  "DE"  "cats"    "blue"    "water"   "Prince"
 3  "UK"  "horses"  "red"     "milk"    "Blends"
 4  "DK"  "fish"    "yellow"  "tea"     "Dunhill"
 5  "SE"  "dog"     "white"   "beer"    "BlueMaster"
17 Likes

It seems clearer and more direct than mine.
How does the AllDifferent(n) constraint work?
Without going into too much detail, how is it implemented?

is it a set that contains all permutations of n elements?

I found (after several attempts) a way to summarize the rules.
Is it possible to replace the variable definition with a for loop?

quasi-short form

begin
    quiz5case = Model(HiGHS.Optimizer)
    set_silent(quiz5case)
    begin
    N=(["NO","DK","UK","DE","SE"])
    A=(["cats","horses","birds","fishs","dog"])
    C=(["yellow","blue","red","green","white"])
    D=(["water","the","milk","coffee","beer"])
    S=(["Dunhill","Blends","PallMall","Prince","BlueMaster"])
    end
    @variables(quiz5case,begin
                    xn[j in 0:6, k in N], Bin
                    xa[j in 0:6, k in A], Bin
                    xc[j in 0:6, k in C], Bin
                    xd[j in 0:6, k in D], Bin
                    xs[j in 0:6, k in S], Bin
                    
    end)

        [[@constraint(quiz5case,  sum(xe[:,e])==1) for e in E] for (xe,E)  in zip([xn,xa,xc,xd,xs],[N,A,C,D,S])]
        [[@constraint(quiz5case,  sum(xe[i,:])==1) for i in 1:5] for xe in [xn,xa,xc,xd,xs]]
        [[@constraint(quiz5case,  sum(xe[i,:])==0) for i in [0,6]] for xe in [xn,xa,xc,xd,xs]]
    @constraints(quiz5case, begin    
        r1[i in 1:5], xn[i,"UK"]==xc[i,"red"]
        r2[i in 1:5], xn[i,"SE"]==xa[i,"dog"]
        r3[i in 1:5], xn[i,"DK"]==xd[i,"the"]
        r4[i in 2:5], xc[i,"green"] .<= 1 .- xc[1:i-1,"white"]
        #  r4a, xc[5,"green"]==0
        #  r4b[i in 1:4], xc[i,"green"] <=  xc[i+1,"white"]
        r5[i in 1:5], xc[i,"green"]==xd[i,"coffee"]
        r6[i in 1:5], xs[i,"PallMall"]==xa[i,"birds"]
        r7[i in 1:5], xc[i,"yellow"]==xs[i,"Dunhill"]
        r8[i=3], xd[i,"milk"]==1
        r9[i=1], xn[i,"NO"]==1
        r10[i in 1:5], xs[i,"Blends"]<=xa[i+1,"cats"] + xa[i-1,"cats"] 
        r11[i in 1:5], xs[i,"Dunhill"]<=xa[i+1,"horses"] + xa[i-1,"horses"]
        r12[i in 1:5], xs[i,"BlueMaster"]==xd[i,"beer"] 
        r13[i in 1:5], xn[i,"DE"]==xs[i,"Prince"]
        r14[i in 1:5], xn[i,"NO"]<=xc[i+1,"blue"] + xc[i-1,"blue"] 
        r15[i in 1:5], xs[i,"Blends"]<=xd[i+1,"water"] + xd[i-1,"water"] 
    end);

    optimize!(quiz5case)
    solution_summary(quiz5case)
    
    f(x, R)=getindex.(Ref(R),[findfirst(==(1),r) for r in eachrow(x.data)[2:end-1]])
    
    permutedims(hcat([f(value.(x),R)  for (x,R) in zip([xn,xa,xc,xd,xs],[N,A,C,D,S])]...))
    
end

That’s actually not the correct solution. It comes down to some fuzzy language here:

The green house is on the left of the white house

In your constraints you interpreted that as “somewhere to the left”, but it should be read as “immediately to the left”. Some googling shows that many formulations of the Riddle have clarified it in this way (or “exactly on the left”). There is only a unique solution if those houses are specified to be next to each other.

1 Like

Ah, English :cry:

I guess we just want:

xc["green"] == xc["white"] - 1

How does the AllDifferent(n) constraint work?
is it a set that contains all permutations of n elements?

Not exactly. It enforces that every element in the vector must have a unique value, not necessarily the integers 1 to n.

Without going into too much detail, how is it implemented?

JuMP reformulates the problem into a MIP involving many binary variables.

Is it possible to replace the variable definition with a for loop?

To simplify, you could do:

using JuMP
import HiGHS
N = ["NO", "DK", "UK", "DE", "SE"]
A = ["cats", "horses", "birds", "fish", "dog"]
C = ["yellow", "blue", "red", "green", "white"]
D = ["water", "tea", "milk", "coffee", "beer"]
S = ["Dunhill", "Blends", "PallMall", "Prince", "BlueMaster"]
K  = union(N, A, C, D, S)
model = Model(HiGHS.Optimizer)
set_silent(model)
@variable(model, 1 <= x[K] <= 5, Int)
@constraints(model, begin
    [k in (N, A, C, D, S)], x[k] in MOI.AllDifferent(5)
    # The Brit lives in the red house
    x["UK"] == x["red"]
    # The Swede keeps dogs as pets
    x["SE"] == x["dog"]
    # The Dane drinks tea
    x["DK"] == x["tea"]
    # The green house is on the left of the white house
    x["green"] == x["white"] - 1
    # The person who smokes Pall Malls rears birds
    x["PallMall"] == x["birds"]
    # The owner of the yellow house smokes Dunhill
    x["yellow"] == x["Dunhill"]
    # The green house’s owner drinks coffee
    x["green"] == x["coffee"]
    # The man living in the center house drinks milk
    x["milk"] == 3
    # The Norwegian lives in the first (leftmost) house
    x["NO"] == 1
    # The man who smokes Blends lives next to the one who keeps cats
    #   !!! note
    #       We want
    #           | x["Blends"] - x["cats"] | == 1
    #       This is tricky constraint, so we add
    #           | x["Blends"] - x["cats"] | <= 1
    #       and
    #           x["Blends"] != x["cats"]
    #       Since JuMP doesn't support `!=`, we use AllDifferent.
    -1 <= x["Blends"] - x["cats"] <= 1
    [x["Blends"], x["cats"]] in MOI.AllDifferent(2)
    # The man who keeps horses lives next to the man who smokes Dunhill
    -1 <= x["horses"] - x["Dunhill"] <= 1
    [x["horses"], x["Dunhill"]] in MOI.AllDifferent(2)
    # The owner who smokes BlueMaster drinks beer
    x["BlueMaster"] == x["beer"]
    # The German smokes Princes
    x["DE"] == x["Prince"]
    # The Norwegian lives next to the blue house
    -1 <= x["NO"] - x["blue"] <= 1
    [x["NO"], x["blue"]] in MOI.AllDifferent(2)
    # The man who smokes Blends has a neighbor who drinks water     
    -1 <= x["Blends"] - x["water"] <= 1
    [x["Blends"], x["water"]] in MOI.AllDifferent(2)
end);
optimize!(model)
@assert is_solved_and_feasible(model)
sort_values(x, keys) = keys[sortperm(round.(Int, value.(x[keys]).data))]
solution = hcat(
    1:5,
    sort_values(x, N),
    sort_values(x, A),
    sort_values(x, C),
    sort_values(x, D),
    sort_values(x, S),
)

julia> solution
5×6 Matrix{Any}:
 1  "NO"  "cats"    "yellow"  "water"   "Dunhill"
 2  "DK"  "horses"  "blue"    "tea"     "Blends"
 3  "UK"  "birds"   "red"     "milk"    "PallMall"
 4  "DE"  "fish"    "green"   "coffee"  "Prince"
 5  "SE"  "dog"     "white"   "beer"    "BlueMaster"
1 Like

If I understand correctly, it’s not necessary to impose the “intergerness” constraint to solve this particular puzzle. What if another puzzle requires the solver to explicitly restrict the values to integers? How should that be expressed in JuMP?

1 Like

Thanks for your attention and time
Using integer variables in the 1:5 domain makes expressions clearer and more direct.
Using binary variables makes it easier to set the “near” constraint (taking advantage of the fact that there are 125 instead of 25 :laughing:)

In this case it doesn’t seem like a relevant feature, but in general from a performance point of view can one setting be expected to be preferable to the other (or does it depend on a case by case basis)?

vars BIN
using JuMP, HiGHS

begin
    quiz5case = Model(HiGHS.Optimizer)
    set_silent(quiz5case)
    dom=( N=["NO","DK","UK","DE","SE"],
    A=["cats","horses","birds","fishs","dog"],
    C=["yellow","blue","red","green","white"],
    D=["water","the","milk","coffee","beer"],
    S=["Dunhill","Blends","PallMall","Prince","BlueMaster"])

    @variables(quiz5case,begin
        xn[j in 0:6, k in dom.N], Bin
        xa[j in 0:6, k in dom.A], Bin
        xc[j in 0:6, k in dom.C], Bin
        xd[j in 0:6, k in dom.D], Bin
        xs[j in 0:6, k in dom.S], Bin           
    end)

    [[@constraint(quiz5case,  sum(xe[:,e])==1) for e in E] for (xe,E)  in zip([xn,xa,xc,xd,xs],dom)]
    [[@constraint(quiz5case,  sum(xe[i,:])==(mod1(i,6)<6)) for i in 0:6] for xe in [xn,xa,xc,xd,xs]]

    @constraints(quiz5case, begin    
        r1[i in 1:5], xn[i,"UK"]==xc[i,"red"]
        r2[i in 1:5], xn[i,"SE"]==xa[i,"dog"]
        r3[i in 1:5], xn[i,"DK"]==xd[i,"the"]
        r4[i in 1:5], xc[i,"green"] <=  xc[i+1,"white"]
        r5[i in 1:5], xc[i,"green"]==xd[i,"coffee"]
        r6[i in 1:5], xs[i,"PallMall"]==xa[i,"birds"]
        r7[i in 1:5], xc[i,"yellow"]==xs[i,"Dunhill"]
        r8[i=[3]], xd[i,"milk"]==1
        r9[i=[1]], xn[i,"NO"]==1
        r10[i in 1:5], xs[i,"Blends"]<=xa[i+1,"cats"] + xa[i-1,"cats"] 
        r11[i in 1:5], xs[i,"Dunhill"]<=xa[i+1,"horses"] + xa[i-1,"horses"]
        r12[i in 1:5], xs[i,"BlueMaster"]==xd[i,"beer"] 
        r13[i in 1:5], xn[i,"DE"]==xs[i,"Prince"]
        r14[i in 1:5], xn[i,"NO"]<=xc[i+1,"blue"] + xc[i-1,"blue"] 
        r15[i in 1:5], xs[i,"Blends"]<=xd[i+1,"water"] + xd[i-1,"water"] 
    end);

    
    optimize!(quiz5case)

    f(x, R)=getindex.(Ref(R),[findfirst(==(1),r) for r in eachrow(x.data)[2:end-1]])
    
    hcat([f(value.(x),R)  for (x,R) in zip([xn,xa,xc,xd,xs],dom)]...)
    
end
1 Like

it’s not necessary to impose the “intergerness” constraint to solve this particular puzzle

It is necessary. See the Int restriction in @variable(model, 1 <= x[K] <= 5, Int).

but in general from a performance point of view can one setting be expected to be preferable to the other (or does it depend on a case by case basis)

It depends on a case-by-case basis.

1 Like

Not knowing the meaning of the acronym MIP, I went looking for information on the topic and on the specific aspect of imposing the uniqueness of the group of variables.
I found many (too specialized for my capabilities) publications but also these very clear answers by Erick Wong.
Does AllDistinct(k) use similar techniques?

It’s mixed-integer program:

1 Like

Does AllDistinct(k) use similar techniques?

Yes, MOI.AllDifferent ends up doing a binary expansion such that no two values can take the same.

Consider:

julia> using JuMP, HiGHS

julia> model = Model(HiGHS.Optimizer)
A JuMP Model
Feasibility problem with:
Variables: 0
Model mode: AUTOMATIC
CachingOptimizer state: EMPTY_OPTIMIZER
Solver name: HiGHS

julia> @variable(model, 1 <= x[1:3] <= 3, Int)
3-element Vector{VariableRef}:
 x[1]
 x[2]
 x[3]

julia> @constraint(model, x in MOI.AllDifferent(3))
[x[1], x[2], x[3]] ∈ MathOptInterface.AllDifferent(3)

julia> MOI.Utilities.attach_optimizer(model)
Running HiGHS 1.7.0 (git hash: 50670fd4c): Copyright (c) 2024 HiGHS under MIT licence terms

julia> print_active_bridges(model)
 * Supported objective: MOI.ScalarAffineFunction{Float64}
 * Supported constraint: MOI.VariableIndex-in-MOI.GreaterThan{Float64}
 * Supported constraint: MOI.VariableIndex-in-MOI.Integer
 * Supported constraint: MOI.VariableIndex-in-MOI.LessThan{Float64}
 * Unsupported constraint: MOI.VectorOfVariables-in-MOI.AllDifferent
 |  bridged by:
 |   MOIB.Constraint.AllDifferentToCountDistinctBridge{Float64, MOI.VectorOfVariables}
 |  may introduce:
 |   * Unsupported constraint: MOI.VectorOfVariables-in-MOI.CountDistinct
 |   |  bridged by:
 |   |   MOIB.Constraint.CountDistinctToMILPBridge{Float64, MOI.VectorOfVariables}
 |   |  may introduce:
 |   |   * Supported constraint: MOI.ScalarAffineFunction{Float64}-in-MOI.EqualTo{Float64}
 |   |   * Supported constraint: MOI.ScalarAffineFunction{Float64}-in-MOI.LessThan{Float64}
 |   |   * Supported variable: MOI.ZeroOne
 |   * Supported variable: MOI.EqualTo{Float64}

julia> print(unsafe_backend(model))
Feasibility

Subject to:

VariableIndex-in-EqualTo{Float64}
 v[4] == 3.0

ScalarAffineFunction{Float64}-in-LessThan{Float64}
 0.0 + 1.0 v[5] + 1.0 v[8] + 1.0 v[11] - 3.0 v[14] <= 0.0
 0.0 - 1.0 v[5] - 1.0 v[8] - 1.0 v[11] + 1.0 v[14] <= 0.0
 0.0 + 1.0 v[6] + 1.0 v[9] + 1.0 v[12] - 3.0 v[15] <= 0.0
 0.0 - 1.0 v[6] - 1.0 v[9] - 1.0 v[12] + 1.0 v[15] <= 0.0
 0.0 + 1.0 v[7] + 1.0 v[10] + 1.0 v[13] - 3.0 v[16] <= 0.0
 0.0 - 1.0 v[7] - 1.0 v[10] - 1.0 v[13] + 1.0 v[16] <= 0.0

VariableIndex-in-ZeroOne
 v[5] ∈ {0, 1}
 v[6] ∈ {0, 1}
 v[7] ∈ {0, 1}
 v[8] ∈ {0, 1}
 v[9] ∈ {0, 1}
 v[10] ∈ {0, 1}
 v[11] ∈ {0, 1}
 v[12] ∈ {0, 1}
 v[13] ∈ {0, 1}
 v[14] ∈ {0, 1}
 v[15] ∈ {0, 1}
 v[16] ∈ {0, 1}

VariableIndex-in-LessThan{Float64}
 x[1] <= 3.0
 x[2] <= 3.0
 x[3] <= 3.0

VariableIndex-in-Integer
 x[1] ∈ ℤ
 x[2] ∈ ℤ
 x[3] ∈ ℤ

ScalarAffineFunction{Float64}-in-EqualTo{Float64}
 0.0 + 1.0 x[1] - 1.0 v[5] - 2.0 v[6] - 3.0 v[7] == 0.0
 0.0 + 1.0 v[5] + 1.0 v[6] + 1.0 v[7] == 1.0
 0.0 + 1.0 x[2] - 1.0 v[8] - 2.0 v[9] - 3.0 v[10] == 0.0
 0.0 + 1.0 v[8] + 1.0 v[9] + 1.0 v[10] == 1.0
 0.0 + 1.0 x[3] - 1.0 v[11] - 2.0 v[12] - 3.0 v[13] == 0.0
 0.0 + 1.0 v[11] + 1.0 v[12] + 1.0 v[13] == 1.0
 0.0 - 1.0 v[4] + 1.0 v[14] + 1.0 v[15] + 1.0 v[16] == 0.0

VariableIndex-in-GreaterThan{Float64}
 x[1] >= 1.0
 x[2] >= 1.0
 x[3] >= 1.0

The reformulation uses the MOIB.Constraint.AllDifferentToCountDistinctBridge, followed by MOIB.Constraint.CountDistinctToMILPBridge, and introduces some binary variables, = constraints, and <= constraints.

The underlying HiGHS model has constraints like:

 0.0 + 1.0 x[1] - 1.0 v[5] - 2.0 v[6] - 3.0 v[7] == 0.0

or put more nicely:

x[1] == 1 * v[5] + 2 * v[6] + 3 * v[7]

and there is a constraint that exactly one of these binary variables must be chosen:

 0.0 + 1.0 v[5] + 1.0 v[6] + 1.0 v[7] == 1.0

If you follow the rest of the constraints, you should be able to see how they enforce that exactly three unique values of the binary variables are chosen. (Note that v[4] == 3.0)

1 Like