dpsanders / SatisfiabilityInterface.jl

MIT License
14 stars 6 forks source link

How to add `OR` constraints? #23

Open ericphanson opened 3 years ago

ericphanson commented 3 years ago

Is it possible to have constraints like x in 1:3 || y in 2:4?

julia> @variables x y
2-element Vector{Num}:
 x
 y

julia> x in 1:3 || y in 2:4
ERROR: TypeError: non-boolean (Num) used in boolean context
Stacktrace:
 [1] top-level scope
   @ REPL[232]:1

julia> x in 1:3 | y in 2:4
ERROR: MethodError: no method matching |(::Int64, ::Num)
Closest candidates are:
  |(::Any, ::Any, ::Any, ::Any...) at operators.jl:655
  |(::T, ::T) where T<:Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8} at int.jl:355
  |(::Num, ::Num) at /Users/eph/.julia/packages/Symbolics/H8dtg/src/num.jl:143
  ...
Stacktrace:
 [1] top-level scope
   @ REPL[233]:1

julia> (x in 1:3) + (y in 2:4) >= true # Symbolics accepts it!
(in(x, 1:3) + in(y, 2:4)) >= true

julia> DiscreteCSP([(x in 1:3) + (y in 2:4) >= true]) # but not DiscreteCSP

keys(domains) = Any[]
ERROR: KeyError: key in(x, 1:3) not found
Stacktrace:
 [1] getindex
   @ ./dict.jl:481 [inlined]
 [2] parse_expression(varmap::Dict{Any, Any}, ex::SymbolicUtils.Term{Real, Nothing})
   @ SatisfiabilityInterface ~/.julia/packages/SatisfiabilityInterface/bFdNP/src/relations.jl:206
 [3] DiscreteCSP(prob::ConstraintSatisfactionProblem)
   @ SatisfiabilityInterface ~/.julia/packages/SatisfiabilityInterface/bFdNP/src/relations.jl:388
 [4] DiscreteCSP(constraints::Vector{Num})
   @ SatisfiabilityInterface ~/.julia/packages/SatisfiabilityInterface/bFdNP/src/relations.jl:368
 [5] top-level scope
   @ REPL[235]:1
dpsanders commented 3 years ago

This would definitely be possible (and I think not too hard) , it's just not implemented yet! Would you like to make a PR?

dpsanders commented 3 years ago

Basically it just needs extending encode with a new method to handle |, I think.

dpsanders commented 2 years ago

I am no longer sure that this is so easy as I thought it was ;)

dpsanders commented 2 years ago

@ericphanson Do you still need this? Do you have a simple full example?

ericphanson commented 2 years ago

No, and I don’t even remember what I was doing back then 😅. I think maybe trying to model the resolver for Pkg…