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