always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] relax model validation requirement on scheduling constraints

Browse Source
This commit is contained in:
Laurent Perron
2022-01-12 12:05:12 +01:00
parent 5d3ccd2881
commit 23e3a7b989
5 changed files with 115 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
ortools/sat/cp_model.proto
View File

@@ -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.

63
ortools/sat/cp_model_checker.cc
View File

@@ -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<int> 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.";

6
ortools/sat/cp_model_checker.h
View File

@@ -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

83
ortools/sat/cp_model_presolve.cc
View File

@@ -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<int>& ignored_constraints) {
const CpModelProto& in_model, const std::vector<int>& ignored_constraints,
bool first_copy) {
const absl::flat_hash_set<int> 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<int> 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;

14
ortools/sat/cp_model_presolve.h
View File

@@ -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<int>& 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<int>& 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);