Skip to content

Commit

Permalink
fix tight_bound and maximum_ge (#56)
Browse files Browse the repository at this point in the history
**Bugfix**: In tight_bound, getobjectivebound was empirically observed not to return the correct objective bound when the objective is an affine expression with a constant term (the constant term was ignored). This could lead to correctness issues with the solver where problems that are SAT are incorrectly determined to be UNSAT because (for example) the lower or upper bounds to some ReLU input are too tight.

We believe that this is what is causing the following error message, since expect even LP solves to provide a better answer than interval arithmetic. We will increase the warning message to an error that stops optimization in the future.

```
Tightening via interval_arithmetic gives a better result than lp; using best bound found.
```

As a short-term fix, we fall back to bounds determined by interval arithmetic if this is the case.

**Perf**: In maximum_ge, we created additional continuous and binary variables even when the array we were maximizing over consisted of only a single entry. We fix this, allowing us to save on extraneous variables.
  • Loading branch information
vtjeng authored Jul 19, 2020
1 parent b6a585d commit c184f78
Showing 1 changed file with 13 additions and 11 deletions.
24 changes: 13 additions & 11 deletions src/net_components/core_ops.jl
Original file line number Diff line number Diff line change
Expand Up @@ -89,25 +89,24 @@ function tight_bound(
status = solve(model, suppress_warnings = true, relaxation = relaxation)
if status == :Optimal
b = getobjectivevalue(model)
db = bound_delta_f[bound_type](b, b_0)
Memento.debug(MIPVerify.LOGGER, " Δu = $(db)")
if db < 0
b = b_0
Memento.info(
MIPVerify.LOGGER,
"Tightening via interval_arithmetic gives a better result than $(tightening_algorithm); using best bound found.",
)
end
elseif status == :UserLimit
b = getobjectivebound(model)
log_gap(model)
b = b_0
else
Memento.warn(
MIPVerify.LOGGER,
"Unexpected solve status $(status) while tightening via $(tightening_algorithm); using interval_arithmetic to obtain upperbound.",
)
b = b_0
end
db = bound_delta_f[bound_type](b, b_0)
Memento.debug(MIPVerify.LOGGER, " Δu = $(db)")
if db < 0
b = b_0
Memento.info(
MIPVerify.LOGGER,
"Tightening via interval_arithmetic gives a better result than $(tightening_algorithm); using best bound found.",
)
end
return b
end

Expand Down Expand Up @@ -416,6 +415,9 @@ function maximum_ge(xs::AbstractArray{T})::JuMPLinearType where {T<:JuMPLinearTy
if all(is_constant.(xs))
return maximum_of_constants(xs)
end
if length(xs) == 1
return first(xs)
end
# at least one of xs is not constant.
model = MIPVerify.getmodel(xs)
x_max = @variable(model)
Expand Down

0 comments on commit c184f78

Please sign in to comment.