From 0274d021ccdaa386516f71cf6380f2a19f62cf76 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 11 Feb 2022 13:40:22 +0100 Subject: [PATCH] [CP-SAT] reduce amount of logging --- ortools/sat/cp_model_lns.cc | 8 ++++++ ortools/sat/cp_model_lns.h | 3 +++ ortools/sat/optimization.cc | 46 +++++++++++++++++++++++++++----- ortools/sat/optimization.h | 9 +++---- ortools/sat/sat_parameters.proto | 3 ++- 5 files changed, 57 insertions(+), 12 deletions(-) diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc index 5c8581c9d5..034e33a096 100644 --- a/ortools/sat/cp_model_lns.cc +++ b/ortools/sat/cp_model_lns.cc @@ -55,6 +55,7 @@ NeighborhoodGeneratorHelper::NeighborhoodGeneratorHelper( InitializeHelperData(); RecomputeHelperData(); Synchronize(); + last_logging_time_ = absl::Now(); } void NeighborhoodGeneratorHelper::Synchronize() { @@ -204,6 +205,8 @@ void NeighborhoodGeneratorHelper::RecomputeHelperData() { for (int ct_index = 0; ct_index < constraints.size(); ++ct_index) { // We remove the interval constraints since we should have an equivalent // linear constraint somewhere else. + // TODO(user): Fix, the above is not true for a fixed size optional + // interval var. if (constraints[ct_index].constraint_case() == ConstraintProto::kInterval) { continue; } @@ -294,6 +297,10 @@ void NeighborhoodGeneratorHelper::RecomputeHelperData() { // // TODO(user): Exploit connected component while generating fragments. // TODO(user): Do not generate fragment not touching the objective. + const double freq = parameters_.log_frequency_in_seconds(); + absl::Time now = absl::Now(); + if (freq <= 0.0 || now <= last_logging_time_ + absl::Seconds(freq)) return; + std::vector component_sizes; for (const std::vector& component : components_) { component_sizes.push_back(component.size()); @@ -316,6 +323,7 @@ void NeighborhoodGeneratorHelper::RecomputeHelperData() { absl::StrCat("var:", active_variables_.size(), "/", num_variables, " constraints:", simplied_model_proto_.constraints().size(), "/", model_proto_.constraints().size(), compo_message)); + last_logging_time_ = now; } bool NeighborhoodGeneratorHelper::IsActive(int var) const { diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h index 9f4b67002f..bcd7d2bbf5 100644 --- a/ortools/sat/cp_model_lns.h +++ b/ortools/sat/cp_model_lns.h @@ -280,6 +280,9 @@ class NeighborhoodGeneratorHelper : public SubSolver { std::vector active_variables_ ABSL_GUARDED_BY(graph_mutex_); mutable absl::Mutex domain_mutex_; + + // Used to display periodic info to the log. + absl::Time last_logging_time_; }; // Base class for a CpModelProto neighborhood generator. diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 71c685e973..ee410e24b5 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -1274,9 +1274,20 @@ SatSolver::Status FindMultipleCoresForMaxHs( cores->clear(); SatSolver* sat_solver = model->GetOrCreate(); TimeLimit* limit = model->GetOrCreate(); + const double saved_dlimit = limit->GetDeterministicLimit(); + auto cleanup = ::absl::MakeCleanup([limit, saved_dlimit]() { + limit->ChangeDeterministicLimit(saved_dlimit); + }); + + bool first_loop = true; do { if (limit->LimitReached()) return SatSolver::LIMIT_REACHED; + // The order of assumptions do not matter. + // Randomizing it should improve diversity. + auto* random = model->GetOrCreate(); + std::shuffle(assumptions.begin(), assumptions.end(), *random); + const SatSolver::Status result = ResetAndSolveIntegerProblem(assumptions, model); if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; @@ -1291,7 +1302,6 @@ SatSolver::Status FindMultipleCoresForMaxHs( // Pick a random literal from the core and remove it from the set of // assumptions. CHECK(!core.empty()); - auto* random = model->GetOrCreate(); const Literal random_literal = core[absl::Uniform(*random, 0, core.size())]; for (int i = 0; i < assumptions.size(); ++i) { @@ -1301,6 +1311,14 @@ SatSolver::Status FindMultipleCoresForMaxHs( break; } } + + // Once we found at least one core, we impose a time limit to not spend + // too much time finding more. + if (first_loop) { + limit->ChangeDeterministicLimit( + std::min(saved_dlimit, limit->GetElapsedDeterministicTime() + 1.0)); + first_loop = false; + } } while (!assumptions.empty()); return SatSolver::ASSUMPTIONS_UNSAT; } @@ -1640,7 +1658,8 @@ SatSolver::Status CoreBasedOptimizer::Optimize() { " gap:", gap, "%", " assumptions:", term_indices.size(), " strat:", stratification_threshold_.value(), - " depth:", max_depth); + " depth:", max_depth, + " bool: ", sat_solver_->NumVariables()); } // Convert integer_assumptions to Literals. @@ -1764,9 +1783,10 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( std::vector variables = objective_definition.vars; std::vector coefficients = objective_definition.coeffs; - SatSolver* sat_solver = model->GetOrCreate(); - IntegerTrail* integer_trail = model->GetOrCreate(); - IntegerEncoder* integer_encoder = model->GetOrCreate(); + auto* sat_solver = model->GetOrCreate(); + auto* integer_trail = model->GetOrCreate(); + auto* integer_encoder = model->GetOrCreate(); + auto* time_limit = model->GetOrCreate(); // This will be called each time a feasible solution is found. const auto process_solution = [&]() { @@ -1839,8 +1859,18 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( // TODO(user): Even though we keep the same solver, currently the solve is // not really done incrementally. It might be hard to improve though. // - // TODO(user): deal with time limit. + // TODO(user): C^c is broken when using SCIP. MPSolver::SolveWithProto(request, &response); + if (response.status() != MPSolverResponseStatus::MPSOLVER_OPTIMAL) { + // We currently abort if we have a non-optimal result. + // This is correct if we had a limit reached, but not in the other cases. + // + // TODO(user): It is actually easy to use a FEASIBLE result. If when + // passing it to SAT it is no feasbile, we can still create cores. If it + // is feasible, we have a solution, but we cannot increase the lower + // bound. + return SatSolver::LIMIT_REACHED; + } CHECK_EQ(response.status(), MPSolverResponseStatus::MPSOLVER_OPTIMAL); const IntegerValue mip_objective( @@ -1911,6 +1941,10 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( --iter; // "false" iteration, the lower bound does not increase. continue; } + } else if (result == SatSolver::LIMIT_REACHED) { + // Hack: we use a local limit internally that we restore at the end. + // However we still return LIMIT_REACHED in this case... + if (time_limit->LimitReached()) break; } else if (result != SatSolver::ASSUMPTIONS_UNSAT) { break; } diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index d6097bb811..99699dba57 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -114,10 +114,9 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore( LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, std::vector* solution); -// Model-based API, for now we just provide a basic algorithm that minimizes a -// given IntegerVariable by solving a sequence of decision problem by using -// SolveIntegerProblem(). Returns the status of the last solved decision -// problem. +// Model-based API to minimize a given IntegerVariable by solving a sequence of +// decision problem. Each problem is solved using SolveIntegerProblem(). Returns +// the status of the last solved decision problem. // // The feasible_solution_observer function will be called each time a new // feasible solution is found. @@ -223,7 +222,7 @@ class CoreBasedOptimizer { // on the industrial category, see // http://maxsat.ia.udl.cat/results/#wpms-industrial // -// TODO(user): This function brings dependency to the SCIP MIP solver which is +// TODO(user): This function requires linking with the SCIP MIP solver which is // quite big, maybe we should find a way not to do that. SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( const ObjectiveDefinition& objective_definition, diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 034bfd8a3d..4fdda4bcf1 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -383,7 +383,7 @@ message SatParameters { // Indicates how much logging should wait before logging periodic search // information from specialized workers (lb_tree_search, probing). // A value <= 0.0 will disable periodic logs. - optional double log_frequency_in_seconds = 212 [default = 30.0]; + optional double log_frequency_in_seconds = 212 [default = 0.0]; // Whether the solver should display per sub-solver search statistics. // This is only useful is log_search_progress is set to true, and if the @@ -636,6 +636,7 @@ message SatParameters { // If true, when the max-sat algo find a core, we compute the minimal number // of literals in the core that needs to be true to have a feasible solution. + // This is also called core exhaustion in more recent max-SAT papers. optional bool cover_optimization = 89 [default = true]; // In what order do we add the assumptions in a core-based max-sat algorithm