diff --git a/ortools/sat/2d_rectangle_presolve_test.cc b/ortools/sat/2d_rectangle_presolve_test.cc index 7650f9bb27..205ea18ff0 100644 --- a/ortools/sat/2d_rectangle_presolve_test.cc +++ b/ortools/sat/2d_rectangle_presolve_test.cc @@ -702,7 +702,7 @@ ShapePath TraceBoundary( std::string RenderShapes(std::optional bb, absl::Span rectangles, - const std::vector& shapes) { + absl::Span shapes) { const std::vector colors = {"black", "white", "orange", "cyan", "yellow", "purple"}; std::stringstream ss; diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 464f42427e..7d30fd7af6 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -949,6 +949,7 @@ cc_library( "//ortools/util:logging", "//ortools/util:sorted_interval_list", "@com_google_absl//absl/log:check", + "@com_google_absl//absl/types:span", ], ) @@ -1442,6 +1443,7 @@ cc_library( ":cp_model_cc_proto", ":cp_model_utils", ":integer", + ":integer_base", ":presolve_context", ":presolve_util", ":util", @@ -1469,7 +1471,7 @@ cc_test( srcs = ["var_domination_test.cc"], deps = [ ":cp_model_cc_proto", - ":integer", + ":integer_base", ":model", ":presolve_context", ":var_domination", @@ -3207,6 +3209,7 @@ cc_library( "@com_google_absl//absl/container:flat_hash_set", "@com_google_absl//absl/log:check", "@com_google_absl//absl/meta:type_traits", + "@com_google_absl//absl/types:span", ], ) diff --git a/ortools/sat/all_different.cc b/ortools/sat/all_different.cc index dbcd749955..739b8870f6 100644 --- a/ortools/sat/all_different.cc +++ b/ortools/sat/all_different.cc @@ -36,8 +36,9 @@ namespace operations_research { namespace sat { std::function AllDifferentBinary( - const std::vector& vars) { - return [=](Model* model) { + absl::Span vars) { + return [=, vars = std::vector(vars.begin(), vars.end())]( + Model* model) { // Fully encode all the given variables and construct a mapping value -> // List of literal each indicating that a given variable takes this value. // @@ -97,8 +98,9 @@ std::function AllDifferentOnBounds( } std::function AllDifferentAC( - const std::vector& variables) { - return [=](Model* model) { + absl::Span variables) { + return [=, variables = std::vector( + variables.begin(), variables.end())](Model* model) { if (variables.size() < 3) return; AllDifferentConstraint* constraint = new AllDifferentConstraint( diff --git a/ortools/sat/all_different.h b/ortools/sat/all_different.h index 3384353f53..094eea1667 100644 --- a/ortools/sat/all_different.h +++ b/ortools/sat/all_different.h @@ -36,7 +36,7 @@ namespace sat { // encodes all the variables and simply enforces a <= 1 constraint on each // possible values. std::function AllDifferentBinary( - const std::vector& vars); + absl::Span vars); // Enforces that the given tuple of variables takes different values. // Same as AllDifferentBinary() but use a different propagator that only enforce @@ -62,7 +62,7 @@ std::function AllDifferentOnBounds( // // This will fully encode variables. std::function AllDifferentAC( - const std::vector& variables); + absl::Span variables); // Implementation of AllDifferentAC(). class AllDifferentConstraint : PropagatorInterface { diff --git a/ortools/sat/circuit.cc b/ortools/sat/circuit.cc index 74619e2048..b28ab8e41b 100644 --- a/ortools/sat/circuit.cc +++ b/ortools/sat/circuit.cc @@ -21,6 +21,7 @@ #include "absl/container/flat_hash_set.h" #include "absl/log/check.h" #include "absl/meta/type_traits.h" +#include "absl/types/span.h" #include "ortools/base/logging.h" #include "ortools/graph/strongly_connected_components.h" #include "ortools/sat/integer.h" @@ -33,9 +34,9 @@ namespace operations_research { namespace sat { CircuitPropagator::CircuitPropagator(const int num_nodes, - const std::vector& tails, - const std::vector& heads, - const std::vector& literals, + absl::Span tails, + absl::Span heads, + absl::Span literals, Options options, Model* model) : num_nodes_(num_nodes), options_(options), @@ -483,7 +484,7 @@ bool NoCyclePropagator::Propagate() { CircuitCoveringPropagator::CircuitCoveringPropagator( std::vector> graph, - const std::vector& distinguished_nodes, Model* model) + absl::Span distinguished_nodes, Model* model) : graph_(std::move(graph)), num_nodes_(graph_.size()), trail_(model->GetOrCreate()) { @@ -626,8 +627,9 @@ bool CircuitCoveringPropagator::Propagate() { } std::function ExactlyOnePerRowAndPerColumn( - const std::vector>& graph) { - return [=](Model* model) { + absl::Span> graph) { + return [=, graph = std::vector>( + graph.begin(), graph.end())](Model* model) { const int n = graph.size(); std::vector exactly_one_constraint; exactly_one_constraint.reserve(n); @@ -695,9 +697,10 @@ void LoadSubcircuitConstraint(int num_nodes, const std::vector& tails, } std::function CircuitCovering( - const std::vector>& graph, + absl::Span> graph, const std::vector& distinguished_nodes) { - return [=](Model* model) { + return [=, graph = std::vector>( + graph.begin(), graph.end())](Model* model) { CircuitCoveringPropagator* constraint = new CircuitCoveringPropagator(graph, distinguished_nodes, model); constraint->RegisterWith(model->GetOrCreate()); diff --git a/ortools/sat/circuit.h b/ortools/sat/circuit.h index b5f3c75cb2..1935007f19 100644 --- a/ortools/sat/circuit.h +++ b/ortools/sat/circuit.h @@ -21,6 +21,7 @@ #include "absl/container/btree_set.h" #include "absl/container/flat_hash_map.h" +#include "absl/types/span.h" #include "ortools/base/logging.h" #include "ortools/base/types.h" #include "ortools/graph/strongly_connected_components.h" @@ -53,9 +54,9 @@ class CircuitPropagator : PropagatorInterface, ReversibleInterface { // The constraints take a sparse representation of a graph on [0, n). Each arc // being present when the given literal is true. - CircuitPropagator(int num_nodes, const std::vector& tails, - const std::vector& heads, - const std::vector& literals, Options options, + CircuitPropagator(int num_nodes, absl::Span tails, + absl::Span heads, + absl::Span literals, Options options, Model* model); // This type is neither copyable nor movable. @@ -173,7 +174,7 @@ class NoCyclePropagator : PropagatorInterface, ReversibleInterface { class CircuitCoveringPropagator : PropagatorInterface, ReversibleInterface { public: CircuitCoveringPropagator(std::vector> graph, - const std::vector& distinguished_nodes, + absl::Span distinguished_nodes, Model* model); void SetLevel(int level) final; @@ -254,9 +255,9 @@ void LoadSubcircuitConstraint(int num_nodes, const std::vector& tails, // TODO(user): Change to a sparse API like for the function above. std::function ExactlyOnePerRowAndPerColumn( - const std::vector>& graph); + absl::Span> graph); std::function CircuitCovering( - const std::vector>& graph, + absl::Span> graph, const std::vector& distinguished_nodes); } // namespace sat diff --git a/ortools/sat/cp_constraints.h b/ortools/sat/cp_constraints.h index 3090489d1c..7e07c4d83f 100644 --- a/ortools/sat/cp_constraints.h +++ b/ortools/sat/cp_constraints.h @@ -161,10 +161,13 @@ inline std::function GreaterThanAtLeastOneOf( // Note(user): If there is just one or two candidates, this doesn't add // anything. inline std::function PartialIsOneOfVar( - IntegerVariable target_var, const std::vector& vars, - const std::vector& selectors) { + IntegerVariable target_var, absl::Span vars, + absl::Span selectors) { CHECK_EQ(vars.size(), selectors.size()); - return [=](Model* model) { + return [=, + selectors = std::vector(selectors.begin(), selectors.end()), + vars = std::vector(vars.begin(), vars.end())]( + Model* model) { const std::vector offsets(vars.size(), IntegerValue(0)); if (vars.size() > 2) { // Propagate the min. diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index daf282f6c2..b99dad9b4b 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -1351,8 +1351,8 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { // We list for each tuple the possible values the variable can take. // If the list is empty, then this encode "any value". void ProcessOneCompressedColumn( - int variable, const std::vector& tuple_literals, - const std::vector>& values, + int variable, absl::Span tuple_literals, + absl::Span> values, std::optional table_is_active_literal, PresolveContext* context) { DCHECK_EQ(tuple_literals.size(), values.size()); @@ -1656,7 +1656,7 @@ bool ReduceTableInPresenceOfUniqueVariableWithCosts( // is called. Some checks will fail otherwise. void CompressAndExpandPositiveTable(ConstraintProto* ct, bool last_column_is_cost, - const std::vector& vars, + absl::Span vars, std::vector>* tuples, PresolveContext* context) { const int num_tuples_before_compression = tuples->size(); diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc index b6b13994c3..8169661da0 100644 --- a/ortools/sat/cp_model_lns.cc +++ b/ortools/sat/cp_model_lns.cc @@ -825,7 +825,7 @@ struct IndexedRectangle { }; void InsertRectanglePredecences( - const std::vector& rectangles, + absl::Span rectangles, absl::flat_hash_set>* precedences) { // TODO(user): Refine set of interesting points. std::vector interesting_points; @@ -1148,7 +1148,7 @@ void NeighborhoodGeneratorHelper::AddSolutionHinting( Neighborhood NeighborhoodGeneratorHelper::RelaxGivenVariables( const CpSolverResponse& initial_solution, - const std::vector& relaxed_variables) const { + absl::Span relaxed_variables) const { std::vector relaxed_variables_set(model_proto_.variables_size(), false); for (const int var : relaxed_variables) relaxed_variables_set[var] = true; absl::flat_hash_set fixed_variables; @@ -1737,8 +1737,8 @@ namespace { // Create a constraint sum (X - LB) + sum (UB - X) <= rhs. ConstraintProto DistanceToBoundsSmallerThanConstraint( - const std::vector>& dist_to_lower_bound, - const std::vector>& dist_to_upper_bound, + absl::Span> dist_to_lower_bound, + absl::Span> dist_to_upper_bound, const int64_t rhs) { DCHECK_GE(rhs, 0); ConstraintProto new_constraint; @@ -2290,6 +2290,84 @@ Neighborhood RandomRectanglesPackingNeighborhoodGenerator::Generate( return helper_.FixGivenVariables(initial_solution, variables_to_freeze); } +Neighborhood RectanglesPackingRelaxOneNeighborhoodGenerator::Generate( + const CpSolverResponse& initial_solution, SolveData& data, + absl::BitGenRef random) { + // First pick one rectangle. + const std::vector all_active_rectangles = + helper_.GetActiveRectangles(initial_solution); + if (all_active_rectangles.size() <= 1) return helper_.FullNeighborhood(); + + const ActiveRectangle& base_rectangle = + all_active_rectangles[absl::Uniform(random, 0, + all_active_rectangles.size())]; + + const auto get_rectangle = [&initial_solution, helper = &helper_]( + const ActiveRectangle& rectangle) { + const int x_interval_idx = rectangle.x_interval; + const int y_interval_idx = rectangle.y_interval; + const ConstraintProto& x_interval_ct = + helper->ModelProto().constraints(x_interval_idx); + const ConstraintProto& y_interval_ct = + helper->ModelProto().constraints(y_interval_idx); + return Rectangle{.x_min = GetLinearExpressionValue( + x_interval_ct.interval().start(), initial_solution), + .x_max = GetLinearExpressionValue( + x_interval_ct.interval().end(), initial_solution), + .y_min = GetLinearExpressionValue( + y_interval_ct.interval().start(), initial_solution), + .y_max = GetLinearExpressionValue( + y_interval_ct.interval().end(), initial_solution)}; + }; + + const Rectangle center_rect = get_rectangle(base_rectangle); + + // Now compute a neighborhood around that rectangle. In this neighborhood + // we prefer a "Square" region around the initial rectangle center rather than + // a circle. + // + // Note that we only consider two rectangles as potential neighbors if they + // are part of the same no_overlap_2d constraint. + absl::flat_hash_set variables_to_freeze; + std::vector> distances; + distances.reserve(all_active_rectangles.size()); + for (int i = 0; i < all_active_rectangles.size(); ++i) { + const ActiveRectangle& rectangle = all_active_rectangles[i]; + InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.x_interval, + variables_to_freeze); + InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.y_interval, + variables_to_freeze); + + const Rectangle rect = get_rectangle(rectangle); + const bool same_no_overlap_as_center_rect = absl::c_any_of( + base_rectangle.no_overlap_2d_constraints, [&rectangle](const int c) { + return rectangle.no_overlap_2d_constraints.contains(c); + }); + if (same_no_overlap_as_center_rect) { + distances.push_back( + {i, CenterToCenterLInfinityDistance(center_rect, rect)}); + } + } + std::sort(distances.begin(), distances.end(), + [](const auto& a, const auto& b) { return a.second < b.second; }); + + const int num_to_sample = data.difficulty * all_active_rectangles.size(); + absl::flat_hash_set variables_to_relax; + const int num_to_relax = std::min(distances.size(), num_to_sample); + for (int i = 0; i < num_to_relax; ++i) { + const int rectangle_idx = distances[i].first; + const ActiveRectangle& rectangle = all_active_rectangles[rectangle_idx]; + InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.x_interval, + variables_to_relax); + InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.y_interval, + variables_to_relax); + } + for (const int v : variables_to_relax) { + variables_to_freeze.erase(v); + } + return helper_.FixGivenVariables(initial_solution, variables_to_freeze); +} + Neighborhood RectanglesPackingRelaxTwoNeighborhoodsGenerator::Generate( const CpSolverResponse& initial_solution, SolveData& data, absl::BitGenRef random) { @@ -2327,22 +2405,16 @@ Neighborhood RectanglesPackingRelaxTwoNeighborhoodsGenerator::Generate( y_interval_ct.interval().end(), initial_solution)}; }; - // TODO(user): This computes the distance between the center of the - // rectangles. We could use the real distance between the closest points, but - // not sure it is worth the extra complexity. - const auto compute_rectangle_distance = [](const Rectangle& rect1, - const Rectangle& rect2) { - return (static_cast(rect1.x_min.value()) + rect1.x_max.value() - - rect2.x_min.value() - rect2.x_max.value()) * - (static_cast(rect1.y_min.value()) + rect1.y_max.value() - - rect2.y_min.value() - rect2.y_max.value()); - }; const Rectangle rect1 = get_rectangle(chosen_rectangle_1); const Rectangle rect2 = get_rectangle(chosen_rectangle_2); // Now compute a neighborhood around each rectangle. Note that we only // consider two rectangles as potential neighbors if they are part of the same // no_overlap_2d constraint. + // + // TODO(user): This computes the distance between the center of the + // rectangles. We could use the real distance between the closest points, but + // not sure it is worth the extra complexity. absl::flat_hash_set variables_to_freeze; std::vector> distances1; std::vector> distances2; @@ -2367,10 +2439,10 @@ Neighborhood RectanglesPackingRelaxTwoNeighborhoodsGenerator::Generate( return rectangle.no_overlap_2d_constraints.contains(c); }); if (same_no_overlap_as_rect1) { - distances1.push_back({i, compute_rectangle_distance(rect1, rect)}); + distances1.push_back({i, CenterToCenterL2Distance(rect1, rect)}); } if (same_no_overlap_as_rect2) { - distances2.push_back({i, compute_rectangle_distance(rect2, rect)}); + distances2.push_back({i, CenterToCenterL2Distance(rect2, rect)}); } } const int num_to_sample_each = diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h index 7c2a096c4f..8dd0645000 100644 --- a/ortools/sat/cp_model_lns.h +++ b/ortools/sat/cp_model_lns.h @@ -116,7 +116,7 @@ class NeighborhoodGeneratorHelper : public SubSolver { // variables in relaxed_variables. Neighborhood RelaxGivenVariables( const CpSolverResponse& initial_solution, - const std::vector& relaxed_variables) const; + absl::Span relaxed_variables) const; // Returns a trivial model by fixing all active variables to the initial // solution values. @@ -361,7 +361,11 @@ class NeighborhoodGenerator { public: NeighborhoodGenerator(absl::string_view name, NeighborhoodGeneratorHelper const* helper) - : name_(name), helper_(*helper), difficulty_(0.5) {} + : name_(name), + helper_(*helper), + deterministic_limit_( + helper->Parameters().lns_initial_deterministic_limit()), + difficulty_(helper->Parameters().lns_initial_difficulty()) {} virtual ~NeighborhoodGenerator() = default; using ActiveRectangle = NeighborhoodGeneratorHelper::ActiveRectangle; @@ -721,6 +725,19 @@ class RandomRectanglesPackingNeighborhoodGenerator SolveData& data, absl::BitGenRef random) final; }; +// Only make sense for problems with no_overlap_2d constraints. This selects one +// random rectangles and relax the closest rectangles to it. +class RectanglesPackingRelaxOneNeighborhoodGenerator + : public NeighborhoodGenerator { + public: + explicit RectanglesPackingRelaxOneNeighborhoodGenerator( + NeighborhoodGeneratorHelper const* helper, absl::string_view name) + : NeighborhoodGenerator(name, helper) {} + + Neighborhood Generate(const CpSolverResponse& initial_solution, + SolveData& data, absl::BitGenRef random) final; +}; + // Only make sense for problems with no_overlap_2d constraints. This selects two // random rectangles and relax them alongside the closest rectangles to each one // of them. The idea is that this will find a better solution when there is a diff --git a/ortools/sat/cp_model_postsolve.cc b/ortools/sat/cp_model_postsolve.cc index 5f329a9625..4a522f554d 100644 --- a/ortools/sat/cp_model_postsolve.cc +++ b/ortools/sat/cp_model_postsolve.cc @@ -19,6 +19,7 @@ #include #include "absl/log/check.h" +#include "absl/types/span.h" #include "ortools/base/logging.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/cp_model.pb.h" @@ -226,7 +227,7 @@ int64_t EvaluateLinearExpression(const LinearExpressionProto& expr, } bool LinearExpressionIsFixed(const LinearExpressionProto& expr, - const std::vector& domains) { + absl::Span domains) { for (const int var : expr.vars()) { if (!domains[var].IsFixed()) return false; } @@ -335,7 +336,7 @@ void PostsolveIntProd(const ConstraintProto& ct, std::vector* domains) { void PostsolveResponse(const int64_t num_variables_in_original_model, const CpModelProto& mapping_proto, - const std::vector& postsolve_mapping, + absl::Span postsolve_mapping, std::vector* solution) { CHECK_EQ(solution->size(), postsolve_mapping.size()); diff --git a/ortools/sat/cp_model_postsolve.h b/ortools/sat/cp_model_postsolve.h index efa24521de..e49661340c 100644 --- a/ortools/sat/cp_model_postsolve.h +++ b/ortools/sat/cp_model_postsolve.h @@ -17,6 +17,7 @@ #include #include +#include "absl/types/span.h" #include "ortools/base/types.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/util/logging.h" @@ -45,7 +46,7 @@ namespace sat { // chosen values? The feature might never be needed though. void PostsolveResponse(int64_t num_variables_in_original_model, const CpModelProto& mapping_proto, - const std::vector& postsolve_mapping, + absl::Span postsolve_mapping, std::vector* solution); // Try to postsolve with a "best-effort" the reduced domain from the presolved diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 4f78ad9e4d..c093f9cae4 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -7031,6 +7031,7 @@ void CpModelPresolver::RunPropagatorsForConstraint(const ConstraintProto& ct) { local_params.set_use_conservative_scale_overload_checker(true); local_params.set_use_dual_scheduling_heuristics(true); + model.GetOrCreate()->MergeWithGlobalTimeLimit(time_limit_); std::vector variable_mapping; CreateValidModelWithSingleConstraint(ct, context_, &variable_mapping, &tmp_model_); @@ -7813,6 +7814,73 @@ void CpModelPresolver::ShiftObjectiveWithExactlyOnes() { } } +bool CpModelPresolver::PropagateObjective() { + if (!context_->working_model->has_objective()) return true; + if (context_->ModelIsUnsat()) return false; + context_->WriteObjectiveToProto(); + + int64_t min_activity = 0; + int64_t max_variation = 0; + const CpObjectiveProto& objective = context_->working_model->objective(); + const int num_terms = objective.vars().size(); + for (int i = 0; i < num_terms; ++i) { + const int var = objective.vars(i); + const int64_t coeff = objective.coeffs(i); + CHECK(RefIsPositive(var)); + CHECK_NE(coeff, 0); + + const int64_t domain_min = context_->MinOf(var); + const int64_t domain_max = context_->MaxOf(var); + if (coeff > 0) { + min_activity += coeff * domain_min; + } else { + min_activity += coeff * domain_max; + } + const int64_t variation = std::abs(coeff) * (domain_max - domain_min); + max_variation = std::max(max_variation, variation); + } + + // Infeasible ? + const int64_t slack = + CapSub(ReadDomainFromProto(objective).Max(), min_activity); + if (slack < 0) { + return context_->NotifyThatModelIsUnsat( + "infeasible while propagating objective"); + } + + // No propagation ? + if (max_variation <= slack) return true; + + int num_propagations = 0; + for (int i = 0; i < num_terms; ++i) { + const int var = objective.vars(i); + const int64_t coeff = objective.coeffs(i); + const int64_t domain_min = context_->MinOf(var); + const int64_t domain_max = context_->MaxOf(var); + + const int64_t new_diff = slack / std::abs(coeff); + if (new_diff >= domain_max - domain_min) continue; + + ++num_propagations; + if (coeff > 0) { + if (!context_->IntersectDomainWith( + var, Domain(domain_min, domain_min + new_diff))) { + return false; + } + } else { + if (!context_->IntersectDomainWith( + var, Domain(domain_max - new_diff, domain_max))) { + return false; + } + } + } + CHECK_GT(num_propagations, 0); + + context_->UpdateRuleStats("objective: restricted var domains by propagation", + num_propagations); + return true; +} + // Expand the objective expression in some easy cases. // // The ideas is to look at all the "tight" equality constraints. These should @@ -12895,25 +12963,43 @@ bool ModelCopy::CopyAllDiff(const ConstraintProto& ct) { } bool ModelCopy::CopyLinMax(const ConstraintProto& ct) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); + // We will create it lazily if we end up copying something. + ConstraintProto* new_ct = nullptr; + + // Regroup all constant terms and copy the other. + int64_t max_of_fixed_terms = std::numeric_limits::min(); for (const auto& expr : ct.lin_max().exprs()) { - CopyLinearExpression(expr, new_ct->mutable_lin_max()->add_exprs()); - auto& last_expr = *new_ct->mutable_lin_max()->mutable_exprs( - new_ct->lin_max().exprs_size() - 1); - if (last_expr.vars().empty() && new_ct->lin_max().exprs().size() > 1) { - LinearExpressionProto* first_expr = - new_ct->mutable_lin_max()->mutable_exprs(0); - if (first_expr->vars().empty()) { - // We have two constants, keep the largest. - first_expr->set_offset( - std::max(first_expr->offset(), last_expr.offset())); - new_ct->mutable_lin_max()->mutable_exprs()->RemoveLast(); - } else { - // Put the constant in the first position. - last_expr.Swap(first_expr); + if (context_->IsFixed(expr)) { + max_of_fixed_terms = + std::max(max_of_fixed_terms, context_->FixedValue(expr)); + } else { + // copy. + if (new_ct == nullptr) { + new_ct = context_->working_model->add_constraints(); } + CopyLinearExpression(expr, new_ct->mutable_lin_max()->add_exprs()); } } + + // If we have no non-fixed expression, we can just fix the target when it + // involve at most one variable. + if (new_ct == nullptr && ct.enforcement_literal().empty() && + ct.lin_max().target().vars().size() <= 1) { + context_->UpdateRuleStats("lin_max: all exprs fixed during copy"); + return context_->IntersectDomainWith(ct.lin_max().target(), + Domain(max_of_fixed_terms)); + } + + // Otherwise, add a constant term if needed. + if (max_of_fixed_terms > std::numeric_limits::min()) { + if (new_ct == nullptr) { + new_ct = context_->working_model->add_constraints(); + } + new_ct->mutable_lin_max()->add_exprs()->set_offset(max_of_fixed_terms); + } + + // Finish by copying the target. + if (new_ct == nullptr) return false; // No expr == unsat. CopyLinearExpression(ct.lin_max().target(), new_ct->mutable_lin_max()->mutable_target()); return true; @@ -13576,6 +13662,9 @@ CpSolverStatus CpModelPresolver::Presolve() { context_->UpdateRuleStats("presolve: iteration"); const int64_t old_num_presolve_op = context_->num_presolve_operations; + // Propagate the objective. + if (!PropagateObjective()) return InfeasibleStatus(); + // TODO(user): The presolve transformations we do after this is called might // result in even more presolve if we were to call this again! improve the // code. See for instance plusexample_6_sat.fzn were represolving the diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index a337a66e77..ec75d6f7cf 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -254,6 +254,10 @@ class CpModelPresolver { // Converts bool_or and at_most_one of size 2 to bool_and. void ConvertToBoolAnd(); + // Sometimes an upper bound on the objective can reduce the domains of many + // variables. This "propagates" the objective like a normal linear constraint. + bool PropagateObjective(); + // Try to reformulate the objective in term of "base" variables. This is // mainly useful for core based approach where having more terms in the // objective (but with a same trivial lower bound) should help. diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 7f4a634d8d..c341b6fa77 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -759,6 +759,53 @@ bool VarIsFixed(const CpModelProto& model_proto, int i) { model_proto.variables(i).domain(1); } +// Note that we restrict the objective to be <= so that the hint is still +// feasible. Alternatively, we could look for < hint value if we only want +// better solution. +void RestrictObjectiveUsingHint(CpModelProto* model_proto) { + if (!model_proto->has_objective()) return; + if (!model_proto->has_solution_hint()) return; + + // We will abort if the hint is not complete, ignoring fixed variables. + const int num_vars = model_proto->variables().size(); + int num_filled = 0; + std::vector filled(num_vars, false); + std::vector solution(num_vars, 0); + for (int var = 0; var < num_vars; ++var) { + if (VarIsFixed(*model_proto, var)) { + solution[var] = model_proto->variables(var).domain(0); + filled[var] = true; + ++num_filled; + } + } + const auto& hint_proto = model_proto->solution_hint(); + const int num_hinted = hint_proto.vars().size(); + for (int i = 0; i < num_hinted; ++i) { + const int var = hint_proto.vars(i); + CHECK(RefIsPositive(var)); + if (filled[var]) continue; + + const int64_t value = hint_proto.values(i); + solution[var] = value; + filled[var] = true; + ++num_filled; + } + if (num_filled != num_vars) return; + + const int64_t obj_upper_bound = + ComputeInnerObjective(model_proto->objective(), solution); + const Domain restriction = + Domain(std::numeric_limits::min(), obj_upper_bound); + + if (model_proto->objective().domain().empty()) { + FillDomainInProto(restriction, model_proto->mutable_objective()); + } else { + FillDomainInProto(ReadDomainFromProto(model_proto->objective()) + .IntersectionWith(restriction), + model_proto->mutable_objective()); + } +} + // Returns false if there is a complete solution hint that is infeasible, or // true otherwise. bool TestSolutionHintForFeasibility(const CpModelProto& model_proto, @@ -1347,6 +1394,12 @@ class LnsSolver : public SubSolver { TestSolutionHintForFeasibility(lns_fragment, /*logger=*/nullptr); } + // If we use a hint, we will restrict the objective to be <= to the one + // of the hint. This is helpful on some model where doing so can cause + // the presolve to restrict the domain of many variables. Note that the + // hint will still be feasible as we use <= and not <. + RestrictObjectiveUsingHint(&lns_fragment); + CpModelProto debug_copy; if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) { // We need to make a copy because the presolve is destructive. @@ -1777,12 +1830,18 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) { const bool has_no_overlap2d = !helper->TypeToConstraints(ConstraintProto::kNoOverlap2D).empty(); if (has_no_overlap2d) { - if (name_filter.Keep("packing_rectangles_lns")) { + if (name_filter.Keep("packing_random_lns")) { reentrant_interleaved_subsolvers.push_back(std::make_unique( std::make_unique( helper, name_filter.LastName()), lns_params, helper, shared)); } + if (name_filter.Keep("packing_square_lns")) { + reentrant_interleaved_subsolvers.push_back(std::make_unique( + std::make_unique( + helper, name_filter.LastName()), + lns_params, helper, shared)); + } if (name_filter.Keep("packing_swap_lns")) { reentrant_interleaved_subsolvers.push_back(std::make_unique( std::make_unique( @@ -2012,8 +2071,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) { // If the option use_sat_inprocessing is true, then before post-solving a // solution, we need to make sure we add any new clause required for postsolving // to the mapping_model. -void AddPostsolveClauses(const std::vector& postsolve_mapping, - Model* model, CpModelProto* mapping_proto) { +void AddPostsolveClauses(absl::Span postsolve_mapping, Model* model, + CpModelProto* mapping_proto) { auto* mapping = model->GetOrCreate(); auto* postsolve = model->GetOrCreate(); for (const auto& clause : postsolve->clauses) { diff --git a/ortools/sat/diffn_util.h b/ortools/sat/diffn_util.h index d474254c65..0c8044740f 100644 --- a/ortools/sat/diffn_util.h +++ b/ortools/sat/diffn_util.h @@ -120,6 +120,28 @@ inline IntegerValue Rectangle::IntersectArea(const Rectangle& other) const { } } +// Returns the L2 distance between the centers of the two rectangles. +inline double CenterToCenterL2Distance(const Rectangle& a, const Rectangle& b) { + const double diff_x = + (static_cast(a.x_min.value()) + a.x_max.value()) / 2.0 - + (static_cast(b.x_min.value()) + b.x_max.value()) / 2.0; + const double diff_y = + (static_cast(a.y_min.value()) + a.y_max.value()) / 2.0 - + (static_cast(b.y_min.value()) + b.y_max.value()) / 2.0; + return std::sqrt(diff_x * diff_x + diff_y * diff_y); +} + +inline double CenterToCenterLInfinityDistance(const Rectangle& a, + const Rectangle& b) { + const double diff_x = + (static_cast(a.x_min.value()) + a.x_max.value()) / 2.0 - + (static_cast(b.x_min.value()) + b.x_max.value()) / 2.0; + const double diff_y = + (static_cast(a.y_min.value()) + a.y_max.value()) / 2.0 - + (static_cast(b.y_min.value()) + b.y_max.value()) / 2.0; + return std::max(std::abs(diff_x), std::abs(diff_y)); +} + // Creates a graph when two nodes are connected iff their rectangles overlap. // Then partition into connected components. // diff --git a/ortools/sat/diffn_util_test.cc b/ortools/sat/diffn_util_test.cc index 66cb9935d2..2d76136199 100644 --- a/ortools/sat/diffn_util_test.cc +++ b/ortools/sat/diffn_util_test.cc @@ -50,6 +50,24 @@ using ::testing::ElementsAreArray; using ::testing::UnorderedElementsAre; using ::testing::UnorderedElementsAreArray; +TEST(CenterToCenterDistanceTest, BasicTest) { + Rectangle a, b; + a.x_min = 0; + a.x_max = 2; + a.y_min = 0; + a.y_max = 2; + b.x_min = 0; + b.x_max = 10; + b.y_min = 0; + b.y_max = 10; + + // This is just the distance between (1,1) and (5,5) which should be sqrt(32). + EXPECT_EQ(CenterToCenterL2Distance(a, b), std::sqrt(32)); + + // Now this is 4. + EXPECT_EQ(CenterToCenterLInfinityDistance(a, b), 4.0); +} + TEST(GetOverlappingRectangleComponentsTest, NoComponents) { EXPECT_TRUE(GetOverlappingRectangleComponents({}, {}).empty()); IntegerValue zero(0); diff --git a/ortools/sat/fuzz_testdata/MultipleCumulativesA b/ortools/sat/fuzz_testdata/MultipleCumulativesA index 7a85ca237f..72f6445312 100644 --- a/ortools/sat/fuzz_testdata/MultipleCumulativesA +++ b/ortools/sat/fuzz_testdata/MultipleCumulativesA @@ -1,608 +1,326 @@ # proto-file: ortools/sat/cp_model.proto # proto-message: operations_research.sat.CpModelProto -variables { - domain: 0 - domain: 1024 -} -variables { - domain: 0 - domain: 3 -} -variables { - domain: 0 - domain: 3 -} -variables { - domain: 1 - domain: 4 -} -variables { - domain: 0 - domain: 3 -} -variables { - domain: 0 - domain: 3 -} -variables { - domain: 1 - domain: 4 -} -variables { - domain: 0 - domain: 3 -} -variables { - domain: 0 - domain: 3 -} -variables { - domain: 1 - domain: 4 -} -variables { - domain: 0 - domain: 4 -} -variables { - domain: 0 - domain: 4 -} -variables { - domain: 0 - domain: 4 -} -variables { - domain: 0 - domain: 4 -} -variables { - domain: 0 - domain: 4 -} -variables { - domain: 0 - domain: 4 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 2048 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} +variables { domain: [0, 1024] } +variables { domain: [0, 3] } +variables { domain: [0, 3] } +variables { domain: [1, 4] } +variables { domain: [0, 3] } +variables { domain: [0, 3] } +variables { domain: [1, 4] } +variables { domain: [0, 3] } +variables { domain: [0, 3] } +variables { domain: [1, 4] } +variables { domain: [0, 4] } +variables { domain: [0, 4] } +variables { domain: [0, 4] } +variables { domain: [0, 4] } +variables { domain: [0, 4] } +variables { domain: [0, 4] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 512] } +variables { domain: [0, 512] } +variables { domain: [0, 2048] } +variables { domain: [0, 512] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } constraints { linear { - vars: 2 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [2, 1] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 3 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [3, 1] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 5 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [5, 4] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 6 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [6, 4] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 8 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [8, 7] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 9 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [9, 7] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 3 - vars: 1 - vars: 10 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [3, 1, 10] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 1 - coeffs: 1 - offset: 1 - } - end { - vars: 3 - coeffs: 1 - } - size { - vars: 10 - coeffs: 1 - } + start { vars: [1] coeffs: [1] offset: 1 } + end { vars: [3] coeffs: [1] } + size { vars: [10] coeffs: [1] } } } constraints { linear { - vars: 1 - vars: 2 - vars: 11 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [1, 2, 11] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 2 - coeffs: 1 - } - end { - vars: 1 - coeffs: 1 - } - size { - vars: 11 - coeffs: 1 - } + start { vars: [2] coeffs: [1] } + end { vars: [1] coeffs: [1] } + size { vars: [11] coeffs: [1] } } } constraints { linear { - vars: 6 - vars: 4 - vars: 12 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [6, 4, 12] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 4 - coeffs: 1 - offset: 1 - } - end { - vars: 6 - coeffs: 1 - } - size { - vars: 12 - coeffs: 1 - } + start { vars: [4] coeffs: [1] offset: 1 } + end { vars: [6] coeffs: [1] } + size { vars: [12] coeffs: [1] } } } constraints { linear { - vars: 4 - vars: 5 - vars: 13 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [4, 5, 13] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 5 - coeffs: 1 - } - end { - vars: 4 - coeffs: 1 - } - size { - vars: 13 - coeffs: 1 - } + start { vars: [5] coeffs: [1] } + end { vars: [4] coeffs: [1] } + size { vars: [13] coeffs: [1] } } } constraints { linear { - vars: 9 - vars: 7 - vars: 14 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [9, 7, 14] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 7 - coeffs: 1 - offset: 1 - } - end { - vars: 9 - coeffs: 1 - } - size { - vars: 14 - coeffs: 1 - } + start { vars: [7] coeffs: [1] offset: 1 } + end { vars: [9] coeffs: [1] } + size { vars: [14] coeffs: [1] } } } constraints { linear { - vars: 7 - vars: 8 - vars: 15 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [7, 8, 15] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 8 - coeffs: 1 - } - end { - vars: 7 - coeffs: 1 - } - size { - vars: 15 - coeffs: 1 - } + start { vars: [8] coeffs: [1] } + end { vars: [7] coeffs: [1] } + size { vars: [15] coeffs: [1] } } } constraints { linear { - vars: 5 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [5, 1] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 6 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [6, 1] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { - enforcement_literal: -17 + enforcement_literal: [-17] linear { - vars: 4 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 0 - domain: 0 + vars: [4, 1] + coeffs: [1, -1] + domain: [0, 0] } } constraints { - enforcement_literal: 16 + enforcement_literal: [16] interval { - start { - vars: 1 - coeffs: 1 - } - end { - vars: 1 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [1] coeffs: [1] } + end { vars: [1] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { interval { - start { - vars: 4 - coeffs: 1 - } - end { - vars: 4 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [4] coeffs: [1] } + end { vars: [4] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 8 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [8, 4] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 9 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [9, 4] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { - enforcement_literal: -18 + enforcement_literal: [-18] linear { - vars: 7 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: 0 - domain: 0 + vars: [7, 4] + coeffs: [1, -1] + domain: [0, 0] } } constraints { - enforcement_literal: 17 + enforcement_literal: [17] interval { - start { - vars: 4 - coeffs: 1 - } - end { - vars: 4 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [4] coeffs: [1] } + end { vars: [4] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 7 - coeffs: 1 - domain: 0 - domain: 0 + vars: [7] + coeffs: [1] + domain: [0, 0] } } constraints { linear { - vars: 1 - coeffs: 1 - domain: 1 - domain: 1 + vars: [1] + coeffs: [1] + domain: [1, 1] } } constraints { linear { - vars: 18 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [18, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 18 - coeffs: 1 - } - intervals: 7 - intervals: 11 - intervals: 15 - demands { - offset: 1 - } - demands { - offset: 1 - } - demands { - offset: 2 - } + capacity { vars: [18] coeffs: [1] } + intervals: [7, 11, 15] + demands { offset: 1 } + demands { offset: 1 } + demands { offset: 2 } } } constraints { linear { - vars: 19 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [19, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 19 - coeffs: 1 - } - intervals: 9 - intervals: 13 - intervals: 17 - demands { - offset: 1 - } - demands { - offset: 1 - } - demands { - offset: 2 - } + capacity { vars: [19] coeffs: [1] } + intervals: [9, 13, 17] + demands { offset: 1 } + demands { offset: 1 } + demands { offset: 2 } } } constraints { linear { - vars: 20 - vars: 0 - coeffs: 1 - coeffs: -2 - domain: -9223372036854775808 - domain: 0 + vars: [20, 0] + coeffs: [1, -2] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 20 - coeffs: 1 - } - intervals: 21 - intervals: 26 - demands { - offset: 1 - } - demands { - offset: 2 - } + capacity { vars: [20] coeffs: [1] } + intervals: [21, 26] + demands { offset: 1 } + demands { offset: 2 } } } constraints { linear { - vars: 21 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [21, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 21 - coeffs: 1 - } - intervals: 22 - demands { - offset: 1 - } + capacity { vars: [21] coeffs: [1] } + intervals: [22] + demands { offset: 1 } } } constraints { - enforcement_literal: 22 + enforcement_literal: [22] linear { - vars: 2 - vars: 3 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [2, 3] + coeffs: [1, -1] + domain: [-1, -1] } } constraints { - enforcement_literal: 23 + enforcement_literal: [23] linear { - vars: 5 - vars: 6 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [5, 6] + coeffs: [1, -1] + domain: [-1, -1] } } constraints { - enforcement_literal: 24 + enforcement_literal: [24] linear { - vars: 8 - vars: 9 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [8, 9] + coeffs: [1, -1] + domain: [-1, -1] } } objective { - vars: 0 - coeffs: 1 + vars: [0] + coeffs: [1] } + diff --git a/ortools/sat/fuzz_testdata/MultipleCumulativesB b/ortools/sat/fuzz_testdata/MultipleCumulativesB index 48532c7c99..91ad2be669 100644 --- a/ortools/sat/fuzz_testdata/MultipleCumulativesB +++ b/ortools/sat/fuzz_testdata/MultipleCumulativesB @@ -1,901 +1,476 @@ # proto-file: ortools/sat/cp_model.proto # proto-message: operations_research.sat.CpModelProto -variables { - domain: 0 - domain: 1024 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 1 - domain: 2 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 1 - domain: 2 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 1 - domain: 2 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 1 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 2 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 2048 -} -variables { - domain: 0 - domain: 512 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} -variables { - domain: 0 - domain: 1 -} +variables { domain: [0, 1024] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [1, 2] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [1, 2] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [1, 2] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [1, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 2] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 512] } +variables { domain: [0, 512] } +variables { domain: [0, 512] } +variables { domain: [0, 2048] } +variables { domain: [0, 512] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } constraints { linear { - vars: 2 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [2, 1] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 3 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [3, 1] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 5 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [5, 4] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 6 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [6, 4] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 8 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [8, 7] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 9 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [9, 7] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 11 - vars: 10 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [11, 10] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 12 - vars: 10 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [12, 10] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { linear { - vars: 3 - vars: 1 - vars: 13 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [3, 1, 13] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 1 - coeffs: 1 - offset: 1 - } - end { - vars: 3 - coeffs: 1 - } - size { - vars: 13 - coeffs: 1 - } + start { vars: [1] coeffs: [1] offset: 1 } + end { vars: [3] coeffs: [1] } + size { vars: [13] coeffs: [1] } } } constraints { linear { - vars: 1 - vars: 2 - vars: 14 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [1, 2, 14] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 2 - coeffs: 1 - } - end { - vars: 1 - coeffs: 1 - } - size { - vars: 14 - coeffs: 1 - } + start { vars: [2] coeffs: [1] } + end { vars: [1] coeffs: [1] } + size { vars: [14] coeffs: [1] } } } constraints { linear { - vars: 6 - vars: 4 - vars: 15 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [6, 4, 15] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 4 - coeffs: 1 - offset: 1 - } - end { - vars: 6 - coeffs: 1 - } - size { - vars: 15 - coeffs: 1 - } + start { vars: [4] coeffs: [1] offset: 1 } + end { vars: [6] coeffs: [1] } + size { vars: [15] coeffs: [1] } } } constraints { linear { - vars: 4 - vars: 5 - vars: 16 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [4, 5, 16] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 5 - coeffs: 1 - } - end { - vars: 4 - coeffs: 1 - } - size { - vars: 16 - coeffs: 1 - } + start { vars: [5] coeffs: [1] } + end { vars: [4] coeffs: [1] } + size { vars: [16] coeffs: [1] } } } constraints { linear { - vars: 9 - vars: 7 - vars: 17 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [9, 7, 17] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 7 - coeffs: 1 - offset: 1 - } - end { - vars: 9 - coeffs: 1 - } - size { - vars: 17 - coeffs: 1 - } + start { vars: [7] coeffs: [1] offset: 1 } + end { vars: [9] coeffs: [1] } + size { vars: [17] coeffs: [1] } } } constraints { linear { - vars: 7 - vars: 8 - vars: 18 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [7, 8, 18] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 8 - coeffs: 1 - } - end { - vars: 7 - coeffs: 1 - } - size { - vars: 18 - coeffs: 1 - } + start { vars: [8] coeffs: [1] } + end { vars: [7] coeffs: [1] } + size { vars: [18] coeffs: [1] } } } constraints { linear { - vars: 12 - vars: 10 - vars: 19 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: -1 - domain: -1 + vars: [12, 10, 19] + coeffs: [-1, 1, 1] + domain: [-1, -1] } } constraints { interval { - start { - vars: 10 - coeffs: 1 - offset: 1 - } - end { - vars: 12 - coeffs: 1 - } - size { - vars: 19 - coeffs: 1 - } + start { vars: [10] coeffs: [1] offset: 1 } + end { vars: [12] coeffs: [1] } + size { vars: [19] coeffs: [1] } } } constraints { linear { - vars: 10 - vars: 11 - vars: 20 - coeffs: -1 - coeffs: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [10, 11, 20] + coeffs: [-1, 1, 1] + domain: [0, 0] } } constraints { interval { - start { - vars: 11 - coeffs: 1 - } - end { - vars: 10 - coeffs: 1 - } - size { - vars: 20 - coeffs: 1 - } + start { vars: [11] coeffs: [1] } + end { vars: [10] coeffs: [1] } + size { vars: [20] coeffs: [1] } } } constraints { interval { - start { - vars: 1 - coeffs: 1 - } - end { - vars: 1 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [1] coeffs: [1] } + end { vars: [1] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 5 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [5, 1] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 6 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [6, 1] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { - enforcement_literal: -22 + enforcement_literal: [-22] linear { - vars: 4 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 0 - domain: 0 + vars: [4, 1] + coeffs: [1, -1] + domain: [0, 0] } } constraints { - enforcement_literal: 21 + enforcement_literal: [21] interval { - start { - vars: 1 - coeffs: 1 - } - end { - vars: 1 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [1] coeffs: [1] } + end { vars: [1] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 8 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [8, 1] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 9 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [9, 1] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { - enforcement_literal: -23 + enforcement_literal: [-23] linear { - vars: 7 - vars: 1 - coeffs: 1 - coeffs: -1 - domain: 0 - domain: 0 + vars: [7, 1] + coeffs: [1, -1] + domain: [0, 0] } } constraints { - enforcement_literal: 22 + enforcement_literal: [22] interval { - start { - vars: 1 - coeffs: 1 - } - end { - vars: 1 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [1] coeffs: [1] } + end { vars: [1] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { interval { - start { - vars: 4 - coeffs: 1 - } - end { - vars: 4 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [4] coeffs: [1] } + end { vars: [4] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 11 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [11, 4] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 12 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [12, 4] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { - enforcement_literal: -24 + enforcement_literal: [-24] linear { - vars: 10 - vars: 4 - coeffs: 1 - coeffs: -1 - domain: 0 - domain: 0 + vars: [10, 4] + coeffs: [1, -1] + domain: [0, 0] } } constraints { - enforcement_literal: 23 + enforcement_literal: [23] interval { - start { - vars: 4 - coeffs: 1 - } - end { - vars: 4 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [4] coeffs: [1] } + end { vars: [4] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { interval { - start { - vars: 7 - coeffs: 1 - } - end { - vars: 7 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [7] coeffs: [1] } + end { vars: [7] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 11 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [11, 7] + coeffs: [1, -1] + domain: [-9223372036854775808, 0] } } constraints { linear { - vars: 12 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: 1 - domain: 9223372036854775807 + vars: [12, 7] + coeffs: [1, -1] + domain: [1, 9223372036854775807] } } constraints { - enforcement_literal: -25 + enforcement_literal: [-25] linear { - vars: 10 - vars: 7 - coeffs: 1 - coeffs: -1 - domain: 0 - domain: 0 + vars: [10, 7] + coeffs: [1, -1] + domain: [0, 0] } } constraints { - enforcement_literal: 24 + enforcement_literal: [24] interval { - start { - vars: 7 - coeffs: 1 - } - end { - vars: 7 - coeffs: 1 - offset: 1 - } - size { - offset: 1 - } + start { vars: [7] coeffs: [1] } + end { vars: [7] coeffs: [1] offset: 1 } + size { offset: 1 } } } constraints { linear { - vars: 10 - coeffs: 1 - domain: 0 - domain: 0 + vars: [10] + coeffs: [1] + domain: [0, 0] } } constraints { linear { - vars: 1 - coeffs: 1 - domain: 0 - domain: 0 + vars: [1] + coeffs: [1] + domain: [0, 0] } } constraints { linear { - vars: 25 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [25, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 25 - coeffs: 1 - } - intervals: 9 - intervals: 13 - intervals: 17 - intervals: 21 - demands { - offset: 2 - } - demands { - offset: 2 - } - demands { - offset: 2 - } - demands { - offset: 2 - } + capacity { vars: [25] coeffs: [1] } + intervals: [9, 13, 17, 21] + demands { offset: 2 } + demands { offset: 2 } + demands { offset: 2 } + demands { offset: 2 } } } constraints { linear { - vars: 26 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [26, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 26 - coeffs: 1 - } - intervals: 11 - intervals: 15 - intervals: 19 - intervals: 23 - demands { - offset: 2 - } - demands { - offset: 2 - } - demands { - offset: 2 - } - demands { - offset: 2 - } + capacity { vars: [26] coeffs: [1] } + intervals: [11, 15, 19, 23] + demands { offset: 2 } + demands { offset: 2 } + demands { offset: 2 } + demands { offset: 2 } } } constraints { linear { - vars: 27 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [27, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 27 - coeffs: 1 - } - intervals: 24 - demands { - offset: 1 - } + capacity { vars: [27] coeffs: [1] } + intervals: [24] + demands { offset: 1 } } } constraints { linear { - vars: 28 - vars: 0 - coeffs: 1 - coeffs: -2 - domain: -9223372036854775808 - domain: 0 + vars: [28, 0] + coeffs: [1, -2] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 28 - coeffs: 1 - } - intervals: 28 - intervals: 32 - intervals: 37 - intervals: 42 - demands { - offset: 2 - } - demands { - offset: 2 - } - demands { - offset: 2 - } - demands { - offset: 2 - } + capacity { vars: [28] coeffs: [1] } + intervals: [28, 32, 37, 42] + demands { offset: 2 } + demands { offset: 2 } + demands { offset: 2 } + demands { offset: 2 } } } constraints { linear { - vars: 29 - vars: 0 - coeffs: 2 - coeffs: -1 - domain: -9223372036854775808 - domain: 0 + vars: [29, 0] + coeffs: [2, -1] + domain: [-9223372036854775808, 0] } } constraints { cumulative { - capacity { - vars: 29 - coeffs: 1 - } - intervals: 33 - intervals: 38 - demands { - offset: 1 - } - demands { - offset: 1 - } + capacity { vars: [29] coeffs: [1] } + intervals: [33, 38] + demands { offset: 1 } + demands { offset: 1 } } } constraints { - enforcement_literal: 30 + enforcement_literal: [30] linear { - vars: 2 - vars: 3 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [2, 3] + coeffs: [1, -1] + domain: [-1, -1] } } constraints { - enforcement_literal: 31 + enforcement_literal: [31] linear { - vars: 5 - vars: 6 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [5, 6] + coeffs: [1, -1] + domain: [-1, -1] } } constraints { - enforcement_literal: 32 + enforcement_literal: [32] linear { - vars: 8 - vars: 9 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [8, 9] + coeffs: [1, -1] + domain: [-1, -1] } } constraints { - enforcement_literal: 33 + enforcement_literal: [33] linear { - vars: 11 - vars: 12 - coeffs: 1 - coeffs: -1 - domain: -1 - domain: -1 + vars: [11, 12] + coeffs: [1, -1] + domain: [-1, -1] } } objective { - vars: 0 - coeffs: 1 + vars: [0] + coeffs: [1] } diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index 58af89f8cb..fbd1a4f77f 100644 --- a/ortools/sat/parameters_validation.cc +++ b/ortools/sat/parameters_validation.cc @@ -93,6 +93,10 @@ std::string ValidateParameters(const SatParameters& params) { TEST_IS_FINITE(symmetry_detection_deterministic_time_limit); TEST_IS_FINITE(variable_activity_decay); + TEST_IS_FINITE(lns_initial_difficulty); + TEST_IS_FINITE(lns_initial_deterministic_limit); + TEST_IN_RANGE(lns_initial_difficulty, 0.0, 1.0); + TEST_POSITIVE(at_most_one_max_expansion_size); TEST_NOT_NAN(max_time_in_seconds); diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index e704989b1d..78d5a7cf3f 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -23,7 +23,7 @@ option java_multiple_files = true; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 307 +// NEXT TAG: 309 message SatParameters { // In some context, like in a portfolio of search, it makes sense to name a // given parameters set for logging purpose. @@ -1213,6 +1213,10 @@ message SatParameters { // LNS parameters. + // Initial parameters for neighborhood generation. + optional double lns_initial_difficulty = 307 [default = 0.5]; + optional double lns_initial_deterministic_limit = 308 [default = 0.1]; + // Testing parameters used to disable all lns workers. optional bool use_lns = 283 [default = true]; diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc index efdaa40e79..1e28d39dbc 100644 --- a/ortools/sat/var_domination.cc +++ b/ortools/sat/var_domination.cc @@ -39,7 +39,7 @@ #include "ortools/base/strong_vector.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" -#include "ortools/sat/integer.h" +#include "ortools/sat/integer_base.h" #include "ortools/sat/presolve_context.h" #include "ortools/sat/presolve_util.h" #include "ortools/sat/util.h" @@ -850,8 +850,10 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { context->deductions.ImpliedDomain(enf, positive_ref)); if (implied.IsEmpty()) { context->UpdateRuleStats("dual: fix variable"); + context->UpdateLiteralSolutionHint(enf, false); if (!context->SetLiteralToFalse(enf)) return false; - if (!context->IntersectDomainWith(positive_ref, Domain(bound))) { + if (!context->IntersectDomainWithAndUpdateHint(positive_ref, + Domain(bound))) { return false; } continue; @@ -860,7 +862,8 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { // Corner case. if (implied.FixedValue() == bound) { context->UpdateRuleStats("dual: fix variable"); - if (!context->IntersectDomainWith(positive_ref, implied)) { + if (!context->IntersectDomainWithAndUpdateHint(positive_ref, + implied)) { return false; } continue; @@ -925,6 +928,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { .IntersectionWith(var_domain); if (rhs.IsEmpty()) { context->UpdateRuleStats("linear1: infeasible"); + context->UpdateLiteralSolutionHint(ct.enforcement_literal(0), false); if (!context->SetLiteralToFalse(ct.enforcement_literal(0))) { return false; } @@ -1866,8 +1870,9 @@ bool ExploitDominanceRelations(const VarDomination& var_domination, // TODO(user): It look like testing this is not really necessary. // The reduction done by this class seem to be order independent. bool ok = true; - for (const IntegerVariable dom : - var_domination.DominatingVariables(var)) { + const absl::Span dominating_vars = + var_domination.DominatingVariables(var); + for (const IntegerVariable dom : dominating_vars) { // Note that we assumed that a fixed point was reached before this // is called, so modified_domains should have been empty as we // entered this function. If not, the code is still correct, but we @@ -1888,9 +1893,18 @@ bool ExploitDominanceRelations(const VarDomination& var_domination, increase_is_forbidden[var] = true; context->UpdateRuleStats( "domination: dual strenghtening using dominance"); - if (!context->IntersectDomainWithAndUpdateHint( - ref, Domain(context->MinOf(ref), lb))) { - return false; + const Domain reduced_domain = Domain(context->MinOf(ref), lb); + if (dominating_vars.empty()) { + if (!context->IntersectDomainWithAndUpdateHint(ref, + reduced_domain)) { + return false; + } + } else { + MaybeUpdateRefHintFromDominance(*context, ref, reduced_domain, + dominating_vars); + if (!context->IntersectDomainWith(ref, reduced_domain)) { + return false; + } } // The rest of the loop only care about Booleans. diff --git a/ortools/sat/var_domination_test.cc b/ortools/sat/var_domination_test.cc index 5ab9c1ee64..44590b87c1 100644 --- a/ortools/sat/var_domination_test.cc +++ b/ortools/sat/var_domination_test.cc @@ -17,7 +17,7 @@ #include "ortools/base/gmock.h" #include "ortools/base/parse_test_proto.h" #include "ortools/sat/cp_model.pb.h" -#include "ortools/sat/integer.h" +#include "ortools/sat/integer_base.h" #include "ortools/sat/model.h" #include "ortools/sat/presolve_context.h" #include "ortools/util/sorted_interval_list.h"