Add := operator for Boolean satisfiability problems

[odow]

x-ref #2227

This is one improvement suggested by today's call, motivated by the fact that == has lower precedence than && and ||, so x || y == true parses as x || (y == true). The new syntax, x || y := true parses as (x || y) := true.

The key difference of := compared with == is that == uses lhs - rhs in EqualTo(false), whereas := lowers to the NonlinearExpr (lhs == rhs) in EqualTo(true)`. Thus, it should pretty much only be used for Boolean problems that support ScalarNonlinearFunction.

cc @chriscoey thoughts?

See the examples in test/test_constraint.jl

TODO:

• Documentation

[codecov]

Codecov Report

All modified lines are covered by tests ✅

Comparison is base (4b5751c) 98.25% compared to head (fa07a0f) 98.26%.
Report is 8 commits behind head on master.

Additional details and impacted files

@@           Coverage Diff           @@
##           master    #3530   +/-   ##
=======================================
  Coverage   98.25%   98.26%           
=======================================
  Files          37       37           
  Lines        5563     5580   +17     
=======================================
+ Hits         5466     5483   +17     
  Misses         97       97           

Files	Coverage Δ
src/constraints.jl	96.78% <100.00%> (+0.20%)	⬆️

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[chriscoey]

Looks ok! No strong opinions from me. Thanks for experimenting.

[odow]

So this minizinc

var bool: x;
var bool: y;
constraint x - y == false;
solve maximize x + y;

makes the flatzinc

var bool: x:: output_var;
var bool: y:: output_var;
var 0..2: X_INTRODUCED_0_:: is_defined_var;
var 0..1: X_INTRODUCED_2_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_3_ ::var_is_introduced :: is_defined_var;
constraint int_eq(X_INTRODUCED_3_,X_INTRODUCED_2_);
constraint int_lin_eq([1,1,-1],[X_INTRODUCED_3_,X_INTRODUCED_2_,X_INTRODUCED_0_],0):: ctx_pos:: defines_var(X_INTRODUCED_0_);
constraint bool2int(y,X_INTRODUCED_2_):: defines_var(X_INTRODUCED_2_);
constraint bool2int(x,X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_);
solve  maximize X_INTRODUCED_0_;

So the minizinc compiler:

• Re-interprets bool variables as 0..1 integer variables
• Compiles x - y == false into x == y

I guess any arithmetic between bool is converted into integers.

I don't know what that means for us. But perhaps we don't need this special syntax.

[chriscoey]

Seems possibly inefficient... what if you make it a feasibility problem with no objective? I would expect a boolean interpretation to make more sense if the sub-solver is a SAT solver at least

[odow]

var bool: x;
var bool: y;
constraint x - y == false;
solve satisfy;

This is with Gecode

var bool: x:: output_var;
var bool: y:: output_var;
var 0..1: X_INTRODUCED_1_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_2_ ::var_is_introduced :: is_defined_var;
constraint int_eq(X_INTRODUCED_2_,X_INTRODUCED_1_);
constraint bool2int(y,X_INTRODUCED_1_):: defines_var(X_INTRODUCED_1_);
constraint bool2int(x,X_INTRODUCED_2_):: defines_var(X_INTRODUCED_2_);
solve  satisfy;

[odow]

There's also a general problem with VariableRef{Bool} and arithmetic:

julia> model = GenericModel{Bool}()
A JuMP Model
Feasibility problem with:
Variables: 0
Model mode: AUTOMATIC
CachingOptimizer state: NO_OPTIMIZER
Solver name: No optimizer attached.

julia> @variable(model, x[1:2])
2-element Vector{GenericVariableRef{Bool}}:
 x[1]
 x[2]

julia> x[1] - x[2]
ERROR: MethodError: no method matching _build_aff_expr(::Bool, ::Bool, ::GenericVariableRef{Bool}, ::Int64, ::GenericVariableRef{Bool})

Closest candidates are:
  _build_aff_expr(::V, ::V, ::K, ::V, ::K) where {V, K}
   @ JuMP ~/.julia/dev/JuMP/src/aff_expr.jl:87
  _build_aff_expr(::V, ::V, ::K) where {V, K}
   @ JuMP ~/.julia/dev/JuMP/src/aff_expr.jl:81

Stacktrace:
 [1] -(lhs::GenericVariableRef{Bool}, rhs::GenericVariableRef{Bool})
   @ JuMP ~/.julia/dev/JuMP/src/operators.jl:120
 [2] top-level scope
   @ REPL[14]:1

I think this just means that you can't write @constraint(model, x[1] == x[2]).

You have to write @constraint(model, (x[1] == x[2]) == true), which is an argument for @constraint(model, x[1] := x[2]).

[blegat]

Since we do it at the parsing level, it won't work if rhs is a Julia variable (not a JuMP decision variable) for which the value is a Bool right ?

[odow]

This part is at runtime. See the tests.

[blegat]

Ah indeed. I guess it's best to add code inside the build_constraint that add code that is generated by the macro if possible

[blegat]

But in this case, it might be difficult

[blegat]

We would need a new JuMP set Equal with and do build_constraint(error, (a, b), JuMP.Equal())

[mlubin]

The asymmetry of the symbol := is a bit annoying/misleading.

@constraint(model, x[1] || x[2] := y)

and

@constraint(model, y := x[1] || x[2])

should be equivalent, but superficially they don't seem to be.

[odow]

We could use ===, but that could be confusing with ==. The <--> syntax is used for reified constraints, which isn't quite the same.

Ideally, people would only write lhs := true or lhs := false.

[odow]

I had a play to try and come up with a better syntax, but I couldn't really think of anything

[pulsipher]

This would be helpful for defining logical constraints in DisjunctiveProgramming.jl.

[odow]

This would be helpful for defining logical constraints in DisjunctiveProgramming.jl.

Any syntax suggestions?

[pulsipher]

In our use case, it would seem unlikely to have anything beside a true or false on the RHS. In fact, I think we would throw an error if this is not the case. So, having an operator with high priority like := that allows us to avoid using parentheses would be ideal.

We would also prefer for logic constraints to have a distinct set type (not EqualTo) to easily distinguish them from equality constraints. If needed, we can overload build_constraint to accomplish this, since we use a different variable reference type for logical variables.

[odow]

But it'd be EqualTo{Bool}, is that not sufficient? Or I guess the problem is that model_convert would currently convert it to EqualTo{T}. But we could avoid that.

[odow]

Here are our options for operators with a higher precedence than || && == etc:
https://github.com/JuliaLang/julia/blob/342e39433c6f28ce0cbf7b6ad5478ab8a8ac2031/src/julia-parser.scm#L7-L13

  (append! (add-dots '(= += -= −= *= /= //= |\\=| ^= ÷= %= <<= >>= >>>= |\|=| &= ⊻= ≔ ⩴ ≕))
           (add-dots '(~))
           '(:= $=)))
;; comma - higher than assignment outside parentheses, lower when inside
(define prec-pair (add-dots '(=>)))
(define prec-conditional '(?))
(define prec-arrow       (add-dots '(← → ↔ ↚ ↛ ↞ ↠ ↢ ↣ ↦ ↤ ↮ ⇎ ⇍ ⇏ ⇐ ⇒ ⇔ ⇴ ⇶ ⇷ ⇸ ⇹ ⇺ ⇻ ⇼ ⇽ ⇾ ⇿ ⟵ ⟶ ⟷ ⟹ ⟺ ⟻ ⟼ ⟽ ⟾ ⟿ ⤀ ⤁ ⤂ ⤃ ⤄ ⤅ ⤆ ⤇ ⤌ ⤍ ⤎ ⤏ ⤐ ⤑ ⤔ ⤕ ⤖ ⤗ ⤘ ⤝ ⤞ ⤟ ⤠ ⥄ ⥅ ⥆ ⥇ ⥈ ⥊ ⥋ ⥎ ⥐ ⥒ ⥓ ⥖ ⥗ ⥚ ⥛ ⥞ ⥟ ⥢ ⥤ ⥦ ⥧ ⥨ ⥩ ⥪ ⥫ ⥬ ⥭ ⥰ ⧴ ⬱ ⬰ ⬲ ⬳ ⬴ ⬵ ⬶ ⬷ ⬸ ⬹ ⬺ ⬻ ⬼ ⬽ ⬾ ⬿ ⭀ ⭁ ⭂ ⭃ ⥷ ⭄ ⥺ ⭇ ⭈ ⭉ ⭊ ⭋ ⭌ ￩ ￫ ⇜ ⇝ ↜ ↝ ↩ ↪ ↫ ↬ ↼ ↽ ⇀ ⇁ ⇄ ⇆ ⇇ ⇉ ⇋ ⇌ ⇚ ⇛ ⇠ ⇢ ↷ ↶ ↺ ↻ --> <-- <-->)))

For ASCII operators, we really only have := or ~.

Is @constraint(model, x[1] || x[2] ~ y) and @constraint(model, true ~ x[1] || x[2]) to horrific? I guess so, because of bitwise-not.

[odow]

=== is ruled out because of

julia> dump(:(x == y === true))
Expr
  head: Symbol comparison
  args: Array{Any}((5,))
    1: Symbol x
    2: Symbol ==
    3: Symbol y
    4: Symbol ===
    5: Bool true

[pulsipher]

But it'd be EqualTo{Bool}, is that not sufficient? Or I guess the problem is that model_convert would currently convert it to EqualTo{T}. But we could avoid that.

Ya the automated conversion is what led to us to avoid using EqualTo since frequently for GDP problems T != Bool for the model.

For ASCII operators, we really only have := or ~.

Ya ~ doesn't seem a good choice. I think := makes the most sense and the asymmetry is fine for us since we want logical constraints of the form logical_proposition = RHS where RHS is either true or false.

[odow]

I've changed it so that := returns EqualTo{Bool}, even for other value type models.

I wonder if we should enforce that the func := rhs where rhs is a Bool, and not support others. Then we won't have the non-symmetric problem, and it's more obvious when to use := than ==.

[pulsipher]

I think restricting the RHS to be a Bool is for the best. It satisfies the use case for DisjunctiveProgramming and it aligns with @chriscoey's original idea of specifying logic constraints without a set (implying the RHS is true).

[odow]

Yeah, I've changed to only rhs Bool and it makes more sense.

[pulsipher]

This looks great.

[odow]

We may want to expose the _DoNotConvertSet as a public API, but that can wait for a request.