OR-Tools  8.1
cp_constraints.h
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 
14 #ifndef OR_TOOLS_SAT_CP_CONSTRAINTS_H_
15 #define OR_TOOLS_SAT_CP_CONSTRAINTS_H_
16 
17 #include <functional>
18 #include <memory>
19 #include <vector>
20 
21 #include "ortools/base/int_type.h"
23 #include "ortools/base/logging.h"
24 #include "ortools/base/macros.h"
25 #include "ortools/sat/integer.h"
26 #include "ortools/sat/model.h"
27 #include "ortools/sat/sat_base.h"
28 #include "ortools/util/rev.h"
29 
30 namespace operations_research {
31 namespace sat {
32 
33 // Propagate the fact that a XOR of literals is equal to the given value.
34 // The complexity is in O(n).
35 //
36 // TODO(user): By using a two watcher mechanism, we can propagate this a lot
37 // faster.
39  public:
40  BooleanXorPropagator(const std::vector<Literal>& literals, bool value,
41  Trail* trail, IntegerTrail* integer_trail)
42  : literals_(literals),
43  value_(value),
44  trail_(trail),
45  integer_trail_(integer_trail) {}
46 
47  bool Propagate() final;
48  void RegisterWith(GenericLiteralWatcher* watcher);
49 
50  private:
51  const std::vector<Literal> literals_;
52  const bool value_;
53  std::vector<Literal> literal_reason_;
54  Trail* trail_;
55  IntegerTrail* integer_trail_;
56 
57  DISALLOW_COPY_AND_ASSIGN(BooleanXorPropagator);
58 };
59 
60 // If we have:
61 // - selectors[i] => (target_var >= vars[i] + offset[i])
62 // - and we known that at least one selectors[i] must be true
63 // then we can propagate the fact that if no selectors is chosen yet, the lower
64 // bound of target_var is greater than the min of the still possible
65 // alternatives.
66 //
67 // This constraint take care of this case when no selectors[i] is chosen yet.
68 //
69 // This constraint support duplicate selectors.
71  public:
73  IntegerVariable target_var, const absl::Span<const IntegerVariable> vars,
74  const absl::Span<const IntegerValue> offsets,
75  const absl::Span<const Literal> selectors,
76  const absl::Span<const Literal> enforcements, Model* model);
77 
78  bool Propagate() final;
79  void RegisterWith(GenericLiteralWatcher* watcher);
80 
81  private:
82  const IntegerVariable target_var_;
83  const std::vector<IntegerVariable> vars_;
84  const std::vector<IntegerValue> offsets_;
85  const std::vector<Literal> selectors_;
86  const std::vector<Literal> enforcements_;
87 
88  Trail* trail_;
89  IntegerTrail* integer_trail_;
90 
91  std::vector<Literal> literal_reason_;
92  std::vector<IntegerLiteral> integer_reason_;
93 
94  DISALLOW_COPY_AND_ASSIGN(GreaterThanAtLeastOneOfPropagator);
95 };
96 
97 // ============================================================================
98 // Model based functions.
99 // ============================================================================
100 
101 inline std::vector<IntegerValue> ToIntegerValueVector(
102  const std::vector<int64>& input) {
103  std::vector<IntegerValue> result(input.size());
104  for (int i = 0; i < input.size(); ++i) {
105  result[i] = IntegerValue(input[i]);
106  }
107  return result;
108 }
109 
110 // Enforces the XOR of a set of literals to be equal to the given value.
111 inline std::function<void(Model*)> LiteralXorIs(
112  const std::vector<Literal>& literals, bool value) {
113  return [=](Model* model) {
114  Trail* trail = model->GetOrCreate<Trail>();
115  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
116  BooleanXorPropagator* constraint =
117  new BooleanXorPropagator(literals, value, trail, integer_trail);
118  constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
119  model->TakeOwnership(constraint);
120  };
121 }
122 
123 inline std::function<void(Model*)> GreaterThanAtLeastOneOf(
124  IntegerVariable target_var, const absl::Span<const IntegerVariable> vars,
125  const absl::Span<const IntegerValue> offsets,
126  const absl::Span<const Literal> selectors) {
127  return [=](Model* model) {
129  new GreaterThanAtLeastOneOfPropagator(target_var, vars, offsets,
130  selectors, {}, model);
131  constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
132  model->TakeOwnership(constraint);
133  };
134 }
135 
136 inline std::function<void(Model*)> GreaterThanAtLeastOneOf(
137  IntegerVariable target_var, const absl::Span<const IntegerVariable> vars,
138  const absl::Span<const IntegerValue> offsets,
139  const absl::Span<const Literal> selectors,
140  const absl::Span<const Literal> enforcements) {
141  return [=](Model* model) {
143  new GreaterThanAtLeastOneOfPropagator(target_var, vars, offsets,
144  selectors, enforcements, model);
145  constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
146  model->TakeOwnership(constraint);
147  };
148 }
149 
150 // The target variable is equal to exactly one of the candidate variable. The
151 // equality is controlled by the given "selector" literals.
152 //
153 // Note(user): This only propagate from the min/max of still possible candidates
154 // to the min/max of the target variable. The full constraint also requires
155 // to deal with the case when one of the literal is true.
156 //
157 // Note(user): If there is just one or two candidates, this doesn't add
158 // anything.
159 inline std::function<void(Model*)> PartialIsOneOfVar(
160  IntegerVariable target_var, const std::vector<IntegerVariable>& vars,
161  const std::vector<Literal>& selectors) {
162  CHECK_EQ(vars.size(), selectors.size());
163  return [=](Model* model) {
164  const std::vector<IntegerValue> offsets(vars.size(), IntegerValue(0));
165  if (vars.size() > 2) {
166  // Propagate the min.
167  model->Add(GreaterThanAtLeastOneOf(target_var, vars, offsets, selectors));
168  }
169  if (vars.size() > 2) {
170  // Propagate the max.
171  model->Add(GreaterThanAtLeastOneOf(NegationOf(target_var),
172  NegationOf(vars), offsets, selectors));
173  }
174  };
175 }
176 
177 } // namespace sat
178 } // namespace operations_research
179 
180 #endif // OR_TOOLS_SAT_CP_CONSTRAINTS_H_
operations_research::sat::GreaterThanAtLeastOneOfPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: cp_constraints.cc:137
operations_research::sat::GreaterThanAtLeastOneOfPropagator
Definition: cp_constraints.h:70
integral_types.h
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::LiteralXorIs
std::function< void(Model *)> LiteralXorIs(const std::vector< Literal > &literals, bool value)
Definition: cp_constraints.h:111
logging.h
operations_research::sat::PropagatorInterface
Definition: integer.h:1043
value
int64 value
Definition: demon_profiler.cc:43
model.h
operations_research::sat::BooleanXorPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: cp_constraints.cc:71
macros.h
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::NegationOf
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
sat_base.h
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
int_type.h
operations_research::sat::ToIntegerValueVector
std::vector< IntegerValue > ToIntegerValueVector(const std::vector< int64 > &input)
Definition: cp_constraints.h:101
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::PartialIsOneOfVar
std::function< void(Model *)> PartialIsOneOfVar(IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
Definition: cp_constraints.h:159
target_var_
IntervalVar *const target_var_
Definition: sched_constraints.cc:230
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
rev.h
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::BooleanXorPropagator::BooleanXorPropagator
BooleanXorPropagator(const std::vector< Literal > &literals, bool value, Trail *trail, IntegerTrail *integer_trail)
Definition: cp_constraints.h:40
operations_research::sat::Literal
Definition: sat_base.h:64
input
static int input(yyscan_t yyscanner)
vars_
const std::vector< IntVar * > vars_
Definition: alldiff_cst.cc:43
operations_research::sat::BooleanXorPropagator::Propagate
bool Propagate() final
Definition: cp_constraints.cc:26
operations_research::sat::BooleanXorPropagator
Definition: cp_constraints.h:38
operations_research::sat::GreaterThanAtLeastOneOf
std::function< void(Model *)> GreaterThanAtLeastOneOf(IntegerVariable target_var, const absl::Span< const IntegerVariable > vars, const absl::Span< const IntegerValue > offsets, const absl::Span< const Literal > selectors)
Definition: cp_constraints.h:123
integer.h
operations_research::sat::Trail
Definition: sat_base.h:233