diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 3dbe93933d..473c067ebb 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -1831,6 +1831,19 @@ bool IsExprEqOrNeqValue(PresolveContext* context, return false; } +// This method will scan all constraints of all variables appearing in an +// all_diff. +// There are 3 outcomes: +// - expand to Boolean variables +// - keep integer all_different constraint (and cuts) +// - expand and keep. +// +// Expand is selected if the variable will be fully encoded (index of element, +// table, automaton...). +// Keep is forced is the variable appears in a linear equation with at least 3 +// terms, and with a tight domain ( == cst). +// If unknown, we rely on the AllDiffShouldBeExpanded() method that checks the +// size of the domain of the variables, and their numbers/ void ScanModelAndDecideAllDiffExpansion( PresolveContext* context, absl::flat_hash_set& expand_all_diff, absl::flat_hash_set& keep_all_diff) { @@ -1883,22 +1896,20 @@ void ScanModelAndDecideAllDiffExpansion( case ConstraintProto::ConstraintCase::kBoolXor: break; case ConstraintProto::ConstraintCase::kIntDiv: - bounds_are_used = true; break; case ConstraintProto::ConstraintCase::kIntMod: - bounds_are_used = true; break; case ConstraintProto::ConstraintCase::kLinMax: bounds_are_used = true; break; case ConstraintProto::ConstraintCase::kIntProd: - bounds_are_used = true; break; case ConstraintProto::ConstraintCase::kLinear: if (IsExprEqOrNeqValue(context, o.linear())) { // Encoding literals. domain_is_used = true; - } else if (o.linear().domain_size() == 2 && + } else if (o.linear().vars_size() > 2 && + o.linear().domain_size() == 2 && o.linear().domain(0) == o.linear().domain(1)) { // We assume all_diff cuts will only be useful if the linear // constraint has a fixed domain. @@ -1915,8 +1926,6 @@ void ScanModelAndDecideAllDiffExpansion( // Note: elements should have been expanded. if (o.element().index() == var) { domain_is_used = true; - } else { - bounds_are_used = true; } break; case ConstraintProto::ConstraintCase::kCircuit: @@ -1938,13 +1947,13 @@ void ScanModelAndDecideAllDiffExpansion( bounds_are_used = true; break; case ConstraintProto::ConstraintCase::kNoOverlap: - bounds_are_used = true; + // Will be covered by the interval case. break; case ConstraintProto::ConstraintCase::kNoOverlap2D: - bounds_are_used = true; + // Will be covered by the interval case. break; case ConstraintProto::ConstraintCase::kCumulative: - bounds_are_used = true; + // Will be covered by the interval case. break; case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET: break; diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 7c56d5f6a8..3ea18b6cda 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -2541,6 +2541,7 @@ bool CpModelPresolver::PresolveDiophantine(ConstraintProto* ct) { // TODO(user): Make sure the newly generated linear constraint // satisfy our no-overflow precondition on the min/max activity. // We should check that the model still satisfy conditions in + // 3/ortools/sat/cp_model_checker.cc;l=165;bpv=0 // Create new variables. std::vector new_variables(num_new_variables); diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc index a214e4f14b..b8776e6e26 100644 --- a/ortools/sat/lp_utils.cc +++ b/ortools/sat/lp_utils.cc @@ -1333,6 +1333,18 @@ bool ScaleAndSetObjective(const SatParameters& params, SOLVER_LOG(logger, "[Scaling] Objective scaling factor: ", scaling_factor / gcd); + if (scaled_sum_error / scaling_factor > wanted_precision) { + SOLVER_LOG(logger, + "[Scaling] Warning: the wort-case absolute error is greater " + "than the wanted precision (", + wanted_precision, + "). Try to increase mip_max_activity_exponent (default = ", + params.mip_max_activity_exponent(), + ") or reduced your variables range and/or objective " + "coefficient. We will continue the solve, but the final " + "objective value might be off."); + } + // Note that here we set the scaling factor for the inverse operation of // getting the "true" objective value from the scaled one. Hence the // inverse.