diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 3f51c4f34c..4614449dd7 100644 --- a/ortools/sat/BUILD.bazel +++ b/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", diff --git a/ortools/sat/cp_model_solver_test.cc b/ortools/sat/cp_model_solver_test.cc index 0fde989f94..cf5963e6b8 100644 --- a/ortools/sat/cp_model_solver_test.cc +++ b/ortools/sat/cp_model_solver_test.cc @@ -955,8 +955,8 @@ TEST(SolveCpModelTest, HintWithNegativeRef) { TEST(SolveCpModelTest, SolutionHintBasicTest) { SatParameters params; - params.set_num_workers(1); params.set_cp_model_presolve(false); + params.set_num_workers(1); for (int loop = 0; loop < 50; ++loop) { CpModelProto model_proto; diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index 6e65cd85f8..8e97be5ab5 100644 --- a/ortools/sat/integer_search.h +++ b/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); diff --git a/ortools/sat/opb_reader.h b/ortools/sat/opb_reader.h index feb70e0972..6432016c72 100644 --- a/ortools/sat/opb_reader.h +++ b/ortools/sat/opb_reader.h @@ -21,6 +21,7 @@ #include #include +#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::min()); - var->add_domain(std::numeric_limits::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."; diff --git a/ortools/sat/opb_reader_test.cc b/ortools/sat/opb_reader_test.cc index b89e86d0c8..b5479b086a 100644 --- a/ortools/sat/opb_reader_test.cc +++ b/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()); } diff --git a/ortools/sat/primary_variables.cc b/ortools/sat/primary_variables.cc index 14a9d0fa73..13959f6a69 100644 --- a/ortools/sat/primary_variables.cc +++ b/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(); diff --git a/ortools/sat/primary_variables.h b/ortools/sat/primary_variables.h index 259fb9720e..22f36911ea 100644 --- a/ortools/sat/primary_variables.h +++ b/ortools/sat/primary_variables.h @@ -40,11 +40,20 @@ namespace sat { // of the secondary variables. struct VariableRelationships { std::vector secondary_variables; - std::vector dependency_resolution_constraint_index; + std::vector 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> 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 redundant_constraint_indices; }; // Compute the variable relationships for a given model. Note that there are diff --git a/ortools/sat/sat_runner.cc b/ortools/sat/sat_runner.cc index cee8fd0bfb..24625b05eb 100644 --- a/ortools/sat/sat_runner.cc +++ b/ortools/sat/sat_runner.cc @@ -15,6 +15,7 @@ #include #include #include +#include #include #include @@ -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::min()); + var->add_domain(std::numeric_limits::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") ||