diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 3e867addbb..77d9af3608 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -22,7 +22,6 @@ option java_package = "com.google.ortools.sat"; option java_multiple_files = true; option java_outer_classname = "CpModelProtobuf"; - // An integer variable. // // It will be referred to by an int32 corresponding to its index in a diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 125680ae27..7dcc7ebe12 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -661,6 +661,7 @@ std::vector GetDiverseSetOfParameters( } if (name == "less_encoding") continue; } else { + if (params.optimize_with_lb_tree_search()) continue; if (params.optimize_with_core()) continue; if (params.search_branching() == SatParameters::LP_SEARCH) continue; if (params.search_branching() == SatParameters::PSEUDO_COST_SEARCH) { diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 8c9978f7ed..3c5993d020 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -179,6 +179,7 @@ std::string CpModelStats(const CpModelProto& model_proto) { absl::btree_map name_to_num_literals; absl::btree_map name_to_num_terms; absl::btree_map name_to_num_complex_domain; + absl::btree_map name_to_num_expressions; int no_overlap_2d_num_rectangles = 0; int no_overlap_2d_num_optional_rectangles = 0; @@ -249,6 +250,9 @@ std::string CpModelStats(const CpModelProto& model_proto) { } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kExactlyOne) { name_to_num_literals[name] += ct.exactly_one().literals().size(); + } else if (ct.constraint_case() == + ConstraintProto::ConstraintCase::kLinMax) { + name_to_num_expressions[name] += ct.lin_max().exprs().size(); } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kNoOverlap2D) { const int num_boxes = ct.no_overlap_2d().x_intervals_size(); @@ -444,6 +448,10 @@ std::string CpModelStats(const CpModelProto& model_proto) { absl::StrAppend(&constraints.back(), " (#terms: ", name_to_num_terms[name], ")"); } + if (name_to_num_expressions.contains(name)) { + absl::StrAppend(&constraints.back(), + " (#expressions: ", name_to_num_expressions[name], ")"); + } if (name_to_num_complex_domain.contains(name)) { absl::StrAppend(&constraints.back(), " (#complex_domain: ", name_to_num_complex_domain[name], diff --git a/ortools/sat/integer_expr.h b/ortools/sat/integer_expr.h index bde56340d6..7fcf926a09 100644 --- a/ortools/sat/integer_expr.h +++ b/ortools/sat/integer_expr.h @@ -471,8 +471,8 @@ inline std::function WeightedSumLowerOrEqual( {}, local_vars, local_coeffs, IntegerValue(upper_bound), model); constraint->RegisterWith(model->GetOrCreate()); model->TakeOwnership(constraint); - return; } + return; } if (params.new_linear_propagation()) { diff --git a/ortools/sat/linear_propagation.cc b/ortools/sat/linear_propagation.cc index 25fd8cf10e..701494cf15 100644 --- a/ortools/sat/linear_propagation.cc +++ b/ortools/sat/linear_propagation.cc @@ -62,6 +62,7 @@ bool EnforcementPropagator::Propagate(Trail* /*trail*/) { } watch_list.resize(new_size); } + rev_num_enforced_ = static_cast(enforced_.size()); return true; } @@ -126,7 +127,17 @@ void EnforcementPropagator::CallWhenEnforced(EnforcementId id, // Returns true iff the constraint with given id is currently enforced. bool EnforcementPropagator::IsEnforced(EnforcementId id) const { - return is_enforced_[id]; + if (propagation_trail_index_ == trail_.Index()) return is_enforced_[id]; + + // TODO(user): In some corner case, when LinearPropagator pushes a literal + // we don't repropagate this right away. Maybe we should just simplify this + // class and just pay the O(num_enforcement_literal) cost. + // + // For now we pay the cost to catch bugs. + for (const Literal l : GetSpan(id)) { + if (!assignment_.LiteralIsTrue(l)) return false; + } + return true; } // Add the enforcement reason to the given vector. diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index 4e861b2820..447a680bed 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -991,36 +991,42 @@ void AppendLinMaxRelaxationPart2( // For the relaxation, we use different constraints with a stronger linear // relaxation as explained in the .h - // - // TODO(user): Consider passing the x_vars to this method instead of - // computing it here. - std::vector x_vars; - for (int i = 0; i < num_exprs; ++i) { - x_vars.insert(x_vars.end(), exprs[i].vars.begin(), exprs[i].vars.end()); - } - gtl::STLSortAndRemoveDuplicates(&x_vars); - - // All expressions should only contain positive variables. - DCHECK(std::all_of(x_vars.begin(), x_vars.end(), [](IntegerVariable var) { - return VariableIsPositive(var); - })); - std::vector> sum_of_max_corner_diff( num_exprs, std::vector(num_exprs, IntegerValue(0))); - IntegerTrail* integer_trail = model->GetOrCreate(); + // Cache coefficients. + absl::flat_hash_map, IntegerValue> cache; for (int i = 0; i < num_exprs; ++i) { - for (int j = 0; j < num_exprs; ++j) { - if (i == j) continue; - for (const IntegerVariable x_var : x_vars) { + for (int j = 0; j < exprs[i].vars.size(); ++j) { + cache[std::make_pair(i, exprs[i].vars[j])] = exprs[i].coeffs[j]; + } + } + const auto get_coeff = [&cache](IntegerVariable var, int index) { + const auto it = cache.find(std::make_pair(index, var)); + if (it == cache.end()) return IntegerValue(0); + return it->second; + }; + + IntegerTrail* integer_trail = model->GetOrCreate(); + std::vector active_vars; + for (int i = 0; i + 1 < num_exprs; ++i) { + for (int j = i + 1; j < num_exprs; ++j) { + active_vars = exprs[i].vars; + active_vars.insert(active_vars.end(), exprs[j].vars.begin(), + exprs[j].vars.end()); + gtl::STLSortAndRemoveDuplicates(&active_vars); + for (const IntegerVariable x_var : active_vars) { + const IntegerValue diff = get_coeff(x_var, j) - get_coeff(x_var, i); + if (diff == 0) continue; + const IntegerValue lb = integer_trail->LevelZeroLowerBound(x_var); const IntegerValue ub = integer_trail->LevelZeroUpperBound(x_var); - const IntegerValue diff = - GetCoefficient(x_var, exprs[j]) - GetCoefficient(x_var, exprs[i]); sum_of_max_corner_diff[i][j] += std::max(diff * lb, diff * ub); + sum_of_max_corner_diff[j][i] += std::max(-diff * lb, -diff * ub); } } } + for (int i = 0; i < num_exprs; ++i) { LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0)); lc.AddTerm(target, IntegerValue(1)); @@ -1153,7 +1159,7 @@ void TryToLinearizeConstraint(const CpModelProto& model_proto, if (linearization_level > 1) { if (is_affine_max) { AddMaxAffineCutGenerator(ct, model, relaxation); - } else { + } else if (ct.lin_max().exprs().size() < 100) { AddLinMaxCutGenerator(ct, model, relaxation); } } diff --git a/ortools/sat/model.h b/ortools/sat/model.h index 9696734535..1b3462b709 100644 --- a/ortools/sat/model.h +++ b/ortools/sat/model.h @@ -37,7 +37,7 @@ namespace sat { * Class that owns everything related to a particular optimization model. * * This class is actually a fully generic wrapper that can hold any type of - * constraints, watchers, solvers and provide a mecanism to wire them together. + * constraints, watchers, solvers and provide a mechanism to wire them together. */ class Model { public: diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 6c870a6e7b..df39c83eb4 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -20,7 +20,6 @@ option java_multiple_files = true; option csharp_namespace = "Google.OrTools.Sat"; - // Contains the definitions for all the sat algorithm parameters and their // default values. //