From c292221427b6178ed5bca35cdba2a487dc6d50d0 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 30 Jan 2025 14:27:23 +0100 Subject: [PATCH] [CP-SAT] experiment with prefered linearization_level in lns; fuzzer bugs fixed --- ortools/sat/cp_model_copy.cc | 32 ++++++++++++++++++++++---------- ortools/sat/cp_model_copy.h | 5 +++-- ortools/sat/cp_model_presolve.cc | 4 ++-- ortools/sat/cp_model_solver.cc | 20 +++++++++++++------- ortools/sat/linear_relaxation.cc | 8 +++++--- 5 files changed, 45 insertions(+), 24 deletions(-) diff --git a/ortools/sat/cp_model_copy.cc b/ortools/sat/cp_model_copy.cc index ff05407aef..72eea80387 100644 --- a/ortools/sat/cp_model_copy.cc +++ b/ortools/sat/cp_model_copy.cc @@ -119,7 +119,9 @@ bool ModelCopy::ImportAndSimplifyConstraints( } break; case ConstraintProto::kLinear: - if (!CopyLinear(ct)) return CreateUnsatModel(c, ct); + if (!CopyLinear(ct, /*canonicalize=*/first_copy)) { + return CreateUnsatModel(c, ct); + } break; case ConstraintProto::kIntProd: if (!CopyIntProd(ct, ignore_names)) return CreateUnsatModel(c, ct); @@ -407,8 +409,9 @@ bool ModelCopy::CopyBoolAndWithDupSupport(const ConstraintProto& ct) { return true; } -bool ModelCopy::CopyLinearExpression(const LinearExpressionProto& expr, - LinearExpressionProto* dst) { +bool ModelCopy::CopyLinearExpression( + const LinearExpressionProto& expr, LinearExpressionProto* dst, + absl::Span enforcement_literals) { non_fixed_variables_.clear(); non_fixed_coefficients_.clear(); int64_t offset = expr.offset(); @@ -436,10 +439,13 @@ bool ModelCopy::CopyLinearExpression(const LinearExpressionProto& expr, non_fixed_variables_.end()); dst->mutable_coeffs()->Add(non_fixed_coefficients_.begin(), non_fixed_coefficients_.end()); + // TODO(user): We could save work by only doing this if this is the first + // copy. + context_->CanonicalizeLinearExpression(enforcement_literals, dst); return true; } -bool ModelCopy::CopyLinear(const ConstraintProto& ct) { +bool ModelCopy::CopyLinear(const ConstraintProto& ct, bool canonicalize) { non_fixed_variables_.clear(); non_fixed_coefficients_.clear(); int64_t offset = 0; @@ -516,6 +522,9 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) { linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(), non_fixed_coefficients_.end()); FillDomainInProto(tight_domain, linear); + if (canonicalize) { + context_->CanonicalizeLinearConstraint(new_ct); + } return true; } @@ -708,11 +717,14 @@ bool ModelCopy::CopyInterval(const ConstraintProto& ct, int c, } *new_ct->mutable_enforcement_literal() = ct.enforcement_literal(); CopyLinearExpression(ct.interval().start(), - new_ct->mutable_interval()->mutable_start()); + new_ct->mutable_interval()->mutable_start(), + ct.enforcement_literal()); CopyLinearExpression(ct.interval().size(), - new_ct->mutable_interval()->mutable_size()); + new_ct->mutable_interval()->mutable_size(), + ct.enforcement_literal()); CopyLinearExpression(ct.interval().end(), - new_ct->mutable_interval()->mutable_end()); + new_ct->mutable_interval()->mutable_end(), + ct.enforcement_literal()); return true; } @@ -778,10 +790,10 @@ bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) { AddLinearExpressionToLinearConstraint(itv.start(), 1, mutable_linear); AddLinearExpressionToLinearConstraint(itv.size(), 1, mutable_linear); AddLinearExpressionToLinearConstraint(itv.end(), -1, mutable_linear); - if (!CopyLinear(tmp_constraint_)) return false; + if (!CopyLinear(tmp_constraint_, true)) return false; } - // An enforced interval must have is size non-negative. + // An enforced interval must have its size non-negative. const LinearExpressionProto& size_expr = itv.size(); if (context_->MinOf(size_expr) < 0) { tmp_constraint_.Clear(); @@ -791,7 +803,7 @@ bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) { tmp_constraint_.mutable_linear()->add_domain(-size_expr.offset()); tmp_constraint_.mutable_linear()->add_domain( std::numeric_limits::max()); - if (!CopyLinear(tmp_constraint_)) return false; + if (!CopyLinear(tmp_constraint_, true)) return false; } return true; diff --git a/ortools/sat/cp_model_copy.h b/ortools/sat/cp_model_copy.h index 8522af873d..d6fdf13006 100644 --- a/ortools/sat/cp_model_copy.h +++ b/ortools/sat/cp_model_copy.h @@ -90,9 +90,10 @@ class ModelCopy { bool CopyIntProd(const ConstraintProto& ct, bool ignore_names); bool CopyIntDiv(const ConstraintProto& ct, bool ignore_names); bool CopyIntMod(const ConstraintProto& ct, bool ignore_names); - bool CopyLinear(const ConstraintProto& ct); + bool CopyLinear(const ConstraintProto& ct, bool canonicalize); bool CopyLinearExpression(const LinearExpressionProto& expr, - LinearExpressionProto* dst); + LinearExpressionProto* dst, + absl::Span enforcement_literals = {}); bool CopyAutomaton(const ConstraintProto& ct); bool CopyTable(const ConstraintProto& ct); bool CopyAllDiff(const ConstraintProto& ct); diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 34794cd3cf..c3056756d2 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -5866,8 +5866,8 @@ bool CpModelPresolver::PresolveNoOverlap2DFramed( // Something can be outside of the frame. return false; } - if (2 * box.bounding_area.SizeX() <= framed_region.SizeX() || - 2 * box.bounding_area.SizeY() <= framed_region.SizeY()) { + if (2 * box.x_size <= framed_region.SizeX() || + 2 * box.y_size <= framed_region.SizeY()) { // We can fit two boxes in the delimited space between the fixed boxes, so // we cannot replace it by an at-most-one. return false; diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index ca1e5de76b..5f9be71b2f 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1192,8 +1192,10 @@ class LnsSolver : public SubSolver { public: LnsSolver(std::unique_ptr generator, const SatParameters& lns_parameters, - NeighborhoodGeneratorHelper* helper, SharedClasses* shared) + NeighborhoodGeneratorHelper* helper, SharedClasses* shared, + int preferred_linearization_level = 0) : SubSolver(generator->name(), INCOMPLETE), + preferred_linearization_level_(preferred_linearization_level), generator_(std::move(generator)), helper_(helper), lns_parameters_(lns_parameters), @@ -1274,13 +1276,13 @@ class LnsSolver : public SubSolver { // TODO(user): Tune these. // TODO(user): This could be a good candidate for bandits. const int64_t stall = generator_->num_consecutive_non_improving_calls(); + std::string search_info; const int search_index = stall < 10 ? 0 : task_id % 2; - absl::string_view search_info; switch (search_index) { case 0: local_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); - local_params.set_linearization_level(0); - search_info = "auto_l0"; + local_params.set_linearization_level(preferred_linearization_level_); + search_info = absl::StrCat("auto_l", preferred_linearization_level_); break; default: local_params.set_search_branching(SatParameters::PORTFOLIO_SEARCH); @@ -1616,6 +1618,7 @@ class LnsSolver : public SubSolver { } private: + int preferred_linearization_level_ = 0; std::unique_ptr generator_; NeighborhoodGeneratorHelper* helper_; const SatParameters lns_parameters_; @@ -1881,6 +1884,9 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) { } } + // For routing, the LP relaxation seems pretty important, so we prefer an + // high linearization level to solve LNS subproblems. + const int routing_lin_level = 2; const int num_circuit = static_cast( helper->TypeToConstraints(ConstraintProto::kCircuit).size()); const int num_routes = static_cast( @@ -1890,13 +1896,13 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) { reentrant_interleaved_subsolvers.push_back(std::make_unique( std::make_unique( helper, name_filter.LastName()), - lns_params, helper, shared)); + lns_params, helper, shared, routing_lin_level)); } if (name_filter.Keep("routing_path_lns")) { reentrant_interleaved_subsolvers.push_back(std::make_unique( std::make_unique( helper, name_filter.LastName()), - lns_params, helper, shared)); + lns_params, helper, shared, routing_lin_level)); } } if (num_routes > 0 || num_circuit > 1) { @@ -1904,7 +1910,7 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) { reentrant_interleaved_subsolvers.push_back(std::make_unique( std::make_unique( helper, name_filter.LastName()), - lns_params, helper, shared)); + lns_params, helper, shared, routing_lin_level)); } } } diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index b1c711d4d9..db5723824d 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -1056,10 +1056,12 @@ void AppendNoOverlap2dRelaxation(const ConstraintProto& ct, Model* model, intervals_repository->IsPresent(x_intervals[i]) ? intervals_repository->PresenceLiteral(y_intervals[i]) : intervals_repository->PresenceLiteral(x_intervals[i]); - const IntegerValue area_min = - integer_trail->LevelZeroLowerBound(x_sizes[i]) * + const IntegerValue x_size = + integer_trail->LevelZeroLowerBound(x_sizes[i]); + const IntegerValue y_size = integer_trail->LevelZeroLowerBound(y_sizes[i]); - if (area_min > 0) { + if (x_size > 0 && y_size > 0) { + const IntegerValue area_min = x_size * y_size; // Note that intervals that must be absent can have negative sizes. // Not including the term if we don't have a view is ok. (void)lc.AddLiteralTerm(presence_literal, area_min);