From cbfa7630c9a87cc7dd0693ddcab5f68cee34f4de Mon Sep 17 00:00:00 2001 From: odow Date: Fri, 2 Feb 2024 16:12:23 +1300 Subject: [PATCH 1/5] [Bridge] implement special case for x != y in CountDistinctToMILPBridge --- .../Constraint/bridges/count_distinct.jl | 116 +++++++++++++++++- test/Bridges/Constraint/count_distinct.jl | 49 +++++++- 2 files changed, 160 insertions(+), 5 deletions(-) diff --git a/src/Bridges/Constraint/bridges/count_distinct.jl b/src/Bridges/Constraint/bridges/count_distinct.jl index c4b4081f34..623d165fda 100644 --- a/src/Bridges/Constraint/bridges/count_distinct.jl +++ b/src/Bridges/Constraint/bridges/count_distinct.jl @@ -41,6 +41,24 @@ non-zero: n - \\sum\\limits_{j \\in \\bigcup_{i=1,\\ldots,d} S_i} y_{j} = 0 ``` +## Formulation (special case) + +In the special case that the constraint is `[2, x, y] in CountDistinct(3)`, then +the constraint is equivalent to `[x, y] in AllDifferent(2)`, which is equivalent +to `x != y`. + +```math +(x - y <= -1) \\vee (y - x <= -1) +``` +which is equivalent to (for suitable `M`): +```math +\\begin{aligned} +z \\in \\{0, 1\\} +x - y - M * z <= -1 \\\\ +y - x - M * (z - 1) <= -1 +\\end{aligned} +``` + ## Source node `CountDistinctToMILPBridge` supports: @@ -232,9 +250,105 @@ function MOI.Bridges.final_touch( bridge::CountDistinctToMILPBridge{T,F}, model::MOI.ModelLike, ) where {T,F} - S = Dict{T,Vector{MOI.VariableIndex}}() scalars = collect(MOI.Utilities.eachscalar(bridge.f)) bounds = Dict{MOI.VariableIndex,NTuple{2,T}}() + ret = MOI.Utilities.get_bounds(model, bounds, scalars[1]) + if MOI.output_dimension(bridge.f) == 3 && ret == (2.0, 2.0) + # The special case of + # [x, y] in AllDifferent() + # bridged to + # [2, x, y] in CountDistinct() + # This is equivalent to the NotEqualTo set. + _final_touch_not_equal_case(bridge, model, scalars) + else + _final_touch_general_case(bridge, model, scalars) + end + return +end + +function _final_touch_not_equal_case( + bridge::CountDistinctToMILPBridge{T,F}, + model::MOI.ModelLike, + scalars, +) where {T,F} + bounds = Dict{MOI.VariableIndex,NTuple{2,T}}() + new_bounds = false + for i in 2:length(scalars) + x = scalars[i] + ret = MOI.Utilities.get_bounds(model, bounds, x) + if ret === nothing + error( + "Unable to use CountDistinctToMILPBridge because element $i " * + "in the function has a non-finite domain: $x", + ) + end + if length(bridge.bounds) < i - 1 + # This is the first time calling final_touch + push!(bridge.bounds, ret) + new_bounds = true + elseif bridge.bounds[i-1] == ret + # We've called final_touch before, and the bounds match. No need to + # reformulate a second time. + continue + elseif bridge.bounds[i-1] != ret + # There is a stored bound, and the current bounds do not match. This + # means the model has been modified since the previous call to + # final_touch. We need to delete the bridge and start again. + MOI.delete(model, bridge) + MOI.Bridges.final_touch(bridge, model) + return + end + end + if !new_bounds + return + end + # [2, x, y] in CountDistinct() + # <--> + # x != y + # <--> + # {x - y >= 1} \/ {y - x >= 1} + # <--> + # {x - y <= -1} \/ {y - x <= -1} + # <--> + # {x - y - M * z <= -1} /\ {y - x - M * (z - 1) <= -1}, z in {0, 1} + z, _ = MOI.add_constrained_variable(model, MOI.ZeroOne()) + push!(bridge.variables, z) + x, y = scalars[2], scalars[3] + bx, by = bridge.bounds[1], bridge.bounds[2] + # {x - y - M * z <= -1}, M = u_x - l_y + M = bx[2] - by[1] + f = MOI.Utilities.operate(-, T, x, y) + push!( + bridge.less_than, + MOI.Utilities.normalize_and_add_constraint( + model, + MOI.Utilities.operate!(-, T, f, M * z), + MOI.LessThan(T(-1)); + allow_modify_function = true, + ), + ) + # {y - x - M * (z - 1) <= -1}, M = u_x - l_y + M = by[2] - bx[1] + g = MOI.Utilities.operate(-, T, y, x) + push!( + bridge.less_than, + MOI.Utilities.normalize_and_add_constraint( + model, + MOI.Utilities.operate!(-, T, g, M * z), + MOI.LessThan(T(-1 - M)); + allow_modify_function = true, + ), + ) + return +end + +function _final_touch_general_case( + bridge::CountDistinctToMILPBridge{T,F}, + model::MOI.ModelLike, + scalars, +) where {T,F} + S = Dict{T,Vector{MOI.VariableIndex}}() + bounds = Dict{MOI.VariableIndex,NTuple{2,T}}() for i in 2:length(scalars) x = scalars[i] ret = MOI.Utilities.get_bounds(model, bounds, x) diff --git a/test/Bridges/Constraint/count_distinct.jl b/test/Bridges/Constraint/count_distinct.jl index c342b5a174..054a0af1fc 100644 --- a/test/Bridges/Constraint/count_distinct.jl +++ b/test/Bridges/Constraint/count_distinct.jl @@ -61,21 +61,46 @@ function test_runtests_VectorOfVariables() return end +function test_runtests_VectorOfVariables_NotEqualTo() + MOI.Bridges.runtests( + MOI.Bridges.Constraint.CountDistinctToMILPBridge, + """ + variables: n, x, y + [n, x, y] in CountDistinct(3) + x in Interval(1.0, 4.0) + y >= 2.0 + y <= 5.0 + n == 2.0 + """, + """ + variables: n, x, y, z + 1.0 * x + -1.0 * y + -2.0 * z <= -1.0 + 1.0 * y + -1.0 * x + -4.0 * z <= -5.0 + x in Interval(1.0, 4.0) + y >= 2.0 + y <= 5.0 + n == 2.0 + z in ZeroOne() + """, + ) + return +end + function test_runtests_VectorAffineFunction() MOI.Bridges.runtests( MOI.Bridges.Constraint.CountDistinctToMILPBridge, """ - variables: x, y - [2.0, 2.0 * x + -1.0, y] in CountDistinct(3) + variables: d, x, y + [d, 2.0 * x + -1.0, y] in CountDistinct(3) x in Interval(1.0, 2.0) y >= 2.0 y <= 3.0 """, """ - variables: x, y, z_x1, z_x2, z_x3, z_y2, z_y3, a_1, a_2, a_3 + variables: d, x, y, z_x1, z_x2, z_x3, z_y2, z_y3, a_1, a_2, a_3 2.0 * x + -1.0 * z_x1 + -2.0 * z_x2 + -3.0 * z_x3 == 1.0 1.0 * y + -2.0 * z_y2 + -3.0 * z_y3 == 0.0 - a_1 + a_2 + a_3 == 2.0 + a_1 + a_2 + a_3 + -1.0 * d == 0.0 z_x1 + z_x2 + z_x3 == 1.0 z_y2 + z_y3 == 1.0 z_x1 + -1.0 * a_1 <= 0.0 @@ -146,6 +171,22 @@ function test_runtests_error_affine() return end +function test_resolve_with_modified_not_equal_to() + inner = MOI.Utilities.Model{Int}() + model = MOI.Bridges.Constraint.CountDistinctToMILP{Int}(inner) + x = MOI.add_variables(model, 3) + c = MOI.add_constraint.(model, x[2:3], MOI.Interval(0, 2)) + MOI.add_constraint(model, x[1], MOI.EqualTo(2)) + MOI.add_constraint(model, MOI.VectorOfVariables(x), MOI.CountDistinct(3)) + @test MOI.get(inner, MOI.NumberOfVariables()) == 3 + MOI.Bridges.final_touch(model) + @test MOI.get(inner, MOI.NumberOfVariables()) == 4 + MOI.set(model, MOI.ConstraintSet(), c[2], MOI.Interval(0, 1)) + MOI.Bridges.final_touch(model) + @test MOI.get(inner, MOI.NumberOfVariables()) == 4 + return +end + end # module TestConstraintCountDistinct.runtests() From 52baa2c699a9622692fe6a4e1d0595f61275ed36 Mon Sep 17 00:00:00 2001 From: odow Date: Fri, 2 Feb 2024 16:38:33 +1300 Subject: [PATCH 2/5] Fix --- src/Bridges/Constraint/bridges/count_distinct.jl | 4 ++-- test/Bridges/Constraint/count_distinct.jl | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Bridges/Constraint/bridges/count_distinct.jl b/src/Bridges/Constraint/bridges/count_distinct.jl index 623d165fda..ff81ed4a51 100644 --- a/src/Bridges/Constraint/bridges/count_distinct.jl +++ b/src/Bridges/Constraint/bridges/count_distinct.jl @@ -316,7 +316,7 @@ function _final_touch_not_equal_case( x, y = scalars[2], scalars[3] bx, by = bridge.bounds[1], bridge.bounds[2] # {x - y - M * z <= -1}, M = u_x - l_y - M = bx[2] - by[1] + M = bx[2] - by[1] + 1 f = MOI.Utilities.operate(-, T, x, y) push!( bridge.less_than, @@ -328,7 +328,7 @@ function _final_touch_not_equal_case( ), ) # {y - x - M * (z - 1) <= -1}, M = u_x - l_y - M = by[2] - bx[1] + M = by[2] - bx[1] + 1 g = MOI.Utilities.operate(-, T, y, x) push!( bridge.less_than, diff --git a/test/Bridges/Constraint/count_distinct.jl b/test/Bridges/Constraint/count_distinct.jl index 054a0af1fc..8502d56835 100644 --- a/test/Bridges/Constraint/count_distinct.jl +++ b/test/Bridges/Constraint/count_distinct.jl @@ -74,8 +74,8 @@ function test_runtests_VectorOfVariables_NotEqualTo() """, """ variables: n, x, y, z - 1.0 * x + -1.0 * y + -2.0 * z <= -1.0 - 1.0 * y + -1.0 * x + -4.0 * z <= -5.0 + 1.0 * x + -1.0 * y + -3.0 * z <= -1.0 + 1.0 * y + -1.0 * x + -5.0 * z <= -6.0 x in Interval(1.0, 4.0) y >= 2.0 y <= 5.0 From b3f8bbf912ce9625f3472118ab055008d0c77979 Mon Sep 17 00:00:00 2001 From: Oscar Dowson Date: Fri, 2 Feb 2024 17:22:21 +1300 Subject: [PATCH 3/5] Update src/Bridges/Constraint/bridges/count_distinct.jl --- src/Bridges/Constraint/bridges/count_distinct.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Bridges/Constraint/bridges/count_distinct.jl b/src/Bridges/Constraint/bridges/count_distinct.jl index ff81ed4a51..aed62f8115 100644 --- a/src/Bridges/Constraint/bridges/count_distinct.jl +++ b/src/Bridges/Constraint/bridges/count_distinct.jl @@ -53,7 +53,7 @@ to `x != y`. which is equivalent to (for suitable `M`): ```math \\begin{aligned} -z \\in \\{0, 1\\} +z \\in \\{0, 1\\} \\\\ x - y - M * z <= -1 \\\\ y - x - M * (z - 1) <= -1 \\end{aligned} From 36a0ff406da5278bf639d53bdfb9dc7ea86283cc Mon Sep 17 00:00:00 2001 From: Oscar Dowson Date: Sat, 3 Feb 2024 15:31:11 +1300 Subject: [PATCH 4/5] Apply suggestions from code review --- src/Bridges/Constraint/bridges/count_distinct.jl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Bridges/Constraint/bridges/count_distinct.jl b/src/Bridges/Constraint/bridges/count_distinct.jl index aed62f8115..f49c45a570 100644 --- a/src/Bridges/Constraint/bridges/count_distinct.jl +++ b/src/Bridges/Constraint/bridges/count_distinct.jl @@ -315,7 +315,7 @@ function _final_touch_not_equal_case( push!(bridge.variables, z) x, y = scalars[2], scalars[3] bx, by = bridge.bounds[1], bridge.bounds[2] - # {x - y - M * z <= -1}, M = u_x - l_y + # {x - y - M * z <= -1}, M = u_x - l_y + 1 M = bx[2] - by[1] + 1 f = MOI.Utilities.operate(-, T, x, y) push!( @@ -327,7 +327,7 @@ function _final_touch_not_equal_case( allow_modify_function = true, ), ) - # {y - x - M * (z - 1) <= -1}, M = u_x - l_y + # {y - x - M * (z - 1) <= -1}, M = u_x - l_y + 1 M = by[2] - bx[1] + 1 g = MOI.Utilities.operate(-, T, y, x) push!( From a95bf1a53ab49f2ab439272e6f45d953cd939f55 Mon Sep 17 00:00:00 2001 From: odow Date: Sat, 3 Feb 2024 15:40:34 +1300 Subject: [PATCH 5/5] Fix a silly mistake with z-1 instead of 1-z --- src/Bridges/Constraint/bridges/count_distinct.jl | 10 +++++----- test/Bridges/Constraint/count_distinct.jl | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Bridges/Constraint/bridges/count_distinct.jl b/src/Bridges/Constraint/bridges/count_distinct.jl index f49c45a570..fa4ce11f2f 100644 --- a/src/Bridges/Constraint/bridges/count_distinct.jl +++ b/src/Bridges/Constraint/bridges/count_distinct.jl @@ -55,7 +55,7 @@ which is equivalent to (for suitable `M`): \\begin{aligned} z \\in \\{0, 1\\} \\\\ x - y - M * z <= -1 \\\\ -y - x - M * (z - 1) <= -1 +y - x - M * (1 - z) <= -1 \\end{aligned} ``` @@ -310,7 +310,7 @@ function _final_touch_not_equal_case( # <--> # {x - y <= -1} \/ {y - x <= -1} # <--> - # {x - y - M * z <= -1} /\ {y - x - M * (z - 1) <= -1}, z in {0, 1} + # {x - y - M * z <= -1} /\ {y - x - M * (1 - z) <= -1}, z in {0, 1} z, _ = MOI.add_constrained_variable(model, MOI.ZeroOne()) push!(bridge.variables, z) x, y = scalars[2], scalars[3] @@ -327,15 +327,15 @@ function _final_touch_not_equal_case( allow_modify_function = true, ), ) - # {y - x - M * (z - 1) <= -1}, M = u_x - l_y + 1 + # {y - x - M * (1 - z) <= -1}, M = u_x - l_y + 1 M = by[2] - bx[1] + 1 g = MOI.Utilities.operate(-, T, y, x) push!( bridge.less_than, MOI.Utilities.normalize_and_add_constraint( model, - MOI.Utilities.operate!(-, T, g, M * z), - MOI.LessThan(T(-1 - M)); + MOI.Utilities.operate!(+, T, g, M * z), + MOI.LessThan(T(-1 + M)); allow_modify_function = true, ), ) diff --git a/test/Bridges/Constraint/count_distinct.jl b/test/Bridges/Constraint/count_distinct.jl index 8502d56835..d06cd33b20 100644 --- a/test/Bridges/Constraint/count_distinct.jl +++ b/test/Bridges/Constraint/count_distinct.jl @@ -75,7 +75,7 @@ function test_runtests_VectorOfVariables_NotEqualTo() """ variables: n, x, y, z 1.0 * x + -1.0 * y + -3.0 * z <= -1.0 - 1.0 * y + -1.0 * x + -5.0 * z <= -6.0 + 1.0 * y + -1.0 * x + 5.0 * z <= 4.0 x in Interval(1.0, 4.0) y >= 2.0 y <= 5.0