tweak subsolvers list; add focus on terms parameters to lb_objective_…

…search; fix bug in shared_tree

ortools/sat/BUILD.bazel

@@ -1721,6 +1721,7 @@ cc_binary(
         "//ortools/algorithms:sparse_permutation",
         "//ortools/base",
         "//ortools/base:file",
+        "//ortools/base:path",
         "//ortools/base:threadpool",
         "//ortools/lp_data:mps_reader",
         "//ortools/lp_data:proto_utils",

ortools/sat/cp_model_search.cc

@@ -508,16 +508,17 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
 
   {
     SatParameters new_params = base_params;
-    new_params.set_linearization_level(1);
     new_params.set_use_objective_lb_search(true);
-    if (base_params.use_dual_scheduling_heuristics()) {
-      AddDualSchedulingHeuristics(new_params);
-    }
-    strategies["objective_lb_search"] = new_params;
 
     new_params.set_linearization_level(0);
     strategies["objective_lb_search_no_lp"] = new_params;
 
+    new_params.set_linearization_level(1);
+    strategies["objective_lb_search"] = new_params;
+
+    if (base_params.use_dual_scheduling_heuristics()) {
+      AddDualSchedulingHeuristics(new_params);
+    }
     new_params.set_linearization_level(2);
     strategies["objective_lb_search_max_lp"] = new_params;
   }
@@ -548,6 +549,9 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
     strategies["probing_no_lp"] = new_params;
 
     new_params.set_linearization_level(2);
+    // We want to spend more time on the LP here.
+    new_params.set_add_lp_constraints_lazily(false);
+    new_params.set_root_lp_iterations(100'000);
     strategies["probing_max_lp"] = new_params;
   }
 
@@ -673,6 +677,15 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
     if (num_workers_to_generate >= 24) {
       names.push_back("objective_shaving_search");
     }
+    if (num_workers_to_generate >= 26) {
+      names.push_back("objective_lb_search_no_lp");
+    }
+    if (num_workers_to_generate >= 28) {
+      names.push_back("objective_lb_search_max_lp");
+    }
+    if (num_workers_to_generate >= 30) {
+      names.push_back("core_max_lp");
+    }
 #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
     if (absl::GetFlag(FLAGS_cp_model_use_max_hs)) names.push_back("max_hs");
 #endif  // !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
@@ -725,7 +738,7 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
     if (params.use_probing_search() && cp_model.variables().empty()) continue;
 
     if (cp_model.has_objective() && !cp_model.objective().vars().empty()) {
-      // Disable core search if only 1 term in the objective.
+      // Disable core search if there is only 1 term in the objective.
       if (cp_model.objective().vars().size() == 1 &&
           params.optimize_with_core()) {
         continue;

ortools/sat/integer_search.cc

@@ -17,6 +17,7 @@
 #include <cmath>
 #include <cstdint>
 #include <functional>
+#include <numeric>
 #include <random>
 #include <vector>
 
@@ -336,26 +337,69 @@ std::function<BooleanOrIntegerLiteral()> SatSolverHeuristic(Model* model) {
 
 // TODO(user): Do we need a mechanism to reduce the range of possible gaps
 // when nothing gets proven? This could be a parameter or some adaptative code.
-std::function<BooleanOrIntegerLiteral()> ShaveObjectiveLb(Model* model) {
+std::function<BooleanOrIntegerLiteral()> ShaveObjectiveLb(
+    Model* model, double focus_on_terms_probability) {
   auto* objective_definition = model->GetOrCreate<ObjectiveDefinition>();
   const IntegerVariable obj_var = objective_definition->objective_var;
   auto* integer_trail = model->GetOrCreate<IntegerTrail>();
   auto* sat_solver = model->GetOrCreate<SatSolver>();
   auto* random = model->GetOrCreate<ModelRandomGenerator>();
 
-  return [obj_var, integer_trail, sat_solver, random]() {
+  std::vector<int> random_order;
+  if (objective_definition->vars.size() > 1) {
+    random_order.resize(objective_definition->vars.size());
+    std::iota(random_order.begin(), random_order.end(), 0);
+  }
+
+  const auto random_slack = [random](IntegerValue lb, IntegerValue ub) {
+    const IntegerValue mid = (ub - lb) / 2;
+    return absl::LogUniform<int64_t>(*random, 0, mid.value());
+  };
+
+  return [obj_var, integer_trail, sat_solver, random, random_order,
+          objective_definition, random_slack,
+          focus_on_terms_probability]() mutable {
     BooleanOrIntegerLiteral result;
     const int level = sat_solver->CurrentDecisionLevel();
-    if (level > 0 || obj_var == kNoIntegerVariable) return result;
+    if (random_order.empty() ||
+        absl::Bernoulli(*random, 1.0 - focus_on_terms_probability)) {
+      if (level > 0 || obj_var == kNoIntegerVariable ||
+          integer_trail->IsFixed(obj_var)) {
+        return result;
+      }
+
+      const IntegerValue obj_lb = integer_trail->LowerBound(obj_var);
+      const IntegerValue obj_ub = integer_trail->UpperBound(obj_var);
+      const IntegerValue new_ub = obj_lb + random_slack(obj_lb, obj_ub);
+      result.integer_literal = IntegerLiteral::LowerOrEqual(obj_var, new_ub);
+      return result;
+    }
 
-    const IntegerValue obj_lb = integer_trail->LowerBound(obj_var);
-    const IntegerValue obj_ub = integer_trail->UpperBound(obj_var);
-    if (obj_lb == obj_ub) return result;
-    const IntegerValue mid = (obj_ub - obj_lb) / 2;
-    const IntegerValue new_ub =
-        obj_lb + absl::LogUniform<int64_t>(*random, 0, mid.value());
+    if (level == 0) {
+      VLOG(2) << "ShaveObjectiveLb: randomize " << random_order.size()
+              << " terms";
+      DCHECK_EQ(random_order.size(), objective_definition->vars.size());
+      std::shuffle(random_order.begin(), random_order.end(), *random);
+    }
 
-    result.integer_literal = IntegerLiteral::LowerOrEqual(obj_var, new_ub);
+    for (const int index : random_order) {
+      const IntegerVariable var = objective_definition->vars[index];
+      const IntegerValue coeff = objective_definition->coeffs[index];
+      if (integer_trail->IsFixed(var) || coeff == 0) continue;
+
+      const IntegerValue lb = integer_trail->LowerBound(var);
+      const IntegerValue ub = integer_trail->UpperBound(var);
+      const IntegerValue slack = random_slack(lb, ub);
+      if (coeff > 0) {
+        result.integer_literal = IntegerLiteral::LowerOrEqual(var, lb + slack);
+      } else {
+        result.integer_literal =
+            IntegerLiteral::GreaterOrEqual(var, ub - slack);
+      }
+      return result;
+    }
+
+    // Returns no-decision.
     return result;
   };
 }
@@ -698,8 +742,12 @@ void ConfigureSearchHeuristics(Model* model) {
           SequentialSearch({decision_policy, heuristics.fixed_search});
       decision_policy = IntegerValueSelectionHeuristic(decision_policy, model);
       if (parameters.use_objective_lb_search()) {
-        heuristics.decision_policies = {
-            SequentialSearch({ShaveObjectiveLb(model), decision_policy})};
+        heuristics.decision_policies = {SequentialSearch(
+            {ShaveObjectiveLb(
+                 model,
+                 parameters
+                     .focus_on_terms_in_objective_lb_search_probability()),
+             decision_policy})};
       } else {
         heuristics.decision_policies = {decision_policy};
       }

ortools/sat/parameters_validation.cc

@@ -101,6 +101,7 @@ std::string ValidateParameters(const SatParameters& params) {
   TEST_IN_RANGE(min_num_lns_workers, 0, kMaxReasonableParallelism);
   TEST_IN_RANGE(shared_tree_num_workers, 0, kMaxReasonableParallelism);
   TEST_IN_RANGE(interleave_batch_size, 0, kMaxReasonableParallelism);
+  TEST_IN_RANGE(focus_on_terms_in_objective_lb_search_probability, 0.0, 1.0);
 
   // TODO(user): Consider using annotations directly in the proto for these
   // validation. It is however not open sourced.

ortools/sat/sat_parameters.proto

@@ -1036,6 +1036,12 @@ message SatParameters {
   // minimizing) starting from the lower bound of the objective.
   optional bool use_objective_lb_search = 228 [default = false];
 
+  // With the given probability, objective_lb_search will fix each terms of the
+  // objective following an random order computed each time search returns to
+  // the root node.
+  optional double focus_on_terms_in_objective_lb_search_probability = 231
+      [default = 0.5];
+
   // This search differs from the previous search as it will not use assumptions
   // to bound the objective, and it will recreate a full model with the
   // hardcoded objective value.

ortools/sat/sat_runner.cc

@@ -11,55 +11,31 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
-#include <cstdint>
 #include <cstdlib>
-#include <memory>
 #include <string>
-#include <utility>
-#include <vector>
 
 #include "absl/flags/flag.h"
 #include "absl/flags/parse.h"
 #include "absl/flags/usage.h"
 #include "absl/log/check.h"
 #include "absl/log/flags.h"
 #include "absl/log/initialize.h"
-#include "absl/random/random.h"
-#include "absl/status/status.h"
 #include "absl/strings/match.h"
-#include "absl/strings/numbers.h"
-#include "absl/strings/str_cat.h"
-#include "absl/strings/str_format.h"
 #include "absl/strings/string_view.h"
 #include "google/protobuf/text_format.h"
-#include "ortools/algorithms/sparse_permutation.h"
 #include "ortools/base/helpers.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/options.h"
-#include "ortools/base/timer.h"
-#include "ortools/linear_solver/linear_solver.pb.h"
-#include "ortools/lp_data/lp_data.h"
-#include "ortools/lp_data/mps_reader.h"
-#include "ortools/lp_data/proto_utils.h"
+#include "ortools/base/path.h"
 #include "ortools/sat/boolean_problem.h"
 #include "ortools/sat/boolean_problem.pb.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
-#include "ortools/sat/lp_utils.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/opb_reader.h"
-#include "ortools/sat/optimization.h"
-#include "ortools/sat/pb_constraint.h"
-#include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_cnf_reader.h"
 #include "ortools/sat/sat_parameters.pb.h"
-#include "ortools/sat/sat_solver.h"
-#include "ortools/sat/simplification.h"
-#include "ortools/sat/symmetry.h"
 #include "ortools/util/file_util.h"
-#include "ortools/util/logging.h"
-#include "ortools/util/strong_integers.h"
-#include "ortools/util/time_limit.h"
 
 ABSL_FLAG(
     std::string, input, "",
@@ -83,7 +59,25 @@ namespace operations_research {
 namespace sat {
 namespace {
 
-bool LoadBooleanProblem(const std::string& filename, CpModelProto* cp_model) {
+void TryToRemoveSuffix(absl::string_view suffix, std::string* str) {
+  if (file::Extension(*str) == suffix) *str = file::Stem(*str);
+}
+
+std::string ExtractName(const std::string& full_filename) {
+  std::string filename = std::string(file::Basename(full_filename));
+  // The order is important as '.pb.txt.gz' is a common suffix.
+  TryToRemoveSuffix("gz", &filename);
+  TryToRemoveSuffix("txt", &filename);
+  TryToRemoveSuffix("pb", &filename);
+  TryToRemoveSuffix("pbtxt", &filename);
+  TryToRemoveSuffix("proto", &filename);
+  TryToRemoveSuffix("prototxt", &filename);
+  TryToRemoveSuffix("textproto", &filename);
+  TryToRemoveSuffix("bin", &filename);
+  return filename;
+}
+
+bool LoadProblem(const std::string& filename, CpModelProto* cp_model) {
   if (absl::EndsWith(filename, ".opb") ||
       absl::EndsWith(filename, ".opb.bz2")) {
     OpbReader reader;
@@ -106,6 +100,9 @@ bool LoadBooleanProblem(const std::string& filename, CpModelProto* cp_model) {
     LOG(INFO) << "Reading a CpModelProto.";
     *cp_model = ReadFileToProtoOrDie<CpModelProto>(filename);
   }
+  if (cp_model->name().empty()) {
+    cp_model->set_name(ExtractName(filename));
+  }
   return true;
 }
 
@@ -127,7 +124,7 @@ int Run() {
   google::protobuf::Arena arena;
   CpModelProto* cp_model =
       google::protobuf::Arena::CreateMessage<CpModelProto>(&arena);
-  if (!LoadBooleanProblem(absl::GetFlag(FLAGS_input), cp_model)) {
+  if (!LoadProblem(absl::GetFlag(FLAGS_input), cp_model)) {
     CpSolverResponse response;
     response.set_status(CpSolverStatus::MODEL_INVALID);
     return EXIT_SUCCESS;

ortools/sat/subsolver.h

@@ -27,7 +27,7 @@
 #include <vector>
 
 #include "absl/strings/string_view.h"
-#include "ortools/base/integral_types.h"
+#include "ortools/base/types.h"
 #include "ortools/util/stats.h"
 
 #if !defined(__PORTABLE_PLATFORM__)

ortools/sat/table.h

@@ -19,7 +19,7 @@
 #include <vector>
 
 #include "absl/types/span.h"
-#include "ortools/base/integral_types.h"
+#include "ortools/base/types.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"

ortools/sat/work_assignment.cc

@@ -178,7 +178,9 @@ absl::Span<const int> ProtoTrail::NodeIds(int level) const {
 }
 
 absl::Span<const ProtoLiteral> ProtoTrail::Implications(int level) const {
-  DCHECK_LE(level, decision_indexes_.size());
+  if (level > decision_indexes_.size()) {
+    return absl::MakeSpan(literals_.data(), 0);
+  }
   int start = level == 0 ? 0 : decision_indexes_[level - 1] + 1;
   int end = level == decision_indexes_.size() ? node_ids_.size()
                                               : decision_indexes_[level];
@@ -561,20 +563,19 @@ bool SharedTreeWorker::AddImplications(
 }
 
 bool SharedTreeWorker::SyncWithLocalTrail() {
-  if (sat_solver_->CurrentDecisionLevel() > assigned_tree_.MaxLevel()) {
-    return sat_solver_->FinishPropagation() && helper_->BeforeTakingDecision();
-  }
-  while (sat_solver_->CurrentDecisionLevel() <= assigned_tree_.MaxLevel()) {
+  while (true) {
+    if (!sat_solver_->FinishPropagation()) return false;
     // Ensure we are at fixed point w.r.t. implications in the tree up to the
     // current level.
-    while (AddImplications(
-        assigned_tree_.Implications(sat_solver_->CurrentDecisionLevel()))) {
-      if (!sat_solver_->FinishPropagation()) return false;
+    if (AddImplications(
+            assigned_tree_.Implications(sat_solver_->CurrentDecisionLevel()))) {
+      continue;
     }
     if (!helper_->BeforeTakingDecision()) return false;
     const int level = sat_solver_->CurrentDecisionLevel();
-    // Make sure the next assigned decision makes sense if there is one.
+    if (level >= assigned_tree_.MaxLevel()) break;
     if (level == assigned_tree_.MaxLevel()) break;
+    // The next decision is assigned, make sure it makes sense.
     const Literal next_decision = assigned_tree_literals_[level];
     if (!sat_solver_->Assignment().LiteralIsAssigned(next_decision)) break;
     if (sat_solver_->Assignment().LiteralIsFalse(next_decision)) {