[CP-SAT] more tweakings

ortools/sat/BUILD.bazel

@@ -3920,6 +3920,7 @@ cc_library(
         "//ortools/base",
         "//ortools/base:stl_util",
         "//ortools/util:filelineiter",
+        "@abseil-cpp//absl/base:core_headers",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/log",

ortools/sat/cp_model_solver_test.cc

@@ -956,6 +956,7 @@ TEST(SolveCpModelTest, HintWithNegativeRef) {
 TEST(SolveCpModelTest, SolutionHintBasicTest) {
   SatParameters params;
   params.set_cp_model_presolve(false);
+  params.set_num_workers(1);
   for (int loop = 0; loop < 50; ++loop) {
     CpModelProto model_proto;
 

ortools/sat/integer_search.h

@@ -346,7 +346,7 @@ class ContinuousProber {
 
  private:
   static const int kTestLimitPeriod = 20;
-  static const int kLogPeriod = 1000;
+  static const int kLogPeriod = 5000;
   static const int kSyncPeriod = 50;
 
   SatSolver::Status ShaveLiteral(Literal literal);

ortools/sat/opb_reader.h

@@ -21,6 +21,7 @@
 #include <utility>
 #include <vector>
 
+#include "absl/base/attributes.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/log/check.h"
@@ -56,7 +57,8 @@ class OpbReader {
 
   // Loads the given opb filename into the given problem.
   // Returns true on success.
-  bool LoadAndValidate(const std::string& filename, CpModelProto* model) {
+  ABSL_MUST_USE_RESULT bool LoadAndValidate(const std::string& filename,
+                                            CpModelProto* model) {
     model->Clear();
     model->set_name(ExtractProblemName(filename));
 
@@ -72,17 +74,8 @@ class OpbReader {
       ProcessNewLine(line);
 
       // Check if the model is supported. It is not supported if one constant
-      // contains an integer that does not fit in int64_t.
-      // In that case, we create a dummy model with a single variable that
-      // overflows.
-      if (!model_is_supported_) {
-        model->Clear();
-        IntegerVariableProto* var = model->add_variables();
-        var->add_domain(std::numeric_limits<int64_t>::min());
-        var->add_domain(std::numeric_limits<int64_t>::max());
-        num_variables_ = 1;
-        return true;
-      }
+      // contains an integer that does not fit in an int64_t.
+      if (!model_is_supported_) return false;
     }
     if (num_lines == 0) {
       LOG(ERROR) << "File '" << filename << "' is empty or can't be read.";

ortools/sat/opb_reader_test.cc

@@ -107,7 +107,7 @@ TEST(LoadAndValidateBooleanProblemTest, IntegerOverflow) {
   const std::string filename =
       file::JoinPath(::testing::TempDir(), "file2.opb");
   CHECK_OK(file::SetContents(filename, file, file::Defaults()));
-  EXPECT_TRUE(reader.LoadAndValidate(filename, &problem));
+  EXPECT_FALSE(reader.LoadAndValidate(filename, &problem));
   EXPECT_FALSE(reader.model_is_supported());
 }
 

ortools/sat/primary_variables.cc

@@ -231,7 +231,8 @@ VariableRelationships ComputeVariableRelationships(const CpModelProto& model) {
       }
       var_is_secondary.Set(v);
       result.secondary_variables.push_back(v);
-      result.dependency_resolution_constraint_index.push_back(c);
+      result.dependency_resolution_constraint.push_back(model.constraints(c));
+      result.redundant_constraint_indices.push_back(c);
       break;
     }
 
@@ -295,14 +296,17 @@ VariableRelationships ComputeVariableRelationships(const CpModelProto& model) {
       var_is_secondary.Set(single_deducible_var);
       update_constraints_after_var_is_decided(single_deducible_var);
       result.secondary_variables.push_back(single_deducible_var);
-      result.dependency_resolution_constraint_index.push_back(c);
+      result.dependency_resolution_constraint.push_back(model.constraints(c));
+      result.redundant_constraint_indices.push_back(c);
     }
   }
 
   for (int i = 0; i < result.secondary_variables.size(); ++i) {
     const int var = result.secondary_variables[i];
-    const int c = result.dependency_resolution_constraint_index[i];
-    const ConstraintData& data = constraint_data[c];
+    ConstraintData data;
+    const ConstraintProto& ct = result.dependency_resolution_constraint[i];
+    GetRelationshipForConstraint(ct, &data.deducible_vars, &data.input_vars,
+                                 &data.preferred_to_deduce);
     for (const int v : data.input_vars) {
       if (var_is_secondary.IsSet(v)) {
         result.variable_dependencies.push_back({var, v});
@@ -326,9 +330,8 @@ bool ComputeAllVariablesFromPrimaryVariables(
   }
   for (int i = 0; i < relationships.secondary_variables.size(); ++i) {
     const int var = relationships.secondary_variables[i];
-    const int constraint_index =
-        relationships.dependency_resolution_constraint_index[i];
-    const ConstraintProto& ct = model.constraints(constraint_index);
+    const ConstraintProto& ct =
+        relationships.dependency_resolution_constraint[i];
     switch (ct.constraint_case()) {
       case ConstraintProto::kLinear: {
         const LinearConstraintProto& linear = ct.linear();

ortools/sat/primary_variables.h

@@ -40,11 +40,20 @@ namespace sat {
 // of the secondary variables.
 struct VariableRelationships {
   std::vector<int> secondary_variables;
-  std::vector<int> dependency_resolution_constraint_index;
+  std::vector<ConstraintProto> dependency_resolution_constraint;
+
   // A pair of(x, y) means that one needs to compute the value of y before
   // computing the value of x. This defines an implicit dependency DAG for
   // computing the secondary variables from the primary.
   std::vector<std::pair<int, int>> variable_dependencies;
+
+  // The list of model constraints that are redundant (ie., satisfied by
+  // construction) when the secondary variables are computed from the primary
+  // ones. In other words, a model has a solution for a set of primary
+  // variables {x_i} if and only if all the variable bounds and non-redundant
+  // constraints are satisfied after the secondary variables have been computed
+  // from the primary ones.
+  std::vector<int> redundant_constraint_indices;
 };
 
 // Compute the variable relationships for a given model. Note that there are

ortools/sat/sat_runner.cc

@@ -15,6 +15,7 @@
 #include <cstdlib>
 #include <functional>
 #include <iostream>
+#include <limits>
 #include <string>
 #include <vector>
 
@@ -177,10 +178,31 @@ bool LoadProblem(const std::string& filename, absl::string_view hint_file,
       absl::EndsWith(filename, ".wbo.bz2") ||
       absl::EndsWith(filename, ".wbo.gz")) {
     OpbReader reader;
-    reader.LoadAndValidate(filename, cp_model);
+    if (!reader.LoadAndValidate(filename, cp_model)) {
+      if (!reader.model_is_supported()) {  // Some constants are too large.
+        if (absl::GetFlag(FLAGS_competition_mode)) {
+          // We output the official UNSUPPORTED status.
+          std::cout << "s UNSUPPORTED" << std::endl;
+          return false;  // Bypass the solve part.
+        } else {
+          // Create a dummy model with a single variable that overflows.
+          // This way, the solver will return MODEL_INVALID instead of
+          // crashing.
+          IntegerVariableProto* var = cp_model->add_variables();
+          var->add_domain(std::numeric_limits<int64_t>::min());
+          var->add_domain(std::numeric_limits<int64_t>::max());
+          return true;  // Will still call solve() to get the status.
+        }
+      } else {
+        return false;  // Bypass the solve part.
+      }
+    }
+
     if (absl::GetFlag(FLAGS_competition_mode)) {
-      LogInPbCompetitionFormat(reader.num_variables(),
-                               cp_model->has_objective(), model, parameters);
+      const int num_variables =
+          reader.model_is_supported() ? reader.num_variables() : 1;
+      LogInPbCompetitionFormat(num_variables, cp_model->has_objective(), model,
+                               parameters);
     }
   } else if (absl::EndsWith(filename, ".cnf") ||
              absl::EndsWith(filename, ".cnf.xz") ||