From a18d290bd740746048765a0536bcefb3d6ef6100 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 1 Sep 2021 11:53:03 +0200 Subject: [PATCH] [CP-SAT] fix more corner cases in checker and presolve --- ortools/sat/cp_model_checker.cc | 71 +++++++++++++++++++++++++++++++ ortools/sat/cp_model_expand.cc | 5 +-- ortools/sat/cp_model_postsolve.cc | 4 ++ ortools/sat/cp_model_presolve.cc | 18 +++++++- ortools/sat/intervals.cc | 15 ++++++- ortools/sat/intervals.h | 1 + ortools/sat/java/sat.i | 2 +- ortools/sat/sat_parameters.proto | 1 + 8 files changed, 109 insertions(+), 8 deletions(-) diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 90d6046c2e..220ca612e2 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -187,6 +187,51 @@ bool PossibleIntegerOverflow(const CpModelProto& model, return false; } +int64_t MinOfRef(const CpModelProto& model, int ref) { + const IntegerVariableProto& var_proto = model.variables(PositiveRef(ref)); + if (RefIsPositive(ref)) { + return var_proto.domain(0); + } else { + return -var_proto.domain(var_proto.domain_size() - 1); + } +} + +int64_t MaxOfRef(const CpModelProto& model, int ref) { + const IntegerVariableProto& var_proto = model.variables(PositiveRef(ref)); + if (RefIsPositive(ref)) { + return var_proto.domain(var_proto.domain_size() - 1); + } else { + return -var_proto.domain(0); + } +} + +template +int64_t MaxOfExpression(const CpModelProto& model, + const LinearExpressionProto& proto) { + int64_t sum_max = 0; + for (int i = 0; i < proto.vars_size(); ++i) { + const int ref = proto.vars(i); + const int64_t coeff = proto.coeffs(i); + sum_max = + CapAdd(sum_max, coeff >= 0 ? CapProd(MaxOfRef(model, ref), coeff) + : CapProd(MinOfRef(model, ref), coeff)); + } + + return sum_max; +} + +int64_t IntervalSizeMax(const CpModelProto& model, int interval_index) { + DCHECK_EQ(ConstraintProto::ConstraintCase::kInterval, + model.constraints(interval_index).constraint_case()); + const IntervalConstraintProto& proto = + model.constraints(interval_index).interval(); + if (proto.has_size_view()) { + return MaxOfExpression(model, proto.size_view()); + } else { + return MaxOfRef(model, proto.size()); + } +} + std::string ValidateLinearExpression(const CpModelProto& model, const LinearExpressionProto& expr) { if (expr.coeffs_size() != expr.vars_size()) { @@ -445,6 +490,17 @@ std::string ValidateCumulativeConstraint(const CpModelProto& model, } } + int64_t sum_max_demands = 0; + for (const int demand_ref : ct.cumulative().demands()) { + const int64_t demand_max = MaxOfRef(model, demand_ref); + DCHECK_GE(demand_max, 0); + sum_max_demands = CapAdd(sum_max_demands, demand_max); + if (sum_max_demands == std::numeric_limits::max()) { + return "The sum of max demands do not fit on an int64_t in constraint: " + + ProtobufDebugString(ct); + } + } + for (const LinearExpressionProto& expr : ct.cumulative().energies()) { const std::string error = ValidateLinearExpression(model, expr); if (!error.empty()) { @@ -464,6 +520,21 @@ std::string ValidateNoOverlap2DConstraint(const CpModelProto& model, return absl::StrCat("The two lists of intervals must have the same size: ", ProtobufShortDebugString(ct)); } + + // Checks if the sum of max areas of each rectangle can overflow. + int64_t sum_max_areas = 0; + for (int i = 0; i < ct.no_overlap_2d().x_intervals().size(); ++i) { + const int64_t max_size_x = + IntervalSizeMax(model, ct.no_overlap_2d().x_intervals(i)); + const int64_t max_size_y = + IntervalSizeMax(model, ct.no_overlap_2d().y_intervals(i)); + sum_max_areas = CapAdd(sum_max_areas, CapProd(max_size_x, max_size_y)); + if (sum_max_areas == std::numeric_limits::max()) { + return "Integer overflow when summing all areas in " + "constraint: " + + ProtobufDebugString(ct); + } + } return ""; } diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 3323a1e246..06f063394d 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -979,12 +979,9 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { std::vector tuple_literals; if (transition_values.size() == 1) { - bool tmp_removed_values = false; tuple_literals.push_back(context->GetOrCreateConstantVar(1)); - CHECK_EQ(reachable_states[time + 1].size(), 1); if (!context->IntersectDomainWith(vars[time], - Domain(transition_values.front()), - &tmp_removed_values)) { + Domain(transition_values.front()))) { VLOG(1) << "Infeasible automaton."; return; } diff --git a/ortools/sat/cp_model_postsolve.cc b/ortools/sat/cp_model_postsolve.cc index a673ec739c..7442169e1c 100644 --- a/ortools/sat/cp_model_postsolve.cc +++ b/ortools/sat/cp_model_postsolve.cc @@ -190,6 +190,10 @@ void PostsolveLinear(const ConstraintProto& ct, // We assign any non fixed lhs variables to their minimum value. Then we assign // the target to the max. This should always be feasible. +// +// Note(user): Our heuristic is not feasible if x = max(-x, ...) but we made +// sure we don't output such int_max here. Alternatively we could probably fix +// the code here. void PostsolveIntMax(const ConstraintProto& ct, std::vector* domains) { int64_t m = std::numeric_limits::min(); for (const int ref : ct.int_max().vars()) { diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index e0151fd9f9..97aadd526c 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -530,6 +530,7 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) { int64_t infered_min = std::numeric_limits::min(); int64_t infered_max = std::numeric_limits::min(); bool contains_target_ref = false; + bool contains_negated_target_ref = false; std::set used_ref; int new_size = 0; for (const int ref : ct->int_max().vars()) { @@ -539,6 +540,17 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) { ref == NegatedRef(target_ref)) { infered_min = std::max(infered_min, int64_t{0}); } + if (ref == NegatedRef(target_ref)) { + // x must be non-negative. + // It can be positive if they are other terms, otherwise it must be zero. + // TODO(user): more presolve in this case? + contains_negated_target_ref = true; + context_->UpdateRuleStats("int_max: x = max(-x, ...)"); + if (!context_->IntersectDomainWith( + target_ref, {0, std::numeric_limits::max()})) { + return false; + } + } used_ref.insert(ref); ct->mutable_int_max()->set_vars(new_size++, ref); infered_min = std::max(infered_min, context_->MinOf(ref)); @@ -548,6 +560,7 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) { context_->UpdateRuleStats("int_max: removed dup"); } ct->mutable_int_max()->mutable_vars()->Truncate(new_size); + if (contains_target_ref) { context_->UpdateRuleStats("int_max: x = max(x, ...)"); for (const int ref : ct->int_max().vars()) { @@ -584,7 +597,10 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) { // If the target is only used here and if // infered_domain ∩ [kint64min, target_ub] ⊂ target_domain // then the constraint is really max(...) <= target_ub and we can simplify it. - if (context_->VariableIsUniqueAndRemovable(target_ref)) { + // + // This is not as easy if x = max(-x, ...) so we skip this case. + if (context_->VariableIsUniqueAndRemovable(target_ref) && + !contains_negated_target_ref) { const Domain& target_domain = context_->DomainOf(target_ref); if (infered_domain .IntersectionWith(Domain(std::numeric_limits::min(), diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index 1a688db85a..1028c2716e 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -151,12 +151,23 @@ bool SchedulingConstraintHelper::UpdateCachedValues(int t) { IntegerValue smin = integer_trail_->LowerBound(starts_[t]); IntegerValue smax = integer_trail_->UpperBound(starts_[t]); - IntegerValue dmin = integer_trail_->LowerBound(sizes_[t]); - IntegerValue dmax = integer_trail_->UpperBound(sizes_[t]); IntegerValue emin = integer_trail_->LowerBound(ends_[t]); IntegerValue emax = integer_trail_->UpperBound(ends_[t]); + // We take the max for the corner case where the size of an optional interval + // is used elsewhere and has a domain with negative value. + // + // TODO(user): maybe we should just disallow size with a negative domain, but + // is is harder to enforce if we have a linear expression for size. + IntegerValue dmin = + std::max(IntegerValue(0), integer_trail_->LowerBound(sizes_[t])); + IntegerValue dmax = integer_trail_->UpperBound(sizes_[t]); + // Detect first if we have a conflict using the relation start + size = end. + if (dmax < 0) { + AddSizeMaxReason(t, dmax); + return PushTaskAbsence(t); + } if (smin + dmin - emax > 0) { ClearReason(); AddStartMinReason(t, smin); diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h index e8baac88e6..0cb430d9f1 100644 --- a/ortools/sat/intervals.h +++ b/ortools/sat/intervals.h @@ -546,6 +546,7 @@ inline void SchedulingConstraintHelper::AddSizeMinReason( int t, IntegerValue lower_bound) { AddOtherReason(t); DCHECK(!IsAbsent(t)); + if (lower_bound <= 0) return; AddGenericReason(sizes_[t].Negated(), -lower_bound, minus_ends_[t], starts_[t]); } diff --git a/ortools/sat/java/sat.i b/ortools/sat/java/sat.i index 5460a6f262..7619147498 100644 --- a/ortools/sat/java/sat.i +++ b/ortools/sat/java/sat.i @@ -91,7 +91,7 @@ PROTO2_RETURN(operations_research::sat::CpSolverResponse, $input_object_class, "accept", "(Ljava/lang/Object;)V"); assert($input_method_id != nullptr); - // When the lambda will be destroyed, input_guard's destructor will be call. + // When the lambda will be destroyed, input_guard's destructor will be called. $1 = [jvm, $input_object, $input_method_id, $input_guard]( const std::string& message) -> void { JNIEnv *jenv = NULL; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 613f77dd7f..0cd0a2474d 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -17,6 +17,7 @@ package operations_research.sat; option java_package = "com.google.ortools.sat"; option java_multiple_files = true; + option csharp_namespace = "Google.OrTools.Sat";