always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] polish all-diff expansion heuristics; add warning when scaling floating point objective with high activity

Browse Source
This commit is contained in:
Laurent Perron
2023-01-23 13:19:54 +01:00
parent 873d832042
commit 0094ab9c88
3 changed files with 31 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
ortools/sat/cp_model_expand.cc
View File

@@ -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<int>& expand_all_diff,
absl::flat_hash_set<int>& 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;

1
ortools/sat/cp_model_presolve.cc
View File

@@ -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<int> new_variables(num_new_variables);

12
ortools/sat/lp_utils.cc
View File

@@ -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.