diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 3c258329eb..6b8ac4b2a1 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -113,9 +113,6 @@ message ElementConstraintProto { // This is not really a constraint. It is there so it can be referred by other // constraints using this "interval" concept. // -// IMPORTANT: All intervals must appear before they are used. This is enforced -// by our validation. -// // IMPORTANT: For now, this constraint do not enforce any relations on the // components, and it is up to the client to add in the model: // - enforcement => start + size == end. diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 11990b3150..8ad72a9194 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -118,8 +118,8 @@ std::string ValidateIntegerVariable(const CpModelProto& model, int v) { return ""; } -std::string ValidateArgumentReferencesInConstraint(const CpModelProto& model, - int c) { +std::string ValidateVariablesUsedInConstraint(const CpModelProto& model, + int c) { const ConstraintProto& ct = model.constraints(c); IndexReferences references = GetReferencesUsedByConstraint(ct); for (const int v : references.variables) { @@ -142,12 +142,19 @@ std::string ValidateArgumentReferencesInConstraint(const CpModelProto& model, ProtobufShortDebugString(ct)); } } + return ""; +} + +std::string ValidateIntervalsUsedInConstraint(bool after_presolve, + const CpModelProto& model, + int c) { + const ConstraintProto& ct = model.constraints(c); for (const int i : UsedIntervals(ct)) { if (i < 0 || i >= model.constraints_size()) { return absl::StrCat("Out of bound interval ", i, " in constraint #", c, " : ", ProtobufShortDebugString(ct)); } - if (i >= c) { + if (after_presolve && i >= c) { return absl::StrCat("Interval ", i, " in constraint #", c, " must appear before in the list of constraints :", ProtobufShortDebugString(ct)); @@ -836,32 +843,25 @@ std::string ValidateSolutionHint(const CpModelProto& model) { } // namespace -std::string ValidateCpModel(const CpModelProto& model) { +std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) { for (int v = 0; v < model.variables_size(); ++v) { RETURN_IF_NOT_EMPTY(ValidateIntegerVariable(model, v)); } - // Checks all variable references, and validate intervals before scanning the - // rest of the constraints. - for (int c = 0; c < model.constraints_size(); ++c) { - RETURN_IF_NOT_EMPTY(ValidateArgumentReferencesInConstraint(model, c)); - - const ConstraintProto& ct = model.constraints(c); - if (ct.constraint_case() == ConstraintProto::kInterval) { - RETURN_IF_NOT_EMPTY(ValidateIntervalConstraint(model, ct)); - } - } + // We need to validate the intervals used first, so we add these constraints + // here so that we can validate them in a second pass. + std::vector constraints_using_intervals; for (int c = 0; c < model.constraints_size(); ++c) { + RETURN_IF_NOT_EMPTY(ValidateVariablesUsedInConstraint(model, c)); + // By default, a constraint does not support enforcement literals except if // explicitly stated by setting this to true below. bool support_enforcement = false; // Other non-generic validations. - // TODO(user): validate all constraints. const ConstraintProto& ct = model.constraints(c); - const ConstraintProto::ConstraintCase type = ct.constraint_case(); - switch (type) { + switch (ct.constraint_case()) { case ConstraintProto::ConstraintCase::kBoolOr: support_enforcement = true; break; @@ -914,13 +914,17 @@ std::string ValidateCpModel(const CpModelProto& model) { RETURN_IF_NOT_EMPTY(ValidateRoutesConstraint(model, ct)); break; case ConstraintProto::ConstraintCase::kInterval: + RETURN_IF_NOT_EMPTY(ValidateIntervalConstraint(model, ct)); support_enforcement = true; break; case ConstraintProto::ConstraintCase::kCumulative: - RETURN_IF_NOT_EMPTY(ValidateCumulativeConstraint(model, ct)); + constraints_using_intervals.push_back(c); + break; + case ConstraintProto::ConstraintCase::kNoOverlap: + constraints_using_intervals.push_back(c); break; case ConstraintProto::ConstraintCase::kNoOverlap2D: - RETURN_IF_NOT_EMPTY(ValidateNoOverlap2DConstraint(model, ct)); + constraints_using_intervals.push_back(c); break; case ConstraintProto::ConstraintCase::kReservoir: RETURN_IF_NOT_EMPTY(ValidateReservoirConstraint(model, ct)); @@ -946,6 +950,27 @@ std::string ValidateCpModel(const CpModelProto& model) { } } } + + // Extra validation for constraint using intervals. + for (const int c : constraints_using_intervals) { + RETURN_IF_NOT_EMPTY( + ValidateIntervalsUsedInConstraint(after_presolve, model, c)); + + const ConstraintProto& ct = model.constraints(c); + switch (ct.constraint_case()) { + case ConstraintProto::ConstraintCase::kCumulative: + RETURN_IF_NOT_EMPTY(ValidateCumulativeConstraint(model, ct)); + break; + case ConstraintProto::ConstraintCase::kNoOverlap: + break; + case ConstraintProto::ConstraintCase::kNoOverlap2D: + RETURN_IF_NOT_EMPTY(ValidateNoOverlap2DConstraint(model, ct)); + break; + default: + LOG(DFATAL) << "Shouldn't be here"; + } + } + if (model.has_objective() && model.has_floating_point_objective()) { return "A model cannot have both an objective and a floating point " "objective."; diff --git a/ortools/sat/cp_model_checker.h b/ortools/sat/cp_model_checker.h index dc4ddca538..f19a8949ea 100644 --- a/ortools/sat/cp_model_checker.h +++ b/ortools/sat/cp_model_checker.h @@ -28,11 +28,15 @@ namespace sat { // proto comments. Returns an empty string if it is the case, otherwise fails at // the first error and returns a human-readable description of the issue. // +// The extra parameter is internal and mainly for debugging. After the problem +// has been presolved, we have a stricter set of properties we want to enforce. +// // TODO(user): Add any needed overflow validation because we are far from // exhaustive. We could also run a small presolve that tighten variable bounds // before the overflow check to facilitate the lives of our users, but it is a // some work to put in place. -std::string ValidateCpModel(const CpModelProto& model); +std::string ValidateCpModel(const CpModelProto& model, + bool after_presolve = false); // Verifies that the given variable assignment is a feasible solution of the // given model. The values vector should be in one to one correspondence with diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 39247d7f5b..915e5d9003 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -7115,11 +7115,16 @@ ModelCopy::ModelCopy(PresolveContext* context) : context_(context) {} // contains an interval or if we add a field to an existing constraint. Find a // way to remind contributor to not forget this. bool ModelCopy::ImportAndSimplifyConstraints( - const CpModelProto& in_model, const std::vector& ignored_constraints) { + const CpModelProto& in_model, const std::vector& ignored_constraints, + bool first_copy) { const absl::flat_hash_set ignored_constraints_set( ignored_constraints.begin(), ignored_constraints.end()); context_->InitializeNewDomains(); + // If first_copy is true, we reorder the scheduling constraint to be sure they + // refer to interval before them. + std::vector constraints_using_intervals; + starting_constraint_index_ = context_->working_model->constraints_size(); for (int c = 0; c < in_model.constraints_size(); ++c) { if (ignored_constraints_set.contains(c)) continue; @@ -7128,50 +7133,71 @@ bool ModelCopy::ImportAndSimplifyConstraints( if (OneEnforcementLiteralIsFalse(ct)) continue; switch (ct.constraint_case()) { - case ConstraintProto::CONSTRAINT_NOT_SET: { + case ConstraintProto::CONSTRAINT_NOT_SET: break; - } - case ConstraintProto::kBoolOr: { + case ConstraintProto::kBoolOr: if (!CopyBoolOr(ct)) return CreateUnsatModel(); break; - } - case ConstraintProto::kBoolAnd: { + case ConstraintProto::kBoolAnd: if (!CopyBoolAnd(ct)) return CreateUnsatModel(); break; - } - case ConstraintProto::kLinear: { + case ConstraintProto::kLinear: if (!CopyLinear(ct)) return CreateUnsatModel(); break; - } - case ConstraintProto::kAtMostOne: { + case ConstraintProto::kAtMostOne: if (!CopyAtMostOne(ct)) return CreateUnsatModel(); break; - } - case ConstraintProto::kExactlyOne: { + case ConstraintProto::kExactlyOne: if (!CopyExactlyOne(ct)) return CreateUnsatModel(); break; - } - case ConstraintProto::kInterval: { + case ConstraintProto::kInterval: if (!CopyInterval(ct, c)) return CreateUnsatModel(); break; - } - case ConstraintProto::kNoOverlap: { - CopyAndMapNoOverlap(ct); + case ConstraintProto::kNoOverlap: + if (first_copy) { + constraints_using_intervals.push_back(c); + } else { + CopyAndMapNoOverlap(ct); + } break; - } - case ConstraintProto::kNoOverlap2D: { - CopyAndMapNoOverlap2D(ct); + case ConstraintProto::kNoOverlap2D: + if (first_copy) { + constraints_using_intervals.push_back(c); + } else { + CopyAndMapNoOverlap2D(ct); + } break; - } - case ConstraintProto::kCumulative: { - CopyAndMapCumulative(ct); + case ConstraintProto::kCumulative: + if (first_copy) { + constraints_using_intervals.push_back(c); + } else { + CopyAndMapCumulative(ct); + } break; - } - default: { + default: *context_->working_model->add_constraints() = ct; - } } } + + // This should be empty if first_copy is false. + DCHECK(first_copy || constraints_using_intervals.empty()); + for (const int c : constraints_using_intervals) { + const ConstraintProto& ct = in_model.constraints(c); + switch (ct.constraint_case()) { + case ConstraintProto::kNoOverlap: + CopyAndMapNoOverlap(ct); + break; + case ConstraintProto::kNoOverlap2D: + CopyAndMapNoOverlap2D(ct); + break; + case ConstraintProto::kCumulative: + CopyAndMapCumulative(ct); + break; + default: + LOG(DFATAL) << "Shouldn't be here."; + } + } + return true; } @@ -7427,7 +7453,7 @@ bool ModelCopy::CreateUnsatModel() { bool ImportConstraintsWithBasicPresolveIntoContext(const CpModelProto& in_model, PresolveContext* context) { ModelCopy copier(context); - if (copier.ImportAndSimplifyConstraints(in_model, {})) { + if (copier.ImportAndSimplifyConstraints(in_model, {}, /*first_copy=*/true)) { CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(in_model, context); return true; @@ -7879,7 +7905,8 @@ CpSolverStatus CpModelPresolver::Presolve() { // INVALID model. But for our no-overflow preconditions, we might run into bad // situation that causes the final model to be invalid. { - const std::string error = ValidateCpModel(*context_->working_model); + const std::string error = + ValidateCpModel(*context_->working_model, /*after_presolve=*/true); if (!error.empty()) { SOLVER_LOG(logger_, "Error while validating postsolved model: ", error); return CpSolverStatus::MODEL_INVALID; diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 0a793859d0..fd492c9532 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -237,9 +237,13 @@ class ModelCopy { // It returns false iff the model is proven infeasible. // // It does not clear the constraints part of the working model of the context. - bool ImportAndSimplifyConstraints( - const CpModelProto& in_model, - const std::vector& ignored_constraints); + // + // Note(user): If first_copy is true, we will reorder the scheduling + // constraint so that they only use reference to previously defined intervals. + // This allow to be more efficient later in a few preprocessing steps. + bool ImportAndSimplifyConstraints(const CpModelProto& in_model, + const std::vector& ignored_constraints, + bool first_copy = false); private: // Overwrites the out_model to be unsat. Returns false. @@ -279,6 +283,10 @@ class ModelCopy { // Import the constraints from the in_model to the presolve context. // It performs on the fly simplification, and returns false if the // model is proved infeasible. +// +// This should only be called on the first copy of the user given model. +// Note that this reorder all constraints that use intervals last. We loose the +// user-defined order, but hopefully that should not matter too much. bool ImportConstraintsWithBasicPresolveIntoContext(const CpModelProto& in_model, PresolveContext* context);