OR-Tools  8.1
scheduling_constraints.cc
Go to the documentation of this file.
1 // Copyright 2010-2018 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
15 
16 #include "ortools/sat/integer.h"
17 #include "ortools/sat/sat_base.h"
18 
19 namespace operations_research {
20 namespace sat {
21 
23  public:
24  explicit SelectedMinPropagator(Literal enforcement_literal,
25  AffineExpression target,
26  const std::vector<AffineExpression>& exprs,
27  const std::vector<Literal>& selectors,
28  Model* model)
29  : enforcement_literal_(enforcement_literal),
30  target_(target),
31  exprs_(exprs),
32  selectors_(selectors),
33  trail_(model->GetOrCreate<Trail>()),
34  integer_trail_(model->GetOrCreate<IntegerTrail>()),
35  precedences_(model->GetOrCreate<PrecedencesPropagator>()),
36  true_literal_(model->GetOrCreate<IntegerEncoder>()->GetTrueLiteral()) {}
37  bool Propagate() final;
38  int RegisterWith(GenericLiteralWatcher* watcher);
39 
40  private:
41  const Literal enforcement_literal_;
42  const AffineExpression target_;
43  const std::vector<AffineExpression> exprs_;
44  const std::vector<Literal> selectors_;
45  Trail* trail_;
46  IntegerTrail* integer_trail_;
47  PrecedencesPropagator* precedences_;
48  const Literal true_literal_;
49 
50  std::vector<Literal> literal_reason_;
51  std::vector<IntegerLiteral> integer_reason_;
52 
53  DISALLOW_COPY_AND_ASSIGN(SelectedMinPropagator);
54 };
55 
57  const VariablesAssignment& assignment = trail_->Assignment();
58 
59  // helpers.
60  const auto add_var_non_selection_to_reason = [&](int i) {
61  DCHECK(assignment.LiteralIsFalse(selectors_[i]));
62  literal_reason_.push_back(selectors_[i]);
63  };
64  const auto add_var_selection_to_reason = [&](int i) {
65  DCHECK(assignment.LiteralIsTrue(selectors_[i]));
66  literal_reason_.push_back(selectors_[i].Negated());
67  };
68 
69  // Push the given integer literal if lit is true. Note that if lit is still
70  // not assigned, we may still be able to deduce something.
71  // TODO(user,user): Move this to integer_trail, and remove from here and
72  // from scheduling helper.
73  const auto push_bound = [&](Literal enforcement_lit, IntegerLiteral i_lit) {
74  if (assignment.LiteralIsFalse(enforcement_lit)) return true;
75  if (integer_trail_->OptionalLiteralIndex(i_lit.var) !=
76  enforcement_lit.Index()) {
77  if (assignment.LiteralIsTrue(enforcement_lit)) {
78  // We can still push, but we do need the presence reason.
79  literal_reason_.push_back(Literal(enforcement_lit).Negated());
80  } else {
81  // In this case we cannot push lit.var, but we may force the enforcement
82  // literal to be false.
83  if (i_lit.bound > integer_trail_->UpperBound(i_lit.var)) {
84  integer_reason_.push_back(
85  IntegerLiteral::LowerOrEqual(i_lit.var, i_lit.bound - 1));
86  DCHECK(!assignment.LiteralIsFalse(enforcement_lit));
87  integer_trail_->EnqueueLiteral(Literal(enforcement_lit).Negated(),
88  literal_reason_, integer_reason_);
89  }
90  return true;
91  }
92  }
93 
94  if (!integer_trail_->Enqueue(i_lit, literal_reason_, integer_reason_)) {
95  return false;
96  }
97 
98  return true;
99  };
100 
101  // Propagation.
102  const int num_vars = exprs_.size();
103  const IntegerValue target_min = integer_trail_->LowerBound(target_);
104  const IntegerValue target_max = integer_trail_->UpperBound(target_);
105 
106  // Loop through the variables, and fills the quantities below.
107  // In our naming scheme, a variable is either ignored, selected, or possible.
108  IntegerValue min_of_mins(kMaxIntegerValue);
109  IntegerValue min_of_selected_maxes(kMaxIntegerValue);
110  IntegerValue max_of_possible_maxes(kMinIntegerValue);
111  int num_possible_vars = 0;
112  int num_selected_vars = 0;
113  int min_of_selected_maxes_index = -1;
114  int first_selected = -1;
115  for (int i = 0; i < num_vars; ++i) {
116  if (assignment.LiteralIsFalse(selectors_[i])) continue;
117 
118  const IntegerValue var_min = integer_trail_->LowerBound(exprs_[i]);
119  const IntegerValue var_max = integer_trail_->UpperBound(exprs_[i]);
120 
121  min_of_mins = std::min(min_of_mins, var_min);
122 
123  if (assignment.LiteralIsTrue(selectors_[i])) {
124  DCHECK(assignment.LiteralIsTrue(enforcement_literal_));
125  num_selected_vars++;
126  if (var_max < min_of_selected_maxes) {
127  min_of_selected_maxes = var_max;
128  min_of_selected_maxes_index = i;
129  }
130  if (first_selected == -1) {
131  first_selected = i;
132  }
133  } else {
134  DCHECK(!assignment.LiteralIsFalse(selectors_[i]));
135  num_possible_vars++;
136  max_of_possible_maxes = std::max(max_of_possible_maxes, var_max);
137  }
138  }
139 
140  if (min_of_mins > target_min) {
141  literal_reason_.clear();
142  integer_reason_.clear();
143  for (int i = 0; i < num_vars; ++i) {
144  if (assignment.LiteralIsFalse(selectors_[i])) {
145  add_var_non_selection_to_reason(i);
146  } else if (exprs_[i].var != kNoIntegerVariable) {
147  integer_reason_.push_back(exprs_[i].GreaterOrEqual(min_of_mins));
148  }
149  }
150  if (!push_bound(enforcement_literal_,
151  target_.GreaterOrEqual(min_of_mins))) {
152  return false;
153  }
154  }
155 
156  if (num_selected_vars > 0 && min_of_selected_maxes < target_max) {
157  DCHECK(assignment.LiteralIsTrue(enforcement_literal_));
158  DCHECK_NE(min_of_selected_maxes_index, -1);
159  DCHECK(assignment.LiteralIsTrue(selectors_[min_of_selected_maxes_index]));
160  literal_reason_.clear();
161  integer_reason_.clear();
162  add_var_selection_to_reason(min_of_selected_maxes_index);
163  if (exprs_[min_of_selected_maxes_index].var != kNoIntegerVariable) {
164  integer_reason_.push_back(
165  exprs_[min_of_selected_maxes_index].LowerOrEqual(
166  min_of_selected_maxes));
167  }
168  if (!integer_trail_->Enqueue(target_.LowerOrEqual(min_of_selected_maxes),
169  literal_reason_, integer_reason_)) {
170  return false;
171  }
172  }
173 
174  // Propagates in case every vars are still optional.
175  if (num_possible_vars > 0 && num_selected_vars == 0) {
176  if (target_max > max_of_possible_maxes) {
177  literal_reason_.clear();
178  integer_reason_.clear();
179 
180  for (int i = 0; i < num_vars; ++i) {
181  if (assignment.LiteralIsFalse(selectors_[i])) {
182  add_var_non_selection_to_reason(i);
183  } else if (exprs_[i].var != kNoIntegerVariable) {
184  integer_reason_.push_back(
185  exprs_[i].LowerOrEqual(max_of_possible_maxes));
186  }
187  }
188  if (!push_bound(enforcement_literal_,
189  target_.LowerOrEqual(max_of_possible_maxes))) {
190  return false;
191  }
192  }
193  }
194 
195  // All propagations and checks belows rely of the presence of the target.
196  if (!assignment.LiteralIsTrue(enforcement_literal_)) return true;
197 
198  DCHECK_GE(integer_trail_->LowerBound(target_), min_of_mins);
199 
200  // Note that the case num_possible == 1, num_selected_vars == 0 shouldn't
201  // happen because we assume that the enforcement <=> at_least_one_present
202  // clause has already been propagated.
203  if (num_possible_vars > 0) {
204  DCHECK_GT(num_possible_vars + num_selected_vars, 1);
205  return true;
206  }
207  if (num_selected_vars != 1) return true;
208 
209  DCHECK_NE(first_selected, -1);
210  DCHECK(assignment.LiteralIsTrue(selectors_[first_selected]));
211  const AffineExpression unique_selected_var = exprs_[first_selected];
212 
213  // Propagate bound from target to the unique selected var.
214  if (target_min > integer_trail_->LowerBound(unique_selected_var)) {
215  literal_reason_.clear();
216  integer_reason_.clear();
217  for (int i = 0; i < num_vars; ++i) {
218  if (i != first_selected) {
219  add_var_non_selection_to_reason(i);
220  } else {
221  add_var_selection_to_reason(i);
222  }
223  }
224  if (target_.var != kNoIntegerVariable) {
225  integer_reason_.push_back(target_.GreaterOrEqual(target_min));
226  }
227  if (!integer_trail_->Enqueue(unique_selected_var.GreaterOrEqual(target_min),
228  literal_reason_, integer_reason_)) {
229  return false;
230  }
231  }
232 
233  if (target_max < integer_trail_->UpperBound(unique_selected_var)) {
234  literal_reason_.clear();
235  integer_reason_.clear();
236  for (int i = 0; i < num_vars; ++i) {
237  if (i != first_selected) {
238  add_var_non_selection_to_reason(i);
239  } else {
240  add_var_selection_to_reason(i);
241  }
242  }
243  if (target_.var != kNoIntegerVariable) {
244  integer_reason_.push_back(target_.LowerOrEqual(target_max));
245  }
246  if (!integer_trail_->Enqueue(unique_selected_var.LowerOrEqual(target_max),
247  literal_reason_, integer_reason_)) {
248  return false;
249  }
250  }
251 
252  return true;
253 }
254 
256  const int id = watcher->Register(this);
257  for (int t = 0; t < exprs_.size(); ++t) {
258  watcher->WatchAffineExpression(exprs_[t], id);
259  watcher->WatchLiteral(selectors_[t], id);
260  }
261  watcher->WatchAffineExpression(target_, id);
262  watcher->WatchLiteral(enforcement_literal_, id);
263  return id;
264 }
265 
266 std::function<void(Model*)> EqualMinOfSelectedVariables(
267  Literal enforcement_literal, AffineExpression target,
268  const std::vector<AffineExpression>& exprs,
269  const std::vector<Literal>& selectors) {
270  CHECK_EQ(exprs.size(), selectors.size());
271  return [=](Model* model) {
272  // If both a variable is selected and the enforcement literal is true, then
273  // the var is always greater than the target.
274  for (int i = 0; i < exprs.size(); ++i) {
275  LinearConstraintBuilder builder(model, kMinIntegerValue, IntegerValue(0));
276  builder.AddTerm(target, IntegerValue(1));
277  builder.AddTerm(exprs[i], IntegerValue(-1));
278  LoadConditionalLinearConstraint({enforcement_literal, selectors[i]},
279  builder.Build(), model);
280  }
281 
282  // Add the dedicated propagator.
284  enforcement_literal, target, exprs, selectors, model);
285  constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
286  model->TakeOwnership(constraint);
287  };
288 }
289 
290 std::function<void(Model*)> EqualMaxOfSelectedVariables(
291  Literal enforcement_literal, AffineExpression target,
292  const std::vector<AffineExpression>& exprs,
293  const std::vector<Literal>& selectors) {
294  CHECK_EQ(exprs.size(), selectors.size());
295  return [=](Model* model) {
296  std::vector<AffineExpression> negations;
297  for (const AffineExpression expr : exprs) {
298  negations.push_back(expr.Negated());
299  }
301  enforcement_literal, target.Negated(), negations, selectors));
302  };
303 }
304 
305 std::function<void(Model*)> SpanOfIntervals(
306  IntervalVariable span, const std::vector<IntervalVariable>& intervals) {
307  return [=](Model* model) {
308  auto* sat_solver = model->GetOrCreate<SatSolver>();
309  auto* repository = model->GetOrCreate<IntervalsRepository>();
310 
311  // If the target is absent, then all tasks are absent.
312  if (repository->IsAbsent(span)) {
313  for (const IntervalVariable interval : intervals) {
314  if (repository->IsOptional(interval)) {
315  sat_solver->AddBinaryClause(
316  repository->PresenceLiteral(span).Negated(),
317  repository->PresenceLiteral(interval));
318  } else if (repository->IsPresent(interval)) {
319  sat_solver->NotifyThatModelIsUnsat();
320  return;
321  }
322  }
323  return;
324  }
325 
326  // The target is present iif at least one interval is present. This is a
327  // strict equivalence.
328  std::vector<Literal> presence_literals;
329  std::vector<AffineExpression> starts;
330  std::vector<AffineExpression> ends;
331  std::vector<Literal> clause;
332  bool at_least_one_interval_is_present = false;
333  const Literal true_literal =
334  model->GetOrCreate<IntegerEncoder>()->GetTrueLiteral();
335 
336  for (const IntervalVariable interval : intervals) {
337  if (repository->IsAbsent(interval)) continue;
338 
339  if (repository->IsOptional(interval)) {
340  const Literal task_lit = repository->PresenceLiteral(interval);
341  presence_literals.push_back(task_lit);
342  clause.push_back(task_lit);
343 
344  if (repository->IsOptional(span)) {
345  // task is present => target is present.
346  sat_solver->AddBinaryClause(task_lit.Negated(),
347  repository->PresenceLiteral(span));
348  }
349 
350  } else {
351  presence_literals.push_back(true_literal);
352  at_least_one_interval_is_present = true;
353  }
354  starts.push_back(repository->Start(interval));
355  ends.push_back(repository->End(interval));
356  }
357 
358  if (!at_least_one_interval_is_present) {
359  // enforcement_literal is true => one of the task is present.
360  if (repository->IsOptional(span)) {
361  clause.push_back(repository->PresenceLiteral(span).Negated());
362  }
363  sat_solver->AddProblemClause(clause);
364  }
365 
366  // Link target start and end to the starts and ends of the tasks.
367  const Literal enforcement_literal =
368  repository->IsOptional(span)
369  ? repository->PresenceLiteral(span)
370  : model->GetOrCreate<IntegerEncoder>()->GetTrueLiteral();
371  model->Add(EqualMinOfSelectedVariables(enforcement_literal,
372  repository->Start(span), starts,
373  presence_literals));
375  enforcement_literal, repository->End(span), ends, presence_literals));
376  };
377 }
378 
379 } // namespace sat
380 } // namespace operations_research
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::GenericLiteralWatcher::Register
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1910
min
int64 min
Definition: alldiff_cst.cc:138
operations_research::sat::AffineExpression
Definition: integer.h:205
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
max
int64 max
Definition: alldiff_cst.cc:139
operations_research::sat::LinearConstraintBuilder::Build
LinearConstraint Build()
Definition: linear_constraint.cc:113
operations_research::sat::EqualMinOfSelectedVariables
std::function< void(Model *)> EqualMinOfSelectedVariables(Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors)
Definition: scheduling_constraints.cc:266
operations_research::sat::PropagatorInterface
Definition: integer.h:1043
operations_research::sat::EqualMaxOfSelectedVariables
std::function< void(Model *)> EqualMaxOfSelectedVariables(Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors)
Definition: scheduling_constraints.cc:290
operations_research::sat::SatSolver
Definition: sat_solver.h:58
DCHECK_GT
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::IntegerTrail::EnqueueLiteral
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1058
operations_research::sat::VariablesAssignment::LiteralIsTrue
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
operations_research::sat::IntegerTrail::OptionalLiteralIndex
LiteralIndex OptionalLiteralIndex(IntegerVariable i) const
Definition: integer.h:627
operations_research::sat::SelectedMinPropagator::Propagate
bool Propagate() final
Definition: scheduling_constraints.cc:56
operations_research::sat::Literal::Negated
Literal Negated() const
Definition: sat_base.h:91
sat_base.h
operations_research::sat::LinearConstraintBuilder::AddTerm
void AddTerm(IntegerVariable var, IntegerValue coeff)
Definition: linear_constraint.cc:22
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
DCHECK_NE
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
operations_research::sat::LinearConstraintBuilder
Definition: linear_constraint.h:87
operations_research::sat::GenericLiteralWatcher::WatchAffineExpression
void WatchAffineExpression(AffineExpression e, int id)
Definition: integer.h:1141
operations_research::sat::IntegerTrail::UpperBound
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1287
operations_research::sat::IntegerTrail::Enqueue
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:989
operations_research::sat::PrecedencesPropagator
Definition: precedences.h:51
operations_research::sat::kMaxIntegerValue
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
operations_research::sat::Trail::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::Literal::Index
LiteralIndex Index() const
Definition: sat_base.h:84
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::AffineExpression::GreaterOrEqual
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
Definition: integer.h:1268
operations_research::sat::IntegerLiteral
Definition: integer.h:153
operations_research::sat::LowerOrEqual
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1492
DCHECK
#define DCHECK(condition)
Definition: base/logging.h:884
operations_research::sat::AffineExpression::LowerOrEqual
IntegerLiteral LowerOrEqual(IntegerValue bound) const
Definition: integer.h:1277
operations_research::sat::IntegerLiteral::LowerOrEqual
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1253
DCHECK_GE
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::sat::GenericLiteralWatcher::WatchLiteral
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1348
operations_research::sat::kMinIntegerValue
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
operations_research::sat::GreaterOrEqual
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
Definition: integer.h:1478
operations_research::sat::SelectedMinPropagator
Definition: scheduling_constraints.cc:22
operations_research::sat::UpperBound
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1456
operations_research::sat::IntervalsRepository
Definition: intervals.h:45
operations_research::sat::SpanOfIntervals
std::function< void(Model *)> SpanOfIntervals(IntervalVariable span, const std::vector< IntervalVariable > &intervals)
Definition: scheduling_constraints.cc:305
interval
IntervalVar * interval
Definition: resource.cc:98
operations_research::sat::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::sat::LoadConditionalLinearConstraint
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
Definition: integer_expr.h:572
operations_research::sat::VariablesAssignment
Definition: sat_base.h:122
operations_research::sat::IntegerEncoder
Definition: integer.h:276
operations_research::sat::SelectedMinPropagator::SelectedMinPropagator
SelectedMinPropagator(Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors, Model *model)
Definition: scheduling_constraints.cc:24
integer.h
operations_research::sat::VariablesAssignment::LiteralIsFalse
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
operations_research::sat::Trail
Definition: sat_base.h:233
operations_research::sat::AffineExpression::Negated
AffineExpression Negated() const
Definition: integer.h:224
operations_research::sat::SelectedMinPropagator::RegisterWith
int RegisterWith(GenericLiteralWatcher *watcher)
Definition: scheduling_constraints.cc:255
scheduling_constraints.h