OR-Tools  8.2
presolve_context.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_PRESOLVE_CONTEXT_H_
15 #define OR_TOOLS_SAT_PRESOLVE_CONTEXT_H_
16 
17 #include <deque>
18 #include <vector>
19 
20 #include "ortools/sat/cp_model.pb.h"
22 #include "ortools/sat/model.h"
24 #include "ortools/sat/sat_parameters.pb.h"
25 #include "ortools/sat/util.h"
27 #include "ortools/util/bitset.h"
30 
31 namespace operations_research {
32 namespace sat {
33 
34 // We use some special constraint index in our variable <-> constraint graph.
35 constexpr int kObjectiveConstraint = -1;
36 constexpr int kAffineRelationConstraint = -2;
37 constexpr int kAssumptionsConstraint = -3;
38 
39 class PresolveContext;
40 
41 // When storing a reference to a literal, it is important not to forget when
42 // reading it back to take its representative. Otherwise, we might introduce
43 // literal that have already been removed, which will break invariants in a
44 // bunch of places.
45 class SavedLiteral {
46  public:
48  explicit SavedLiteral(int ref) : ref_(ref) {}
49  int Get(PresolveContext* context) const;
50 
51  private:
52  int ref_ = 0;
53 };
54 
55 // Same as SavedLiteral for variable.
57  public:
59  explicit SavedVariable(int ref) : ref_(ref) {}
60  int Get(PresolveContext* context) const;
61 
62  private:
63  int ref_ = 0;
64 };
65 
66 // Wrap the CpModelProto we are presolving with extra data structure like the
67 // in-memory domain of each variables and the constraint variable graph.
69  public:
70  explicit PresolveContext(bool log_info, Model* model, CpModelProto* cp_model,
71  CpModelProto* mapping)
72  : working_model(cp_model),
73  mapping_model(mapping),
74  log_info_(log_info),
75  params_(*model->GetOrCreate<SatParameters>()),
76  time_limit_(model->GetOrCreate<TimeLimit>()),
77  random_(model->GetOrCreate<ModelRandomGenerator>()) {}
78 
79  // Helpers to adds new variables to the presolved model.
80  int NewIntVar(const Domain& domain);
81  int NewBoolVar();
83 
84  // a => b.
85  void AddImplication(int a, int b);
86 
87  // b => x in [lb, ub].
88  void AddImplyInDomain(int b, int x, const Domain& domain);
89 
90  // Helpers to query the current domain of a variable.
91  bool DomainIsEmpty(int ref) const;
92  bool IsFixed(int ref) const;
93  bool CanBeUsedAsLiteral(int ref) const;
94  bool LiteralIsTrue(int lit) const;
95  bool LiteralIsFalse(int lit) const;
96  int64 MinOf(int ref) const;
97  int64 MaxOf(int ref) const;
98  bool DomainContains(int ref, int64 value) const;
99  Domain DomainOf(int ref) const;
100 
101  // Helpers to query the current domain of a linear expression.
102  // This doesn't check for integer overflow, but our linear expression
103  // should be such that this cannot happen (tested at validation).
104  int64 MinOf(const LinearExpressionProto& expr) const;
105  int64 MaxOf(const LinearExpressionProto& expr) const;
106 
107  // This function takes a positive variable reference.
108  bool DomainOfVarIsIncludedIn(int var, const Domain& domain) {
109  return domains[var].IsIncludedIn(domain);
110  }
111 
112  // Returns true if this ref only appear in one constraint.
113  bool VariableIsUniqueAndRemovable(int ref) const;
114 
115  // Returns true if this ref no longer appears in the model.
116  bool VariableIsNotUsedAnymore(int ref) const;
117 
118  // Functions to make sure that once we remove a variable, we no longer reuse
119  // it.
120  void MarkVariableAsRemoved(int ref);
121  bool VariableWasRemoved(int ref) const;
122 
123  // Same as VariableIsUniqueAndRemovable() except that in this case the
124  // variable also appear in the objective in addition to a single constraint.
125  bool VariableWithCostIsUniqueAndRemovable(int ref) const;
126 
127  // Returns true if an integer variable is only appearing in the rhs of
128  // constraints of the form lit => var in domain. When this is the case, then
129  // we can usually remove this variable and replace these constraints with
130  // the proper constraints on the enforcement literals.
131  bool VariableIsOnlyUsedInEncoding(int ref) const;
132 
133  // Returns false if the new domain is empty. Sets 'domain_modified' (if
134  // provided) to true iff the domain is modified otherwise does not change it.
135  ABSL_MUST_USE_RESULT bool IntersectDomainWith(
136  int ref, const Domain& domain, bool* domain_modified = nullptr);
137 
138  // Returns false if the 'lit' doesn't have the desired value in the domain.
139  ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit);
140  ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit);
141 
142  // This function always return false. It is just a way to make a little bit
143  // more sure that we abort right away when infeasibility is detected.
144  ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(
145  const std::string& message = "") {
146  // TODO(user): Report any explanation for the client in a nicer way?
147  VLOG(1) << "INFEASIBLE: " << message;
148  DCHECK(!is_unsat);
149  is_unsat = true;
150  return false;
151  }
152  bool ModelIsUnsat() const { return is_unsat; }
153 
154  // Stores a description of a rule that was just applied to have a summary of
155  // what the presolve did at the end.
156  void UpdateRuleStats(const std::string& name, int num_times = 1);
157 
158  // Updates the constraints <-> variables graph. This needs to be called each
159  // time a constraint is modified.
160  void UpdateConstraintVariableUsage(int c);
161 
162  // At the beginning of the presolve, we delay the costly creation of this
163  // "graph" until we at least ran some basic presolve. This is because during
164  // a LNS neighbhorhood, many constraints will be reduced significantly by
165  // this "simple" presolve.
167 
168  // Calls UpdateConstraintVariableUsage() on all newly created constraints.
170 
171  // Returns true if our current constraints <-> variables graph is ok.
172  // This is meant to be used in DEBUG mode only.
174 
175  // Regroups fixed variables with the same value.
176  // TODO(user): Also regroup cte and -cte?
177  void ExploitFixedDomain(int var);
178 
179  // Adds the relation (ref_x = coeff * ref_y + offset) to the repository.
180  // Once the relation is added, it doesn't need to be enforced by a constraint
181  // in the model proto, since we will propagate such relation directly and add
182  // them to the proto at the end of the presolve.
183  //
184  // Returns true if the relation was added.
185  // In some rare case, like if x = 3*z and y = 5*t are already added, we
186  // currently cannot add x = 2 * y and we will return false in these case. So
187  // when this returns false, the relation needs to be enforced by a separate
188  // constraint.
189  //
190  // If the relation was added, both variables will be marked to appear in the
191  // special kAffineRelationConstraint. This will allow to identify when a
192  // variable is no longer needed (only appear there and is not a
193  // representative).
194  bool StoreAffineRelation(int ref_x, int ref_y, int64 coeff, int64 offset);
195 
196  // Adds the fact that ref_a == ref_b using StoreAffineRelation() above.
197  // This should never fail, so the relation will always be added.
198  void StoreBooleanEqualityRelation(int ref_a, int ref_b);
199 
200  // Stores/Get the relation target_ref = abs(ref); The first function returns
201  // false if it already exist and the second false if it is not present.
202  bool StoreAbsRelation(int target_ref, int ref);
203  bool GetAbsRelation(int target_ref, int* ref);
204 
205  // Returns the representative of a literal.
206  int GetLiteralRepresentative(int ref) const;
207 
208  // Returns another reference with exactly the same value.
209  int GetVariableRepresentative(int ref) const;
210 
211  // Used for statistics.
212  int NumAffineRelations() const { return affine_relations_.NumRelations(); }
213  int NumEquivRelations() const { return var_equiv_relations_.NumRelations(); }
214 
215  // This makes sure that the affine relation only uses one of the
216  // representative from the var_equiv_relations.
218 
219  // To facilitate debugging.
220  std::string RefDebugString(int ref) const;
221  std::string AffineRelationDebugString(int ref) const;
222 
223  // Makes sure the domain of ref and of its representative are in sync.
224  // Returns false on unsat.
225  bool PropagateAffineRelation(int ref);
226 
227  // Creates the internal structure for any new variables in working_model.
228  void InitializeNewDomains();
229 
230  // Clears the "rules" statistics.
231  void ClearStats();
232 
233  // Inserts the given literal to encode ref == value.
234  // If an encoding already exists, it adds the two implications between
235  // the previous encoding and the new encoding.
236  //
237  // Important: This does not update the constraint<->variable graph, so
238  // ConstraintVariableGraphIsUpToDate() will be false until
239  // UpdateNewConstraintsVariableUsage() is called.
240  void InsertVarValueEncoding(int literal, int ref, int64 value);
241 
242  // Gets the associated literal if it is already created. Otherwise
243  // create it, add the corresponding constraints and returns it.
244  //
245  // Important: This does not update the constraint<->variable graph, so
246  // ConstraintVariableGraphIsUpToDate() will be false until
247  // UpdateNewConstraintsVariableUsage() is called.
249 
250  // If not already done, adds a Boolean to represent any integer variables that
251  // take only two values. Make sure all the relevant affine and encoding
252  // relations are updated.
253  //
254  // Note that this might create a new Boolean variable.
256 
257  // Returns true if a literal attached to ref == var exists.
258  // It assigns the corresponding to `literal` if non null.
259  bool HasVarValueEncoding(int ref, int64 value, int* literal = nullptr);
260 
261  // Stores the fact that literal implies var == value.
262  // It returns true if that information is new.
264 
265  // Stores the fact that literal implies var != value.
266  // It returns true if that information is new.
268 
269  // Objective handling functions. We load it at the beginning so that during
270  // presolve we can work on the more efficient hash_map representation.
271  //
272  // Note that ReadObjectiveFromProto() makes sure that var_to_constraints of
273  // all the variable that appear in the objective contains -1. This is later
274  // enforced by all the functions modifying the objective.
275  //
276  // Note(user): Because we process affine relation only on
277  // CanonicalizeObjective(), it is possible that when processing a
278  // canonicalized linear constraint, we don't detect that a variable in affine
279  // relation is in the objective. For now this is fine, because when this is
280  // the case, we also have an affine linear constraint, so we can't really do
281  // anything with that variable since it appear in at least two constraints.
282  void ReadObjectiveFromProto();
283  ABSL_MUST_USE_RESULT bool CanonicalizeObjective();
284  void WriteObjectiveToProto() const;
285 
286  // Given a variable defined by the given inequality that also appear in the
287  // objective, remove it from the objective by transferring its cost to other
288  // variables in the equality.
289  //
290  // If new_vars_in_objective is not nullptr, it will be filled with "new"
291  // variables that where not in the objective before and are after
292  // substitution.
293  //
294  // Returns false, if the substitution cannot be done. This is the case if the
295  // model become UNSAT or if doing it will result in an objective that do not
296  // satisfy our overflow preconditions. Note that this can only happen if the
297  // substitued variable is not implied free (i.e. if its domain is smaller than
298  // the implied domain from the equality).
300  int var_in_equality, int64 coeff_in_equality,
301  const ConstraintProto& equality,
302  std::vector<int>* new_vars_in_objective = nullptr);
303 
304  // Objective getters.
305  const Domain& ObjectiveDomain() const { return objective_domain_; }
306  const absl::flat_hash_map<int, int64>& ObjectiveMap() const {
307  return objective_map_;
308  }
310  return objective_domain_is_constraining_;
311  }
312 
313  // Advanced usage. This should be called when a variable can be removed from
314  // the problem, so we don't count it as part of an affine relation anymore.
317 
318  // Variable <-> constraint graph.
319  // The vector list is sorted and contains unique elements.
320  //
321  // Important: To properly handle the objective, var_to_constraints[objective]
322  // contains -1 so that if the objective appear in only one constraint, the
323  // constraint cannot be simplified.
324  const std::vector<int>& ConstraintToVars(int c) const {
326  return constraint_to_vars_[c];
327  }
328  const absl::flat_hash_set<int>& VarToConstraints(int var) const {
330  return var_to_constraints_[var];
331  }
332  int IntervalUsage(int c) const {
334  return interval_usage_[c];
335  }
336 
337  // Make sure we never delete an "assumption" literal by using a special
338  // constraint for that.
340  for (const int ref : working_model->assumptions()) {
341  var_to_constraints_[PositiveRef(ref)].insert(kAssumptionsConstraint);
342  }
343  }
344 
345  // The following helper adds the following constraint:
346  // result <=> (time_i <= time_j && active_i is true && active_j is true)
347  // and returns the (cached) literal result.
348  //
349  // Note that this cache should just be used temporarily and then cleared
350  // with ClearPrecedenceCache() because there is no mechanism to update the
351  // cached literals when literal equivalence are detected.
352  int GetOrCreateReifiedPrecedenceLiteral(int time_i, int time_j, int active_i,
353  int active_j);
354 
355  // Clear the precedence cache.
356  void ClearPrecedenceCache();
357 
358  bool log_info() const { return log_info_; }
359  const SatParameters& params() const { return params_; }
360  TimeLimit* time_limit() { return time_limit_; }
361  ModelRandomGenerator* random() { return random_; }
362 
363  // For each variables, list the constraints that just enforce a lower bound
364  // (resp. upper bound) on that variable. If all the constraints in which a
365  // variable appear are in the same direction, then we can usually fix a
366  // variable to one of its bound (modulo its cost).
367  //
368  // TODO(user): Keeping these extra vector of hash_set seems inefficient. Come
369  // up with a better way to detect if a variable is only constrainted in one
370  // direction.
371  std::vector<absl::flat_hash_set<int>> var_to_ub_only_constraints;
372  std::vector<absl::flat_hash_set<int>> var_to_lb_only_constraints;
373 
374  CpModelProto* working_model = nullptr;
375  CpModelProto* mapping_model = nullptr;
376 
377  // Indicate if we are allowed to remove irrelevant feasible solution from the
378  // set of feasible solution. For example, if a variable is unused, can we fix
379  // it to an arbitrary value (or its mimimum objective one)? This must be true
380  // if the client wants to enumerate all solutions or wants correct tightened
381  // bounds in the response.
383 
384  // If true, fills stats_by_rule_name, otherwise do not do that. This can take
385  // a few percent of the run time with a lot of LNS threads.
386  bool enable_stats = true;
387 
388  // Just used to display statistics on the presolve rules that were used.
389  absl::flat_hash_map<std::string, int> stats_by_rule_name;
390 
391  // Number of "rules" applied. This should be equal to the sum of all numbers
392  // in stats_by_rule_name. This is used to decide if we should do one more pass
393  // of the presolve or not. Note that depending on the presolve transformation,
394  // a rule can correspond to a tiny change or a big change. Because of that,
395  // this isn't a perfect proxy for the efficacy of the presolve.
397 
398  // Temporary storage.
399  std::vector<int> tmp_literals;
400  std::vector<Domain> tmp_term_domains;
401  std::vector<Domain> tmp_left_domains;
402  absl::flat_hash_set<int> tmp_literal_set;
403 
404  // Each time a domain is modified this is set to true.
406 
407  // Advanced presolve. See this class comment.
409 
410  private:
411  // Helper to add an affine relation x = c.y + o to the given repository.
412  bool AddRelation(int x, int y, int64 c, int64 o, AffineRelation* repo);
413 
414  void AddVariableUsage(int c);
415  void UpdateLinear1Usage(const ConstraintProto& ct, int c);
416 
417  // Returns true iff the variable is not the representative of an equivalence
418  // class of size at least 2.
419  bool VariableIsNotRepresentativeOfEquivalenceClass(int var) const;
420 
421  // Process encoding_remap_queue_ and updates the encoding maps. This could
422  // lead to UNSAT being detected, in which case it will return false.
423  bool RemapEncodingMaps();
424 
425  // Makes sure we only insert encoding about the current representative.
426  //
427  // Returns false if ref cannot take the given value (it might not have been
428  // propagated yed).
429  bool CanonicalizeEncoding(int* ref, int64* value);
430 
431  // Inserts an half reified var value encoding (literal => var ==/!= value).
432  // It returns true if the new state is different from the old state.
433  // Not that if imply_eq is false, the literal will be stored in its negated
434  // form.
435  //
436  // Thus, if you detect literal <=> var == value, then two calls must be made:
437  // InsertHalfVarValueEncoding(literal, var, value, true);
438  // InsertHalfVarValueEncoding(NegatedRef(literal), var, value, false);
439  bool InsertHalfVarValueEncoding(int literal, int var, int64 value,
440  bool imply_eq);
441 
442  // Insert fully reified var-value encoding.
443  void InsertVarValueEncodingInternal(int literal, int var, int64 value,
444  bool add_constraints);
445 
446  const bool log_info_;
447  const SatParameters& params_;
448  TimeLimit* time_limit_;
449  ModelRandomGenerator* random_;
450 
451  // Initially false, and set to true on the first inconsistency.
452  bool is_unsat = false;
453 
454  // The current domain of each variables.
455  std::vector<Domain> domains;
456 
457  // Internal representation of the objective. During presolve, we first load
458  // the objective in this format in order to have more efficient substitution
459  // on large problems (also because the objective is often dense). At the end
460  // we re-convert it to its proto form.
461  absl::flat_hash_map<int, int64> objective_map_;
462  int64 objective_overflow_detection_;
463  std::vector<std::pair<int, int64>> tmp_entries_;
464  bool objective_domain_is_constraining_ = false;
465  Domain objective_domain_;
466  double objective_offset_;
467  double objective_scaling_factor_;
468 
469  // Constraints <-> Variables graph.
470  std::vector<std::vector<int>> constraint_to_vars_;
471  std::vector<absl::flat_hash_set<int>> var_to_constraints_;
472 
473  // Number of constraints of the form [lit =>] var in domain.
474  std::vector<int> constraint_to_linear1_var_;
475  std::vector<int> var_to_num_linear1_;
476 
477  // We maintain how many time each interval is used.
478  std::vector<std::vector<int>> constraint_to_intervals_;
479  std::vector<int> interval_usage_;
480 
481  // Contains abs relation (key = abs(saved_variable)).
482  absl::flat_hash_map<int, SavedVariable> abs_relations_;
483 
484  // For each constant variable appearing in the model, we maintain a reference
485  // variable with the same constant value. If two variables end up having the
486  // same fixed value, then we can detect it using this and add a new
487  // equivalence relation. See ExploitFixedDomain().
488  absl::flat_hash_map<int64, SavedVariable> constant_to_ref_;
489 
490  // When a "representative" gets a new representative, it should be enqueued
491  // here so that we can lazily update the *encoding_ maps below.
492  std::deque<int> encoding_remap_queue_;
493 
494  // Contains variables with some encoded value: encoding_[i][v] points
495  // to the literal attached to the value v of the variable i.
496  absl::flat_hash_map<int, absl::flat_hash_map<int64, SavedLiteral>> encoding_;
497 
498  // Contains the currently collected half value encodings:
499  // i.e.: literal => var ==/!= value
500  // The state is accumulated (adding x => var == value then !x => var != value)
501  // will deduce that x equivalent to var == value.
502  absl::flat_hash_map<int, absl::flat_hash_map<int64, absl::flat_hash_set<int>>>
503  eq_half_encoding_;
504  absl::flat_hash_map<int, absl::flat_hash_map<int64, absl::flat_hash_set<int>>>
505  neq_half_encoding_;
506 
507  // This regroups all the affine relations between variables. Note that the
508  // constraints used to detect such relations will not be removed from the
509  // model at detection time (thus allowing proper domain propagation). However,
510  // if the arity of a variable becomes one, then such constraint will be
511  // removed.
512  AffineRelation affine_relations_;
513  AffineRelation var_equiv_relations_;
514 
515  std::vector<int> tmp_new_usage_;
516 
517  // Used by SetVariableAsRemoved() and VariableWasRemoved().
518  absl::flat_hash_set<int> removed_variables_;
519 
520  // Cache for the reified precedence literals created during the expansion of
521  // the reservoir constraint. This cache is only valid during the expansion
522  // phase, and is cleared afterwards.
523  absl::flat_hash_map<std::tuple<int, int, int, int>, int>
524  reified_precedences_cache_;
525 };
526 
527 } // namespace sat
528 } // namespace operations_research
529 
530 #endif // OR_TOOLS_SAT_PRESOLVE_CONTEXT_H_
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
We call domain any subset of Int64 = [kint64min, kint64max].
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
bool StoreAbsRelation(int target_ref, int ref)
ABSL_MUST_USE_RESULT bool IntersectDomainWith(int ref, const Domain &domain, bool *domain_modified=nullptr)
void InsertVarValueEncoding(int literal, int ref, int64 value)
std::vector< absl::flat_hash_set< int > > var_to_lb_only_constraints
int GetOrCreateVarValueEncoding(int ref, int64 value)
bool DomainContains(int ref, int64 value) const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value)
bool DomainOfVarIsIncludedIn(int var, const Domain &domain)
bool VariableWithCostIsUniqueAndRemovable(int ref) const
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value)
std::vector< absl::flat_hash_set< int > > var_to_ub_only_constraints
const std::vector< int > & ConstraintToVars(int c) const
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(const std::string &message="")
bool HasVarValueEncoding(int ref, int64 value, int *literal=nullptr)
std::string AffineRelationDebugString(int ref) const
absl::flat_hash_map< std::string, int > stats_by_rule_name
void StoreBooleanEqualityRelation(int ref_a, int ref_b)
bool SubstituteVariableInObjective(int var_in_equality, int64 coeff_in_equality, const ConstraintProto &equality, std::vector< int > *new_vars_in_objective=nullptr)
const absl::flat_hash_map< int, int64 > & ObjectiveMap() const
PresolveContext(bool log_info, Model *model, CpModelProto *cp_model, CpModelProto *mapping)
void UpdateRuleStats(const std::string &name, int num_times=1)
ABSL_MUST_USE_RESULT bool CanonicalizeObjective()
const SatParameters & params() const
AffineRelation::Relation GetAffineRelation(int ref) const
const absl::flat_hash_set< int > & VarToConstraints(int var) const
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
int GetOrCreateReifiedPrecedenceLiteral(int time_i, int time_j, int active_i, int active_j)
absl::flat_hash_set< int > tmp_literal_set
void AddImplyInDomain(int b, int x, const Domain &domain)
bool GetAbsRelation(int target_ref, int *ref)
bool StoreAffineRelation(int ref_x, int ref_y, int64 coeff, int64 offset)
int Get(PresolveContext *context) const
int Get(PresolveContext *context) const
const std::string name
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
GurobiMPCallbackContext * context
int64_t int64
constexpr int kAffineRelationConstraint
constexpr int kAssumptionsConstraint
constexpr int kObjectiveConstraint
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
std::string message
Definition: trace.cc:395