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

[CP-SAT] better logging of infeasible constraint during presolve; improved scheduling search

Browse Source
This commit is contained in:
Laurent Perron
2023-10-27 13:47:04 +02:00
parent 5b50f67ed0
commit bcf402180b
11 changed files with 302 additions and 38 deletions
Download Patch File Download Diff File Expand all files Collapse all files

49
ortools/sat/cp_model_presolve.cc
View File

@@ -40,6 +40,7 @@
#include "absl/status/statusor.h"
#include "absl/strings/str_cat.h"
#include "absl/types/span.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/logging.h"
#include "ortools/base/mathutil.h"
#include "ortools/base/stl_util.h"
@@ -10676,34 +10677,36 @@ bool ModelCopy::ImportAndSimplifyConstraints(
break;
case ConstraintProto::kBoolOr:
if (first_copy) {
if (!CopyBoolOrWithDupSupport(ct)) return CreateUnsatModel();
if (!CopyBoolOrWithDupSupport(ct)) return CreateUnsatModel(c, ct);
} else {
if (!CopyBoolOr(ct)) return CreateUnsatModel();
if (!CopyBoolOr(ct)) return CreateUnsatModel(c, ct);
}
break;
case ConstraintProto::kBoolAnd:
if (temp_enforcement_literals_.empty()) {
for (const int lit : ct.bool_and().literals()) {
context_->UpdateRuleStats("bool_and: non-reified.");
if (!context_->SetLiteralToTrue(lit)) return CreateUnsatModel();
if (!context_->SetLiteralToTrue(lit)) {
return CreateUnsatModel(c, ct);
}
}
} else if (first_copy) {
if (!CopyBoolAndWithDupSupport(ct)) return CreateUnsatModel();
if (!CopyBoolAndWithDupSupport(ct)) return CreateUnsatModel(c, ct);
} else {
if (!CopyBoolAnd(ct)) return CreateUnsatModel();
if (!CopyBoolAnd(ct)) return CreateUnsatModel(c, ct);
}
break;
case ConstraintProto::kLinear:
if (!CopyLinear(ct)) return CreateUnsatModel();
if (!CopyLinear(ct)) return CreateUnsatModel(c, ct);
break;
case ConstraintProto::kAtMostOne:
if (!CopyAtMostOne(ct)) return CreateUnsatModel();
if (!CopyAtMostOne(ct)) return CreateUnsatModel(c, ct);
break;
case ConstraintProto::kExactlyOne:
if (!CopyExactlyOne(ct)) return CreateUnsatModel();
if (!CopyExactlyOne(ct)) return CreateUnsatModel(c, ct);
break;
case ConstraintProto::kInterval:
if (!CopyInterval(ct, c, ignore_names)) return CreateUnsatModel();
if (!CopyInterval(ct, c, ignore_names)) return CreateUnsatModel(c, ct);
break;
case ConstraintProto::kNoOverlap:
if (first_copy) {
@@ -11128,10 +11131,31 @@ void ModelCopy::CopyAndMapCumulative(const ConstraintProto& ct) {
}
}
bool ModelCopy::CreateUnsatModel() {
bool ModelCopy::CreateUnsatModel(int c, const ConstraintProto& ct) {
context_->working_model->mutable_constraints()->Clear();
context_->working_model->add_constraints()->mutable_bool_or();
return false;
// If the model was already marked as unsat, we keep the old message and just
// return. TODO(user): Append messages instead?
if (context_->ModelIsUnsat()) return false;
std::string proto_string;
#if !defined(__PORTABLE_PLATFORM__)
google::protobuf::TextFormat::Printer printer;
SetupTextFormatPrinter(&printer);
printer.PrintToString(ct, &proto_string);
#endif // !defined(__PORTABLE_PLATFORM__)
std::string message = absl::StrCat(
"proven during initial copy of constraint #", c, ":\n", proto_string);
std::vector<int> vars = UsedVariables(ct);
if (vars.size() < 10) {
absl::StrAppend(&message, "With current variable domains:\n");
for (const int var : vars) {
absl::StrAppend(&message, "var:", var,
" domain:", context_->DomainOf(var).ToString(), "\n");
}
}
return context_->NotifyThatModelIsUnsat(message);
}
bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model,
@@ -11143,8 +11167,7 @@ bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model,
context);
return true;
}
if (context->ModelIsUnsat()) return false;
return context->NotifyThatModelIsUnsat();
return !context->ModelIsUnsat();
}
void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(

3
ortools/sat/cp_model_presolve.h
View File

@@ -368,7 +368,8 @@ class ModelCopy {
private:
// Overwrites the out_model to be unsat. Returns false.
bool CreateUnsatModel();
// The arguments are used to log which constraint caused unsat.
bool CreateUnsatModel(int c, const ConstraintProto& ct);
// Returns false if the constraint is never enforced and can be skipped.
bool PrepareEnforcementCopy(const ConstraintProto& ct);

20
ortools/sat/cp_model_search.cc
View File

@@ -342,17 +342,16 @@ std::function<BooleanOrIntegerLiteral()> ConstructUserSearchStrategy(
std::function<BooleanOrIntegerLiteral()> ConstructHeuristicSearchStrategy(
const CpModelProto& cp_model_proto, Model* model) {
if (ModelHasSchedulingConstraints(cp_model_proto)) {
if (model->GetOrCreate<SatParameters>()
->use_dynamic_precedence_in_disjunctive()) {
// We combine the two, because the precedence only work for disjunctive,
// and not if we only have cumulative constraints.
return SequentialSearch({SchedulingPrecedenceSearchHeuristic(model),
SchedulingSearchHeuristic(model)});
} else {
// Precedence based model seems better, but the other one lead to faster
// solution.
return SchedulingSearchHeuristic(model);
std::vector<std::function<BooleanOrIntegerLiteral()>> heuristics;
const auto& params = *model->GetOrCreate<SatParameters>();
if (params.use_dynamic_precedence_in_disjunctive()) {
heuristics.push_back(DisjunctivePrecedenceSearchHeuristic(model));
}
if (params.use_dynamic_precedence_in_cumulative()) {
heuristics.push_back(CumulativePrecedenceSearchHeuristic(model));
}
heuristics.push_back(SchedulingSearchHeuristic(model));
return SequentialSearch(std::move(heuristics));
}
return PseudoCost(model);
}
@@ -629,6 +628,7 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
new_params.set_search_branching(SatParameters::FIXED_SEARCH);
new_params.set_use_dynamic_precedence_in_disjunctive(false);
new_params.set_use_dynamic_precedence_in_cumulative(false);
strategies["fixed"] = new_params;
}

4
ortools/sat/cumulative.cc
View File

@@ -151,8 +151,8 @@ std::function<void(Model*)> Cumulative(
helper = intervals->GetOrCreateHelper(vars);
}
SchedulingDemandHelper* demands_helper =
model->GetOrCreate<IntervalsRepository>()->GetOrCreateDemandHelper(
helper, demands);
intervals->GetOrCreateDemandHelper(helper, demands);
intervals->RegisterCumulative({capacity, helper, demands_helper});
// For each variables that is after a subset of task ends (i.e. like a
// makespan objective), we detect it and add a special constraint to

177
ortools/sat/integer_search.cc
View File

@@ -605,7 +605,7 @@ bool PrecedenceIsBetter(SchedulingConstraintHelper* helper, int a,
// - For each disjunctive, consider the intervals by start time, consider
// adding the first precedence between overlapping interval.
// - Take the smallest start time amongst all disjunctive.
std::function<BooleanOrIntegerLiteral()> SchedulingPrecedenceSearchHeuristic(
std::function<BooleanOrIntegerLiteral()> DisjunctivePrecedenceSearchHeuristic(
Model* model) {
auto* repo = model->GetOrCreate<IntervalsRepository>();
return [repo]() {
@@ -652,12 +652,185 @@ std::function<BooleanOrIntegerLiteral()> SchedulingPrecedenceSearchHeuristic(
}
}
if (best_helper != nullptr) {
VLOG(2) << "New disjunctive precedence: "
<< best_helper->TaskDebugString(best_before) << " "
<< best_helper->TaskDebugString(best_after);
const IntervalVariable a = best_helper->IntervalVariables()[best_before];
const IntervalVariable b = best_helper->IntervalVariables()[best_after];
repo->CreateDisjunctivePrecedenceLiteral(a, b);
return BooleanOrIntegerLiteral(repo->GetPrecedenceLiteral(a, b));
}
return BooleanOrIntegerLiteral();
};
}
// The algo goes as follow:
// - Build a profile of all the tasks packed to the right as long as that is
// feasible.
// - If we can't grow the profile, we have identified a set of tasks that all
// overlap if they are packed on the right, and whose sum of demand exceed
// the capacity.
// - Look for two tasks in that set that can be made non-overlapping, and take
// a "precedence" decision between them.
std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
Model* model) {
auto* repo = model->GetOrCreate<IntervalsRepository>();
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
auto* trail = model->GetOrCreate<Trail>();
return [repo, integer_trail, trail]() {
SchedulingConstraintHelper* best_helper = nullptr;
int best_before = 0;
int best_after = 0;
for (const auto h : repo->AllCumulativeHelpers()) {
auto* helper = h.task_helper;
if (!helper->SynchronizeAndSetTimeDirection(true)) {
return BooleanOrIntegerLiteral();
}
const int num_tasks = helper->NumTasks();
std::vector<IntegerValue> added_demand(num_tasks, 0);
// We use a similar algo as in BuildProfile() in timetable.cc
const auto& by_smin = helper->TaskByIncreasingStartMin();
const auto& by_emin = helper->TaskByIncreasingEndMin();
const IntegerValue capacity_max = integer_trail->UpperBound(h.capacity);
// Start and height of the currently built profile rectangle.
IntegerValue current_height = 0;
int first_skipped_task = -1;
int next_end = 0;
int next_start = 0;
int num_added = 0;
bool found = false;
while (!found && next_end < num_tasks) {
IntegerValue time = by_emin[next_end].time;
if (next_start < num_tasks) {
time = std::min(time, by_smin[next_start].time);
}
// Remove added task ending there.
// Set their demand to zero.
while (next_end < num_tasks && by_emin[next_end].time == time) {
const int t = by_emin[next_end].task_index;
if (added_demand[t] > 0) {
current_height -= added_demand[t];
added_demand[t] = 0;
} else {
// Corner case if task is of duration zero.
added_demand[t] = -1;
}
++next_end;
}
// Add new task starting here.
// If the task cannot be added we have a candidate for precedence.
// TODO(user): tie-break tasks not fitting in the profile smartly.
while (next_start < num_tasks && by_smin[next_start].time == time) {
const int t = by_smin[next_start].task_index;
if (added_demand[t] == -1) continue; // Corner case.
const IntegerValue demand_min = h.demand_helper->DemandMin(t);
if (current_height + demand_min <= capacity_max) {
++num_added;
added_demand[t] = demand_min;
current_height += demand_min;
} else if (first_skipped_task == -1) {
// We should have everyting needed here to add a new precedence.
first_skipped_task = t;
found = true;
break;
}
++next_start;
}
}
// If packing everything to the left is feasible, continue.
if (first_skipped_task == -1) {
CHECK_EQ(num_added, num_tasks);
continue;
}
// We will use a bunch of heuristic to add a new precedence. All the task
// in open_tasks cannot share a time point since they exceed the capacity.
// Moreover if we pack all to the left, they have an intersecting point.
// So we should be able to make two of them disjoint
std::vector<int> open_tasks;
for (int t = 0; t < num_tasks; ++t) {
if (added_demand[t] <= 0) continue;
open_tasks.push_back(t);
}
open_tasks.push_back(first_skipped_task);
// TODO(user): Add heuristic ordering for creating interesting precedence
// first.
bool found_precedence_to_add = false;
std::vector<Literal> conflict;
for (const int s : open_tasks) {
for (const int t : open_tasks) {
if (s == t) continue;
// Can we add s <= t ?
// All the considered tasks are intersecting if on the left.
CHECK_LT(helper->StartMin(s), helper->EndMin(t));
CHECK_LT(helper->StartMin(t), helper->EndMin(s));
// Make sure s could be before t.
if (helper->EndMin(s) > helper->StartMax(t)) continue;
best_before = s;
best_after = t;
// If the literal already exist (and is likely false), skip.
// Note that it being false only implies start_t < end_s.
const IntervalVariable a = helper->IntervalVariables()[best_before];
const IntervalVariable b = helper->IntervalVariables()[best_after];
if (!repo->CreatePrecedenceLiteral(a, b)) {
// Since s can be before t, this should only fail if the literal
// exist. It shouldn't be able to be true here otherwise we
// will have s and t disjoint.
const LiteralIndex existing = repo->GetPrecedenceLiteral(a, b);
CHECK_NE(existing, kNoLiteralIndex);
CHECK(!trail->Assignment().LiteralIsTrue(Literal(existing)))
<< helper->TaskDebugString(s) << " ( <= ?) "
<< helper->TaskDebugString(t);
// This should only be true in normal usage after SAT search has
// fixed all literal, but if it is not, we can just return this
// decision.
if (trail->Assignment().LiteralIsFalse(Literal(existing))) {
conflict.push_back(Literal(existing));
continue;
}
}
best_helper = helper;
found_precedence_to_add = true;
break;
}
if (found_precedence_to_add) break;
}
if (found_precedence_to_add) break;
// If no precedence can be created, and all precedence are assigned to
// false we have a conflict since all these interval must intersect but
// cannot fit in the capacity!
//
// TODO(user): We need to add the reason for demand_min and capacity_max.
// TODO(user): unfortunately we can't report it from here.
if (VLOG_IS_ON(2)) {
LOG(INFO) << "Conflict between precedences !";
for (const int t : open_tasks) LOG(INFO) << helper->TaskDebugString(t);
}
}
// TODO(user): add heuristic criteria, right now we stop at first
// one. See above.
if (best_helper != nullptr) {
VLOG(2) << "New precedence: " << best_helper->TaskDebugString(best_before)
<< " " << best_helper->TaskDebugString(best_after);
const IntervalVariable a = best_helper->IntervalVariables()[best_before];
const IntervalVariable b = best_helper->IntervalVariables()[best_after];
repo->CreateDisjunctivePrecedenceLiteral(a, b);
repo->CreatePrecedenceLiteral(a, b);
return BooleanOrIntegerLiteral(repo->GetPrecedenceLiteral(a, b));
}

7
ortools/sat/integer_search.h
View File

@@ -229,7 +229,12 @@ std::function<BooleanOrIntegerLiteral()> SchedulingSearchHeuristic(
// Compared to SchedulingSearchHeuristic() this one take decision on precedences
// between tasks. Lazily creating a precedence Boolean for the task in
// disjunction.
std::function<BooleanOrIntegerLiteral()> SchedulingPrecedenceSearchHeuristic(
//
// Note that this one is meant to be used when all Boolean has been fixed, so
// more as a "completion" heuristic rather than a fixed search one.
std::function<BooleanOrIntegerLiteral()> DisjunctivePrecedenceSearchHeuristic(
Model* model);
std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
Model* model);
// Returns true if the number of variables in the linearized part represent

35
ortools/sat/intervals.cc
View File

@@ -126,6 +126,10 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral(
disjunctive_precedences_.insert({{a, b}, a_before_b});
disjunctive_precedences_.insert({{b, a}, a_before_b.Negated()});
// Also insert it in precedences.
precedences_.insert({{a, b}, a_before_b});
precedences_.insert({{b, a}, a_before_b.Negated()});
enforcement_literals.push_back(a_before_b);
AddConditionalAffinePrecedence(enforcement_literals, end_a, start_b, model_);
enforcement_literals.pop_back();
@@ -141,10 +145,37 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral(
}
}
bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
IntervalVariable b) {
if (precedences_.find({a, b}) != disjunctive_precedences_.end()) return false;
// We want l => x <= y and not(l) => x > y <=> y + 1 <= x
// Do not create l if the relation is always true or false.
const AffineExpression x = End(a);
const AffineExpression y = Start(b);
if (integer_trail_->UpperBound(x) <= integer_trail_->LowerBound(y)) {
return false;
}
if (integer_trail_->LowerBound(x) > integer_trail_->UpperBound(y)) {
return false;
}
// Create a new literal.
const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
const Literal x_before_y = Literal(boolean_var, true);
precedences_.insert({{a, b}, x_before_y});
AffineExpression y_plus_one = y;
y_plus_one.constant += 1;
AddConditionalAffinePrecedence({x_before_y}, x, y, model_);
AddConditionalAffinePrecedence({x_before_y.Negated()}, y_plus_one, x, model_);
return true;
}
LiteralIndex IntervalsRepository::GetPrecedenceLiteral(
IntervalVariable a, IntervalVariable b) const {
const auto it = disjunctive_precedences_.find({a, b});
if (it != disjunctive_precedences_.end()) return it->second.Index();
const auto it = precedences_.find({a, b});
if (it != precedences_.end()) return it->second.Index();
return kNoLiteralIndex;
}

32
ortools/sat/intervals.h
View File

@@ -182,8 +182,15 @@ class IntervalsRepository {
void CreateDisjunctivePrecedenceLiteral(IntervalVariable a,
IntervalVariable b);
// Returns the precedence literal from GetOrCreateDisjunctivePrecedence() if
// it exists or kNoLiteralIndex otherwise.
// Creates a literal l <=> start_b >= end_a.
// Returns true if such literal is "non-trivial" and was created.
// Note that this ignore the optionality of a or b, it just creates a literal
// comparing the two affine expression.
bool CreatePrecedenceLiteral(IntervalVariable a, IntervalVariable b);
// Returns a literal l <=> start_b >= end_a if it exist or kNoLiteralIndex
// otherwise. This could be the one created by
// CreateDisjunctivePrecedenceLiteral() or CreatePrecedenceLiteral().
LiteralIndex GetPrecedenceLiteral(IntervalVariable a,
IntervalVariable b) const;
@@ -192,6 +199,20 @@ class IntervalsRepository {
return disjunctive_helpers_;
}
// We register cumulative at load time so that our search heuristic can loop
// over all cumulative constraints easily.
struct CumulativeHelper {
AffineExpression capacity;
SchedulingConstraintHelper* task_helper;
SchedulingDemandHelper* demand_helper;
};
void RegisterCumulative(CumulativeHelper helper) {
cumulative_helpers_.push_back(helper);
}
const std::vector<CumulativeHelper>& AllCumulativeHelpers() const {
return cumulative_helpers_;
}
private:
// External classes needed.
Model* model_;
@@ -219,12 +240,15 @@ class IntervalsRepository {
SchedulingDemandHelper*>
demand_helper_repository_;
// Disjunctive precedences.
// Disjunctive and normal precedences.
absl::flat_hash_map<std::pair<IntervalVariable, IntervalVariable>, Literal>
disjunctive_precedences_;
absl::flat_hash_map<std::pair<IntervalVariable, IntervalVariable>, Literal>
precedences_;
// Disjunctive helpers_.
// Disjunctive/Cumulative helpers_.
std::vector<SchedulingConstraintHelper*> disjunctive_helpers_;
std::vector<CumulativeHelper> cumulative_helpers_;
};
// An helper struct to sort task by time. This is used by the

3
ortools/sat/linear_programming_constraint.cc
View File

@@ -30,6 +30,7 @@
#include "absl/log/check.h"
#include "absl/numeric/int128.h"
#include "absl/strings/str_cat.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "ortools/algorithms/binary_search.h"
#include "ortools/base/logging.h"
@@ -990,7 +991,7 @@ bool LinearProgrammingConstraint::PreprocessCut(IntegerVariable first_slack,
}
bool LinearProgrammingConstraint::AddCutFromConstraints(
const std::string& name,
absl::string_view name,
const std::vector<std::pair<RowIndex, IntegerValue>>& integer_multipliers) {
// This is initialized to a valid linear constraint (by taking linear
// combination of the LP rows) and will be transformed into a cut if

3
ortools/sat/linear_programming_constraint.h
View File

@@ -24,6 +24,7 @@
#include "absl/container/flat_hash_map.h"
#include "absl/numeric/int128.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "ortools/base/strong_vector.h"
#include "ortools/glop/parameters.pb.h"
@@ -301,7 +302,7 @@ class LinearProgrammingConstraint : public PropagatorInterface,
//
// Return true if a new cut was added to the cut manager.
bool AddCutFromConstraints(
const std::string& name,
absl::string_view name,
const std::vector<std::pair<glop::RowIndex, IntegerValue>>&
integer_multipliers);

7
ortools/sat/sat_parameters.proto
View File

@@ -23,7 +23,7 @@ option csharp_namespace = "Google.OrTools.Sat";
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 268
// NEXT TAG: 269
message SatParameters {
// In some context, like in a portfolio of search, it makes sense to name a
// given parameters set for logging purpose.
@@ -746,7 +746,12 @@ message SatParameters {
// Whether we try to branch on decision "interval A before interval B" rather
// than on intervals bounds. This usually works better, but slow down a bit
// the time to find first solutions.
//
// Note that for cumulative, this currently seems worse.
// These parameters are still EXPERIMENTAL, the result should be correct, but
// it some corner cases, they can cause some failing CHECK in the solver.
optional bool use_dynamic_precedence_in_disjunctive = 263 [default = false];
optional bool use_dynamic_precedence_in_cumulative = 268 [default = false];
// When this is true, the cumulative constraint is reinforced with overload
// checking, i.e., an additional level of reasoning based on energy. This