sat: do not remove an enforcement literal from incomplete activity bounds

[jipjan]

ActivityBoundHelper::RemoveEnforcementThatMakesConstraintTrivial() computes the min/max activity of a row's boolean terms under the assumption that one enforcement literal is false, and removes that literal when the resulting activity is included in the rhs — i.e. when the constraint holds anyway.

Two guards inside that loop announce that they abort:

      // This is not supposed to happen after PresolveEnforcement(), so we
      // just abort in this case.
      if (ref == enf_lit || ref == NegatedRef(enf_lit)) break;
...
      // Similarly, this is not supposed to happen after PresolveEnforcement().
      if (is_true && is_false) break;

but break only leaves the inner loop. Control still falls into

    if (Domain(min_activity, max_activity)
            .AdditionWith(other_terms)
            .IsIncludedIn(rhs)) {
      tmp_set_.insert(enf_lit);
    }

with min_activity / max_activity missing the contribution of every term after the break. Those bounds are not valid: the interval is too narrow, and if the accumulated max_activity is below min_activity the domain is empty, which IsIncludedIn() reports as included in anything. The enforcement literal is then removed, so enf => row silently becomes an unconditional row and every solution with enf false that did not satisfy the row is lost — a wrong optimum, or an infeasible answer on a satisfiable model.

This PR skips the test when either guard fired, which is what "abort" appears to have been intended to mean. No other behaviour changes.

Context

Found while root-causing #5293 (a certified-optimal answer 51 % above a verified feasible solution, on an all-linear 90'770-variable model). The actual cause of that issue is a different defect in the same function, which main has already fixed: non_amo_min_activity / non_amo_max_activity were int accumulating int64_t coefficients, so a boolean term above 2³¹ wrapped them. That is still int in the current release (v9.15) and int64_t on main.

So this PR is the remaining half. I have no model that triggers it — instrumenting v9.15 on my reproducer shows broke=0 on every removal, the overflow being the culprit there — so it is offered as a soundness fix for a path whose own comments say it should not be reached, rather than as a fix for an observed failure.

Testing

Compiled and run as part of a two-hunk patch on v9.15 (the function is otherwise identical there), against both the original 86'541-constraint model from #5293 and a 192-constraint delta-debugged version of it. Both give the correct optimum with default parameters, and the answers are unchanged by this hunk alone since it never fires on them.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.