[CP-SAT] reduce amount of logging

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<int> component_sizes;
   for (const std::vector<int>& 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 {

ortools/sat/cp_model_lns.h

@@ -280,6 +280,9 @@ class NeighborhoodGeneratorHelper : public SubSolver {
   std::vector<int> 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.

ortools/sat/optimization.cc

@@ -1274,9 +1274,20 @@ SatSolver::Status FindMultipleCoresForMaxHs(
   cores->clear();
   SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
   TimeLimit* limit = model->GetOrCreate<TimeLimit>();
+  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<ModelRandomGenerator>();
+    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<ModelRandomGenerator>();
     const Literal random_literal =
         core[absl::Uniform<int>(*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<IntegerVariable> variables = objective_definition.vars;
   std::vector<IntegerValue> coefficients = objective_definition.coeffs;
 
-  SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
-  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
-  IntegerEncoder* integer_encoder = model->GetOrCreate<IntegerEncoder>();
+  auto* sat_solver = model->GetOrCreate<SatSolver>();
+  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+  auto* integer_encoder = model->GetOrCreate<IntegerEncoder>();
+  auto* time_limit = model->GetOrCreate<TimeLimit>();
 
   // 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;
     }

ortools/sat/optimization.h

@@ -114,10 +114,9 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore(
     LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver,
     std::vector<bool>* 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,

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