How to model an implication

Specific Domains Optimization (Mathematical)
17

There are many other possible formulations. It always helps to have some test cases that enumerate all possible values. Otherwise it can be very easy to make a logic mistake.

julia> using JuMP, HiGHS, Test

julia> function test_subproblem(build_fn; n, N)
           model = Model(HiGHS.Optimizer)
           set_silent(model)
           @variable(model, x[1:2, 1:n], Bin)
           @objective(model, Max, sum(x))
           build_fn(n, N, model, x)
           for y in Iterators.product(ntuple(i -> 0:1, n)...)
               if sum(y) != N
                   continue
               end
               @testset "$y" begin
                   fix.(x[1, :], y; force = true)
                   optimize!(model)
                   @test is_solved_and_feasible(model)
                   @test isapprox(sum(value.(x[2, :])), 2, atol = 1e-4)
               end
           end
           return
       end
test_subproblem (generic function with 1 method)

julia> function main(build_fn)
           @testset "main" begin
               @testset "$n-$N" for n in 2:10, N in 1:n
                   test_subproblem(build_fn; n, N)
               end
           end
           return
       end
main (generic function with 1 method)

julia> main() do n, N, model, x
           @variable(model, z[1:n], Bin)
           @constraint(model, sum(x[1, :]) == sum(i * z[i] for i in 1:n))
           @constraint(model, z[N] --> {sum(x[2, :]) == 2})
           @constraint(model, sum(z) <= 1)
       end
Test Summary: | Pass  Total  Time
main          | 4070   4070  0.3s

julia> main() do n, N, model, x
           @variable(model, z[1:3], Bin)
           @variable(model, 0 <= s[1:2] <= n)
           @constraint(model, [i in 1:2], s[i] <= n * z[i])
           @constraint(model, [i in 1:2], s[i] >= z[i])
           @constraint(model, z[3] == z[1] + z[2])
           @constraint(model, sum(x[1, :]) + s[1] - s[2] == N)
           @constraint(model, !z[3] --> {sum(x[2, :]) == 2})
       end
Test Summary: | Pass  Total  Time
main          | 4070   4070  0.4s