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

[CP-SAT] speedup presolve; fix platform non determinism fix @2056; add symmetry detection for model with scheduling constraints

Browse Source
This commit is contained in:
Laurent Perron
2022-01-08 14:44:59 +01:00
parent da153ce40d
commit a1b369d4c8
9 changed files with 205 additions and 47 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
ortools/sat/clause.cc
View File

@@ -1544,12 +1544,19 @@ bool BinaryImplicationGraph::TransformIntoMaxCliques(
implications_.size());
// We starts by processing larger constraints first.
std::sort(at_most_ones->begin(), at_most_ones->end(),
[](const std::vector<Literal> a, const std::vector<Literal> b) {
return a.size() > b.size();
});
for (std::vector<Literal>& clique : *at_most_ones) {
const int old_size = clique.size();
// But we want the output order to be stable.
std::vector<std::pair<int, int>> index_size_vector;
index_size_vector.reserve(at_most_ones->size());
for (int i = 0; i < at_most_ones->size(); ++i) {
index_size_vector.push_back({i, (*at_most_ones)[i].size()});
}
std::stable_sort(
index_size_vector.begin(), index_size_vector.end(),
[](const std::pair<int, int> a, const std::pair<int, int>& b) {
return a.second > b.second;
});
for (const auto [index, old_size] : index_size_vector) {
std::vector<Literal>& clique = (*at_most_ones)[index];
if (time_limit_->LimitReached()) break;
// Remap the clique to only use representative.

1
ortools/sat/clause.h
View File

@@ -583,6 +583,7 @@ class BinaryImplicationGraph : public SatPropagator {
// This function will transform each of the given constraint into a maximal
// one in the underlying implication graph. Constraints that are redundant
// after other have been expanded (i.e. included into) will be cleared.
// Note that the order of constraints will be conserved.
//
// Returns false if the model is detected to be UNSAT (this needs to call
// DetectEquivalences() if not already done).

25
ortools/sat/cp_model.proto
View File

@@ -110,18 +110,21 @@ message ElementConstraintProto {
repeated int32 vars = 3;
}
// This "special" constraint not only enforces (start + size == end) and (size
// >= 0) but can also be referred by other constraints using this "interval"
// concept.
// 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.
// - enforcement => size >= 0 // Only needed if size is not already >= 0.
//
// IMPORTANT: For now, we just support affine relation. We could easily
// create an intermediate variable to support full linear expression, but this
// isn't done currently.
message IntervalConstraintProto {
// IMPORTANT: For now, this constraint do not enforce any relations on the
// view, and a linear constraint must be added together with this to enforce
// enforcement => start + size == end. An enforcement => size >=0 might also
// be needed.
//
// IMPORTANT: For now, we just support affine relation. We could easily
// create an intermediate variable to support full linear expression, but this
// isn't done currently.
LinearExpressionProto start = 4;
LinearExpressionProto end = 5;
LinearExpressionProto size = 6;

5
ortools/sat/cp_model_checker.cc
View File

@@ -147,6 +147,11 @@ std::string ValidateArgumentReferencesInConstraint(const CpModelProto& model,
return absl::StrCat("Out of bound interval ", i, " in constraint #", c,
" : ", ProtobufShortDebugString(ct));
}
if (i >= c) {
return absl::StrCat("Interval ", i, " in constraint #", c,
" must appear before in the list of constraints :",
ProtobufShortDebugString(ct));
}
if (model.constraints(i).constraint_case() !=
ConstraintProto::ConstraintCase::kInterval) {
return absl::StrCat(

6
ortools/sat/cp_model_loader.cc
View File

@@ -830,7 +830,11 @@ void DetectOptionalVariables(const CpModelProto& model_proto, Model* m) {
mapping->Integer(var),
mapping->Literal(enforcement_intersection[var].front()));
}
VLOG(2) << "Auto-detected " << num_optionals << " optional variables.";
if (num_optionals > 0) {
SOLVER_LOG(m->GetOrCreate<SolverLogger>(), "Auto-detected ", num_optionals,
" optional variables.");
}
}
void AddFullEncodingFromSearchBranching(const CpModelProto& model_proto,

110
ortools/sat/cp_model_presolve.cc
View File

@@ -410,7 +410,8 @@ bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) {
// Deal with duplicate variable reference.
context_->tmp_literal_set.clear();
for (const int literal : *literals) {
if (context_->tmp_literal_set.contains(literal)) {
const auto [_, inserted] = context_->tmp_literal_set.insert(literal);
if (!inserted) {
if (!context_->SetLiteralToFalse(literal)) return false;
context_->UpdateRuleStats(absl::StrCat(name, "duplicate literals"));
}
@@ -440,7 +441,6 @@ bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) {
}
return RemoveConstraint(ct);
}
context_->tmp_literal_set.insert(literal);
}
// Remove fixed variables.
@@ -3796,6 +3796,7 @@ bool CpModelPresolver::PresolveNoOverlap(ConstraintProto* ct) {
}
}
bool move_constraint_last = false;
if (!constant_intervals.empty()) {
// Sort constant_intervals by start min.
std::sort(constant_intervals.begin(), constant_intervals.end(),
@@ -3847,6 +3848,7 @@ bool CpModelPresolver::PresolveNoOverlap(ConstraintProto* ct) {
new_interval->mutable_start()->set_offset(new_start);
new_interval->mutable_size()->set_offset(new_end - new_start);
new_interval->mutable_end()->set_offset(new_end);
move_constraint_last = true;
}
// Cleanup the original proto.
@@ -3880,6 +3882,16 @@ bool CpModelPresolver::PresolveNoOverlap(ConstraintProto* ct) {
return RemoveConstraint(ct);
}
// Unfortunately, because we want all intervals to appear before a constraint
// that uses them, we need to move the constraint last when we merged constant
// intervals.
if (move_constraint_last) {
changed = true;
*context_->working_model->add_constraints() = *ct;
context_->UpdateNewConstraintsVariableUsage();
return RemoveConstraint(ct);
}
return changed;
}
@@ -6043,10 +6055,8 @@ bool CpModelPresolver::ProcessSetPPC() {
if (c1 == c2) continue;
CHECK_LT(c1, c2);
if (compared_constraints.contains(std::pair<int, int>(c1, c2))) {
continue;
}
compared_constraints.insert({c1, c2});
const auto [_, inserted] = compared_constraints.insert({c1, c2});
if (!inserted) continue;
// Hard limit on number of comparisons to avoid spending too much time
// here.
@@ -7100,6 +7110,10 @@ void CpModelPresolver::PresolveToFixPoint() {
ModelCopy::ModelCopy(PresolveContext* context) : context_(context) {}
// TODO(user): Merge with the phase 1 of the presolve code.
//
// TODO(user): It seems easy to forget to update this if any new constraint
// 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 absl::flat_hash_set<int> ignored_constraints_set(
@@ -7111,10 +7125,8 @@ bool ModelCopy::ImportAndSimplifyConstraints(
if (ignored_constraints_set.contains(c)) continue;
const ConstraintProto& ct = in_model.constraints(c);
if (OneEnforcementLiteralIsFalse(ct) &&
ct.constraint_case() != ConstraintProto::kInterval) {
continue;
}
if (OneEnforcementLiteralIsFalse(ct)) continue;
switch (ct.constraint_case()) {
case ConstraintProto::CONSTRAINT_NOT_SET: {
break;
@@ -7143,27 +7155,23 @@ bool ModelCopy::ImportAndSimplifyConstraints(
if (!CopyInterval(ct, c)) return CreateUnsatModel();
break;
}
case ConstraintProto::kNoOverlap: {
CopyAndMapNoOverlap(ct);
break;
}
case ConstraintProto::kNoOverlap2D: {
CopyAndMapNoOverlap2D(ct);
break;
}
case ConstraintProto::kCumulative: {
CopyAndMapCumulative(ct);
break;
}
default: {
*context_->working_model->add_constraints() = ct;
}
}
}
// Re-map interval indices for new constraints.
// TODO(user): Support removing unperformed intervals.
for (int c = starting_constraint_index_;
c < context_->working_model->constraints_size(); ++c) {
ConstraintProto& ct_ref = *context_->working_model->mutable_constraints(c);
ApplyToAllIntervalIndices(
[this](int* ref) {
const auto& it = interval_mapping_.find(*ref);
if (it != interval_mapping_.end()) {
*ref = it->second;
}
},
&ct_ref);
}
return true;
}
@@ -7353,7 +7361,6 @@ bool ModelCopy::CopyExactlyOne(const ConstraintProto& ct) {
}
bool ModelCopy::CopyInterval(const ConstraintProto& ct, int c) {
// TODO(user): remove non performed intervals.
CHECK_EQ(starting_constraint_index_, 0)
<< "Adding new interval constraints to partially filled model is not "
"supported.";
@@ -7362,6 +7369,55 @@ bool ModelCopy::CopyInterval(const ConstraintProto& ct, int c) {
return true;
}
void ModelCopy::CopyAndMapNoOverlap(const ConstraintProto& ct) {
// Note that we don't copy names or enforcement_literal (not supported) here.
auto* new_ct =
context_->working_model->add_constraints()->mutable_no_overlap();
new_ct->mutable_intervals()->Reserve(ct.no_overlap().intervals().size());
for (const int index : ct.no_overlap().intervals()) {
const auto it = interval_mapping_.find(index);
if (it == interval_mapping_.end()) continue;
new_ct->add_intervals(it->second);
}
}
void ModelCopy::CopyAndMapNoOverlap2D(const ConstraintProto& ct) {
// Note that we don't copy names or enforcement_literal (not supported) here.
auto* new_ct =
context_->working_model->add_constraints()->mutable_no_overlap_2d();
new_ct->set_boxes_with_null_area_can_overlap(
ct.no_overlap_2d().boxes_with_null_area_can_overlap());
const int num_intervals = ct.no_overlap_2d().x_intervals().size();
new_ct->mutable_x_intervals()->Reserve(num_intervals);
new_ct->mutable_y_intervals()->Reserve(num_intervals);
for (int i = 0; i < num_intervals; ++i) {
const auto x_it = interval_mapping_.find(ct.no_overlap_2d().x_intervals(i));
if (x_it == interval_mapping_.end()) continue;
const auto y_it = interval_mapping_.find(ct.no_overlap_2d().y_intervals(i));
if (y_it == interval_mapping_.end()) continue;
new_ct->add_x_intervals(x_it->second);
new_ct->add_y_intervals(y_it->second);
}
}
void ModelCopy::CopyAndMapCumulative(const ConstraintProto& ct) {
// Note that we don't copy names or enforcement_literal (not supported) here.
auto* new_ct =
context_->working_model->add_constraints()->mutable_cumulative();
*new_ct->mutable_capacity() = ct.cumulative().capacity();
const int num_intervals = ct.cumulative().intervals().size();
new_ct->mutable_intervals()->Reserve(num_intervals);
new_ct->mutable_demands()->Reserve(num_intervals);
for (int i = 0; i < num_intervals; ++i) {
const auto it = interval_mapping_.find(ct.cumulative().intervals(i));
if (it == interval_mapping_.end()) continue;
new_ct->add_intervals(it->second);
*new_ct->add_demands() = ct.cumulative().demands(i);
}
}
bool ModelCopy::CreateUnsatModel() {
context_->working_model->mutable_constraints()->Clear();
context_->working_model->add_constraints()->mutable_bool_or();

7
ortools/sat/cp_model_presolve.h
View File

@@ -257,6 +257,13 @@ class ModelCopy {
bool CopyExactlyOne(const ConstraintProto& ct);
bool CopyInterval(const ConstraintProto& ct, int c);
// These function remove unperformed intervals. Note that they requires
// interval to appear before (validated) as they test unperformed by testing
// if interval_mapping_ is empty.
void CopyAndMapNoOverlap(const ConstraintProto& ct);
void CopyAndMapNoOverlap2D(const ConstraintProto& ct);
void CopyAndMapCumulative(const ConstraintProto& ct);
PresolveContext* context_;
int64_t skipped_non_zero_ = 0;

77
ortools/sat/cp_model_symmetries.cc
View File

@@ -215,8 +215,13 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
get_implication_node(NegatedRef(ref_a)));
};
// We need to keep track of this for scheduling constraints.
absl::flat_hash_map<int, int> interval_constraint_index_to_node;
// Add constraints to the graph.
for (const ConstraintProto& constraint : problem.constraints()) {
for (int constraint_index = 0; constraint_index < problem.constraints_size();
++constraint_index) {
const ConstraintProto& constraint = problem.constraints(constraint_index);
const int constraint_node = initial_equivalence_classes->size();
std::vector<int64_t> color = {CONSTRAINT_NODE,
constraint.constraint_case()};
@@ -299,6 +304,76 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
}
break;
}
case ConstraintProto::kInterval: {
// We create 3 constraint nodes (for start, size and end) including the
// offset. We connect these to their terms like for a linear constraint.
std::vector<int> nodes;
for (int indicator = 0; indicator <= 2; ++indicator) {
const LinearExpressionProto& expr =
indicator == 0 ? constraint.interval().start()
: indicator == 1 ? constraint.interval().size()
: constraint.interval().end();
std::vector<int64_t> local_color = color;
local_color.push_back(indicator);
local_color.push_back(expr.offset());
const int local_node = new_node(local_color);
nodes.push_back(local_node);
for (int i = 0; i < expr.vars().size(); ++i) {
const int ref = expr.vars(i);
const int var_node = PositiveRef(ref);
const int64_t coeff =
RefIsPositive(ref) ? expr.coeffs(i) : -expr.coeffs(i);
graph->AddArc(get_coefficient_node(var_node, coeff), local_node);
}
}
// We will only map enforcement literal to the start_node below because
// it has the same index as the constraint_node.
interval_constraint_index_to_node[constraint_index] = constraint_node;
CHECK_EQ(nodes[0], constraint_node);
// Make sure that if one node is mapped to another one, its other two
// components are the same.
graph->AddArc(nodes[0], nodes[1]);
graph->AddArc(nodes[1], nodes[2]);
graph->AddArc(nodes[2], nodes[0]); // TODO(user): not needed?
break;
}
case ConstraintProto::kNoOverlap: {
// Note(user): This require that intervals appear before they are used.
// We currently enforce this at validation, otherwise we need two passes
// here and in a bunch of other places.
CHECK_EQ(constraint_node, new_node(color));
for (const int interval : constraint.no_overlap().intervals()) {
graph->AddArc(interval_constraint_index_to_node.at(interval),
constraint_node);
}
break;
}
case ConstraintProto::kNoOverlap2D: {
// Note(user): This require that intervals appear before they are used.
// We currently enforce this at validation, otherwise we need two passes
// here and in a bunch of other places.
//
// TODO(user): With this graph encoding, we loose the symmetry that the
// dimension x can be swapped with the dimension y. I think it is
// possible to encode this by creating two extra nodes X and
// Y, each connected to all the x and all the y, but I have to think
// more about it.
CHECK_EQ(constraint_node, new_node(color));
const int size = constraint.no_overlap_2d().x_intervals().size();
for (int i = 0; i < size; ++i) {
const int x = constraint.no_overlap_2d().x_intervals(i);
const int y = constraint.no_overlap_2d().y_intervals(i);
graph->AddArc(interval_constraint_index_to_node.at(x),
constraint_node);
graph->AddArc(interval_constraint_index_to_node.at(x),
interval_constraint_index_to_node.at(y));
}
break;
}
default: {
// If the model contains any non-supported constraints, return an empty
// graph.

2
ortools/sat/linear_relaxation.cc
View File

@@ -1547,7 +1547,7 @@ LinearRelaxation ComputeLinearRelaxation(const CpModelProto& model_proto,
// Linearize the at most one constraints. Note that we transform them
// into maximum "at most one" first and we removes redundant ones.
m->GetOrCreate<BinaryImplicationGraph>()->TransformIntoMaxCliques(
&relaxation.at_most_ones);
&relaxation.at_most_ones, params.merge_at_most_one_work_limit());
for (const std::vector<Literal>& at_most_one : relaxation.at_most_ones) {
if (at_most_one.empty()) continue;