OR-Tools  8.2
cp_model_loader.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_MODEL_LOADER_H_
15 #define OR_TOOLS_SAT_CP_MODEL_LOADER_H_
16 
17 #include <functional>
18 #include <vector>
19 
20 #include "absl/container/flat_hash_set.h"
21 #include "ortools/base/int_type.h"
23 #include "ortools/base/logging.h"
24 #include "ortools/base/map_util.h"
26 #include "ortools/sat/cp_model.pb.h"
28 #include "ortools/sat/integer.h"
29 #include "ortools/sat/intervals.h"
30 #include "ortools/sat/model.h"
31 #include "ortools/sat/sat_base.h"
32 
33 namespace operations_research {
34 namespace sat {
35 
36 // For an optimization problem, this contains the internal integer objective
37 // to minimize and information on how to display it correctly in the logs.
39  double scaling_factor = 1.0;
40  double offset = 0.0;
41  IntegerVariable objective_var = kNoIntegerVariable;
42 
43  // The objective linear expression that should be equal to objective_var.
44  // If not all proto variable have an IntegerVariable view, then some vars
45  // will be set to kNoIntegerVariable. In practice, when this is used, we make
46  // sure there is a view though.
47  std::vector<IntegerVariable> vars;
48  std::vector<IntegerValue> coeffs;
49 
50  // List of variable that when set to their lower bound should help getting a
51  // better objective. This is used by some search heuristic to preferably
52  // assign any of the variable here to their lower bound first.
53  absl::flat_hash_set<IntegerVariable> objective_impacting_variables;
54 
55  double ScaleIntegerObjective(IntegerValue value) const {
56  return (ToDouble(value) + offset) * scaling_factor;
57  }
58 };
59 
60 // Holds the mapping between CpModel proto indices and the sat::model ones.
61 //
62 // This also holds some information used when loading a CpModel proto.
64  public:
65  // Extracts all the used variables in the CpModelProto and creates a
66  // sat::Model representation for them. More precisely
67  // - All Boolean variables will be mapped.
68  // - All Interval variables will be mapped.
69  // - All non-Boolean variable will have a corresponding IntegerVariable, and
70  // depending on the view_all_booleans_as_integers, some or all of the
71  // BooleanVariable will also have an IntegerVariable corresponding to its
72  // "integer view".
73  //
74  // Note(user): We could create IntegerVariable on the fly as they are needed,
75  // but that loose the original variable order which might be useful in
76  // heuristics later.
77  void CreateVariables(const CpModelProto& model_proto,
78  bool view_all_booleans_as_integers, Model* m);
79 
80  // Automatically detect optional variables.
81  void DetectOptionalVariables(const CpModelProto& model_proto, Model* m);
82 
83  // Experimental. Loads the symmetry form the proto symmetry field, as long as
84  // they only involve Booleans.
85  //
86  // TODO(user): We currently only have the code for Booleans, it is why we
87  // currently ignore symmetries involving integer variables.
88  void LoadBooleanSymmetries(const CpModelProto& model_proto, Model* m);
89 
90  // Extract the encodings (IntegerVariable <-> Booleans) present in the model.
91  // This effectively load some linear constraints of size 1 that will be marked
92  // as already loaded.
93  void ExtractEncoding(const CpModelProto& model_proto, Model* m);
94 
95  // Process all affine relations of the form a*X + b*Y == cte. For each
96  // literals associated to (X >= bound) or (X == value) associate it to its
97  // corresponding relation on Y. Also do the other side.
98  //
99  // TODO(user): In an ideal world, all affine relations like this should be
100  // removed in the presolve.
102  const CpModelProto& model_proto, Model* m);
103 
104  // Returns true if the given CpModelProto variable reference refers to a
105  // Boolean varaible. Such variable will always have an associated Literal(),
106  // but not always an associated Integer().
107  bool IsBoolean(int ref) const {
108  DCHECK_LT(PositiveRef(ref), booleans_.size());
109  return booleans_[PositiveRef(ref)] != kNoBooleanVariable;
110  }
111 
112  bool IsInteger(int ref) const {
113  DCHECK_LT(PositiveRef(ref), integers_.size());
114  return integers_[PositiveRef(ref)] != kNoIntegerVariable;
115  }
116 
117  sat::Literal Literal(int ref) const {
118  DCHECK(IsBoolean(ref));
119  return sat::Literal(booleans_[PositiveRef(ref)], RefIsPositive(ref));
120  }
121 
122  IntegerVariable Integer(int ref) const {
123  DCHECK(IsInteger(ref));
124  const IntegerVariable var = integers_[PositiveRef(ref)];
125  return RefIsPositive(ref) ? var : NegationOf(var);
126  }
127 
128  // TODO(user): We could "easily" create an intermediate variable for more
129  // complex linear expression. We could also identify duplicate expressions to
130  // not create two identical integer variable.
131  AffineExpression LoadAffineView(const LinearExpressionProto& exp) const {
132  CHECK_LE(exp.vars().size(), 1);
133  if (exp.vars().empty()) {
134  return AffineExpression(IntegerValue(exp.offset()));
135  }
136  return AffineExpression(Integer(exp.vars(0)), IntegerValue(exp.coeffs(0)),
137  IntegerValue(exp.offset()));
138  }
139 
140  IntervalVariable Interval(int i) const {
141  CHECK_GE(i, 0);
142  CHECK_LT(i, intervals_.size());
143  CHECK_NE(intervals_[i], kNoIntervalVariable);
144  return intervals_[i];
145  }
146 
147  template <typename List>
148  std::vector<IntegerVariable> Integers(const List& list) const {
149  std::vector<IntegerVariable> result;
150  for (const auto i : list) result.push_back(Integer(i));
151  return result;
152  }
153 
154  template <typename ProtoIndices>
155  std::vector<sat::Literal> Literals(const ProtoIndices& indices) const {
156  std::vector<sat::Literal> result;
157  for (const int i : indices) result.push_back(CpModelMapping::Literal(i));
158  return result;
159  }
160 
161  template <typename ProtoIndices>
162  std::vector<IntervalVariable> Intervals(const ProtoIndices& indices) const {
163  std::vector<IntervalVariable> result;
164  for (const int i : indices) result.push_back(Interval(i));
165  return result;
166  }
167 
168  // Depending on the option, we will load constraints in stages. This is used
169  // to detect constraints that are already loaded. For instance the interval
170  // constraints and the linear constraint of size 1 (encodings) are usually
171  // loaded first.
172  bool ConstraintIsAlreadyLoaded(const ConstraintProto* ct) const {
173  return already_loaded_ct_.contains(ct);
174  }
175 
176  // Returns true if the given constraint is a "half-encoding" constraint. That
177  // is, if it is of the form (b => size 1 linear) but there is no (<=) side in
178  // the model. Such constraint are detected while we extract integer encoding
179  // and are cached here so that we can deal properly with them during the
180  // linear relaxation.
181  bool IsHalfEncodingConstraint(const ConstraintProto* ct) const {
182  return is_half_encoding_ct_.contains(ct);
183  }
184 
185  // Note that both these functions returns positive reference or -1.
186  int GetProtoVariableFromBooleanVariable(BooleanVariable var) const {
187  if (var.value() >= reverse_boolean_map_.size()) return -1;
188  return reverse_boolean_map_[var];
189  }
190  int GetProtoVariableFromIntegerVariable(IntegerVariable var) const {
191  if (var.value() >= reverse_integer_map_.size()) return -1;
192  return reverse_integer_map_[var];
193  }
194 
195  const std::vector<IntegerVariable>& GetVariableMapping() const {
196  return integers_;
197  }
198 
199  // For logging only, these are not super efficient.
200  int NumIntegerVariables() const {
201  int result = 0;
202  for (const IntegerVariable var : integers_) {
203  if (var != kNoIntegerVariable) result++;
204  }
205  return result;
206  }
207  int NumBooleanVariables() const {
208  int result = 0;
209  for (const BooleanVariable var : booleans_) {
210  if (var != kNoBooleanVariable) result++;
211  }
212  return result;
213  }
214 
215  // Returns a heuristic set of values that could be created for the given
216  // variable when the constraints will be loaded.
217  // Note that the pointer is not stable across calls.
218  // It returns nullptr if the set is empty.
219  const absl::flat_hash_set<int64>& PotentialEncodedValues(int var) {
220  const auto& it = variables_to_encoded_values_.find(var);
221  if (it != variables_to_encoded_values_.end()) {
222  return it->second;
223  }
224  return empty_set_;
225  }
226 
227  private:
228  // Note that only the variables used by at least one constraint will be
229  // created, the other will have a kNo[Integer,Interval,Boolean]VariableValue.
230  std::vector<IntegerVariable> integers_;
231  std::vector<IntervalVariable> intervals_;
232  std::vector<BooleanVariable> booleans_;
233 
234  // Recover from a IntervalVariable/BooleanVariable its associated CpModelProto
235  // index. The value of -1 is used to indicate that there is no correspondence
236  // (i.e. this variable is only used internally).
237  absl::StrongVector<BooleanVariable, int> reverse_boolean_map_;
238  absl::StrongVector<IntegerVariable, int> reverse_integer_map_;
239 
240  // Set of constraints to ignore because they were already dealt with by
241  // ExtractEncoding().
242  absl::flat_hash_set<const ConstraintProto*> already_loaded_ct_;
243  absl::flat_hash_set<const ConstraintProto*> is_half_encoding_ct_;
244 
245  absl::flat_hash_map<int, absl::flat_hash_set<int64>>
246  variables_to_encoded_values_;
247  const absl::flat_hash_set<int64> empty_set_;
248 };
249 
250 // Inspects the model and use some heuristic to decide which variable, if any,
251 // should be fully encoded. Note that some constraints like the element or table
252 // constraints require some of their variables to be fully encoded.
253 //
254 // TODO(user): This function exists so that we fully encode first all the
255 // variable that needs to be fully encoded so that at loading time we can adapt
256 // the algorithm used. Howeve it needs to duplicate the logic that decide what
257 // needs to be fully encoded. Try to come up with a more robust design.
258 void MaybeFullyEncodeMoreVariables(const CpModelProto& model_proto, Model* m);
259 
260 // Calls one of the functions below.
261 // Returns false if we do not know how to load the given constraints.
262 bool LoadConstraint(const ConstraintProto& ct, Model* m);
263 
264 void LoadBoolOrConstraint(const ConstraintProto& ct, Model* m);
265 void LoadBoolAndConstraint(const ConstraintProto& ct, Model* m);
266 void LoadAtMostOneConstraint(const ConstraintProto& ct, Model* m);
267 void LoadExactlyOneConstraint(const ConstraintProto& ct, Model* m);
268 void LoadBoolXorConstraint(const ConstraintProto& ct, Model* m);
269 void LoadLinearConstraint(const ConstraintProto& ct, Model* m);
270 void LoadAllDiffConstraint(const ConstraintProto& ct, Model* m);
271 void LoadIntProdConstraint(const ConstraintProto& ct, Model* m);
272 void LoadIntDivConstraint(const ConstraintProto& ct, Model* m);
273 void LoadIntMinConstraint(const ConstraintProto& ct, Model* m);
274 void LoadLinMaxConstraint(const ConstraintProto& ct, Model* m);
275 void LoadIntMaxConstraint(const ConstraintProto& ct, Model* m);
276 void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m);
277 void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m);
278 void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m);
279 void LoadReservoirConstraint(const ConstraintProto& ct, Model* m);
280 void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m);
281 void LoadElementConstraintAC(const ConstraintProto& ct, Model* m);
282 void LoadElementConstraint(const ConstraintProto& ct, Model* m);
283 void LoadTableConstraint(const ConstraintProto& ct, Model* m);
284 void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m);
285 void LoadCircuitConstraint(const ConstraintProto& ct, Model* m);
286 void LoadRoutesConstraint(const ConstraintProto& ct, Model* m);
287 void LoadCircuitCoveringConstraint(const ConstraintProto& ct, Model* m);
288 void LoadInverseConstraint(const ConstraintProto& ct, Model* m);
289 
290 LinearExpression GetExprFromProto(const LinearExpressionProto& expr_proto,
291  const CpModelMapping& mapping);
292 
293 } // namespace sat
294 } // namespace operations_research
295 
296 #endif // OR_TOOLS_SAT_CP_MODEL_LOADER_H_
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define DCHECK(condition)
Definition: base/logging.h:884
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
size_type size() const
IntervalVariable Interval(int i) const
std::vector< sat::Literal > Literals(const ProtoIndices &indices) const
int GetProtoVariableFromIntegerVariable(IntegerVariable var) const
AffineExpression LoadAffineView(const LinearExpressionProto &exp) const
std::vector< IntegerVariable > Integers(const List &list) const
const std::vector< IntegerVariable > & GetVariableMapping() const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
void LoadBooleanSymmetries(const CpModelProto &model_proto, Model *m)
bool ConstraintIsAlreadyLoaded(const ConstraintProto *ct) const
bool IsHalfEncodingConstraint(const ConstraintProto *ct) const
int GetProtoVariableFromBooleanVariable(BooleanVariable var) const
IntegerVariable Integer(int ref) const
sat::Literal Literal(int ref) const
void DetectOptionalVariables(const CpModelProto &model_proto, Model *m)
const absl::flat_hash_set< int64 > & PotentialEncodedValues(int var)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
void PropagateEncodingFromEquivalenceRelations(const CpModelProto &model_proto, Model *m)
void CreateVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
CpModelProto const * model_proto
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
void LoadTableConstraint(const ConstraintProto &ct, Model *m)
void LoadCircuitCoveringConstraint(const ConstraintProto &ct, Model *m)
void LoadExactlyOneConstraint(const ConstraintProto &ct, Model *m)
void LoadIntProdConstraint(const ConstraintProto &ct, Model *m)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
void LoadBoolOrConstraint(const ConstraintProto &ct, Model *m)
bool RefIsPositive(int ref)
void MaybeFullyEncodeMoreVariables(const CpModelProto &model_proto, Model *m)
void LoadCumulativeConstraint(const ConstraintProto &ct, Model *m)
void LoadRoutesConstraint(const ConstraintProto &ct, Model *m)
void LoadReservoirConstraint(const ConstraintProto &ct, Model *m)
void LoadBoolAndConstraint(const ConstraintProto &ct, Model *m)
void LoadLinMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadBoolXorConstraint(const ConstraintProto &ct, Model *m)
LinearExpression GetExprFromProto(const LinearExpressionProto &expr_proto, const CpModelMapping &mapping)
const IntegerVariable kNoIntegerVariable(-1)
const IntervalVariable kNoIntervalVariable(-1)
void LoadIntDivConstraint(const ConstraintProto &ct, Model *m)
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
void LoadAtMostOneConstraint(const ConstraintProto &ct, Model *m)
void LoadCircuitConstraint(const ConstraintProto &ct, Model *m)
void LoadIntMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadNoOverlapConstraint(const ConstraintProto &ct, Model *m)
void LoadAllDiffConstraint(const ConstraintProto &ct, Model *m)
void LoadElementConstraint(const ConstraintProto &ct, Model *m)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
void LoadAutomatonConstraint(const ConstraintProto &ct, Model *m)
void LoadNoOverlap2dConstraint(const ConstraintProto &ct, Model *m)
void LoadIntMinConstraint(const ConstraintProto &ct, Model *m)
void LoadInverseConstraint(const ConstraintProto &ct, Model *m)
const BooleanVariable kNoBooleanVariable(-1)
void LoadElementConstraintAC(const ConstraintProto &ct, Model *m)
double ToDouble(IntegerValue value)
Definition: integer.h:69
void LoadElementConstraintBounds(const ConstraintProto &ct, Model *m)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
double ScaleIntegerObjective(IntegerValue value) const
absl::flat_hash_set< IntegerVariable > objective_impacting_variables