Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add := operator for Boolean satisfiability problems #3530

Merged
merged 8 commits into from
Oct 15, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions docs/src/developers/extensions.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
```

Expand Down
47 changes: 47 additions & 0 deletions docs/src/manual/constraints.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
35 changes: 35 additions & 0 deletions src/constraints.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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
42 changes: 42 additions & 0 deletions test/test_constraint.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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)
odow marked this conversation as resolved.
Show resolved Hide resolved
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
4 changes: 2 additions & 2 deletions test/test_macros.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
Loading