Add := operator for Boolean satisfiability problems (#3530)

docs/src/developers/extensions.md

@@ -200,20 +200,20 @@ julia> model = Model(); @variable(model, x);
 
 julia> function JuMP.parse_constraint_head(
            _error::Function,
-           ::Val{:(:=)},
+           ::Val{:≔},
            lhs,
            rhs,
        )
-           println("Rewriting := as ==")
+           println("Rewriting ≔ as ==")
            new_lhs, parse_code = MutableArithmetics.rewrite(lhs)
            build_code = :(
                build_constraint($(_error), $(new_lhs), MOI.EqualTo($(rhs)))
            )
            return false, parse_code, build_code
        end
 
-julia> @constraint(model, x + x := 1.0)
-Rewriting := as ==
+julia> @constraint(model, x + x ≔ 1.0)
+Rewriting ≔ as ==
 2 x = 1
 ```
 

docs/src/manual/constraints.md

@@ -1534,3 +1534,50 @@ julia> q = [5, 6]
 julia> @constraint(model, M * y + q ⟂ y)
 [y[1] + 2 y[2] + 5, 3 y[1] + 4 y[2] + 6, y[1], y[2]] ∈ MathOptInterface.Complements(4)
 ```
+
+## Boolean constraints
+
+Add a Boolean constraint (a [`MOI.EqualTo{Bool}`](@ref) set) using the `:=`
+operator with a `Bool` right-hand side term:
+
+```jldoctest
+julia> model = GenericModel{Bool}();
+
+julia> @variable(model, x[1:2]);
+
+julia> @constraint(model, x[1] || x[2] := true)
+x[1] || x[2] = true
+
+julia> @constraint(model, x[1] && x[2] := false)
+x[1] && x[2] = false
+
+julia> model
+A JuMP Model
+Feasibility problem with:
+Variables: 2
+`GenericNonlinearExpr{GenericVariableRef{Bool}}`-in-`MathOptInterface.EqualTo{Bool}`: 2 constraints
+Model mode: AUTOMATIC
+CachingOptimizer state: NO_OPTIMIZER
+Solver name: No optimizer attached.
+Names registered in the model: x
+```
+
+Boolean constraints should not be added using the `==` operator because JuMP
+will rewrite the constraint as `lhs - rhs = 0`, and because constraints like
+`a == b == c` require parentheses to disambiguate between `(a == b) == c` and
+`a == (b == c)`. In contrast, `a == b := c` is equivalent to `(a == b) := c`:
+
+```jldoctest
+julia> model = Model();
+
+julia> @variable(model, x[1:2]);
+
+julia> rhs = false
+false
+
+julia> @constraint(model, (x[1] == x[2]) == rhs)
+(x[1] == x[2]) - 0.0 = 0
+
+julia> @constraint(model, x[1] == x[2] := rhs)
+x[1] == x[2] = false
+```

src/constraints.jl

@@ -1542,3 +1542,38 @@ function relax_with_penalty!(
 ) where {T}
     return relax_with_penalty!(model, Dict(); default = default)
 end
+
+struct _DoNotConvertSet{S} <: MOI.AbstractScalarSet
+    set::S
+end
+
+model_convert(::AbstractModel, set::_DoNotConvertSet) = set
+
+moi_set(c::ScalarConstraint{F,<:_DoNotConvertSet}) where {F} = c.set.set
+
+function _build_boolean_equal_to(::Function, lhs::AbstractJuMPScalar, rhs::Bool)
+    return ScalarConstraint(lhs, _DoNotConvertSet(MOI.EqualTo(rhs)))
+end
+
+function _build_boolean_equal_to(error_fn::Function, ::AbstractJuMPScalar, rhs)
+    return error_fn(
+        "cannot add the `:=` constraint. The right-hand side must be a `Bool`",
+    )
+end
+
+function _build_boolean_equal_to(error_fn::Function, lhs, ::Any)
+    return error_fn(
+        "cannot add the `:=` constraint with left-hand side of type `::$(typeof(lhs))`",
+    )
+end
+
+function parse_constraint_head(error_fn::Function, ::Val{:(:=)}, lhs, rhs)
+    new_lhs, parse_code_lhs = _rewrite_expression(lhs)
+    new_rhs, parse_code_rhs = _rewrite_expression(rhs)
+    parse_code = quote
+        $parse_code_lhs
+        $parse_code_rhs
+    end
+    build_code = :(_build_boolean_equal_to($error_fn, $new_lhs, $new_rhs))
+    return false, parse_code, build_code
+end

test/test_constraint.jl

@@ -1721,4 +1721,46 @@ function test_triangle_vec()
     return
 end
 
+function _test_def_equal_to_operator_T(::Type{T}) where {T}
+    model = GenericModel{T}()
+    @variable(model, x[1:3])
+    # x[1] := x[2]
+    @test_throws ErrorException @constraint(model, x[1] := x[2])
+    # x[1] == x[2] := false
+    c = @constraint(model, x[1] == x[2] := false)
+    o = constraint_object(c)
+    @test isequal_canonical(o.func, op_equal_to(x[1], x[2]))
+    @test o.set == MOI.EqualTo(false)
+    # x[1] && x[2] := false
+    c = @constraint(model, x[1] && x[2] := false)
+    o = constraint_object(c)
+    @test isequal_canonical(o.func, op_and(x[1], x[2]))
+    @test o.set == MOI.EqualTo(false)
+    # x[1] && x[2] := true
+    c = @constraint(model, x[1] && x[2] := true)
+    o = constraint_object(c)
+    @test isequal_canonical(o.func, op_and(x[1], x[2]))
+    @test o.set == MOI.EqualTo(true)
+    # x[1] || x[2] := y
+    y = true
+    c = @constraint(model, x[1] || x[2] := y)
+    o = constraint_object(c)
+    @test isequal_canonical(o.func, op_or(x[1], x[2]))
+    @test o.set == MOI.EqualTo(y)
+    # y := x[1] || x[2]
+    y = true
+    @test_throws ErrorException @constraint(model, y := x[1] || x[2])
+    return
+end
+
+function test_def_equal_to_operator_float()
+    _test_def_equal_to_operator_T(Float64)
+    return
+end
+
+function test_def_equal_to_operator_bool()
+    _test_def_equal_to_operator_T(Bool)
+    return
+end
+
 end

test/test_macros.jl

@@ -89,7 +89,7 @@ end
 
 struct CustomType end
 
-function JuMP.parse_constraint_head(_error::Function, ::Val{:(:=)}, lhs, rhs)
+function JuMP.parse_constraint_head(_error::Function, ::Val{:≔}, lhs, rhs)
     return false, :(), :(build_constraint($_error, $(esc(lhs)), $(esc(rhs))))
 end
 
@@ -326,7 +326,7 @@ function test_extension_custom_expression_test(
 )
     model = ModelType()
     @variable(model, x)
-    @constraint(model, con_ref, x := CustomType())
+    @constraint(model, con_ref, x ≔ CustomType())
     con = constraint_object(con_ref)
     @test jump_function(con) == x
     @test moi_set(con) isa CustomSet