OR-Tools  8.2
cp_model_presolve.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_PRESOLVE_H_
15 #define OR_TOOLS_SAT_CP_MODEL_PRESOLVE_H_
16 
17 #include <vector>
18 
19 #include "ortools/sat/cp_model.pb.h"
23 #include "ortools/sat/sat_parameters.pb.h"
25 #include "ortools/util/bitset.h"
28 
29 namespace operations_research {
30 namespace sat {
31 
32 // Replaces all the instance of a variable i (and the literals referring to it)
33 // by mapping[i]. The definition of variables i is also moved to its new index.
34 // Variables with a negative mapping value are ignored and it is an error if
35 // such variable is referenced anywhere (this is CHECKed).
36 //
37 // The image of the mapping should be dense in [0, new_num_variables), this is
38 // also CHECKed.
39 void ApplyVariableMapping(const std::vector<int>& mapping,
40  const PresolveContext& context);
41 
42 // Presolves the initial content of presolved_model.
43 //
44 // This also creates a mapping model that encode the correspondence between the
45 // two problems. This works as follow:
46 // - The first variables of mapping_model are in one to one correspondence with
47 // the variables of the initial model.
48 // - The presolved_model variables are in one to one correspondence with the
49 // variable at the indices given by postsolve_mapping in the mapping model.
50 // - Fixing one of the two sets of variables and solving the model will assign
51 // the other set to a feasible solution of the other problem. Moreover, the
52 // objective value of these solutions will be the same. Note that solving such
53 // problems will take little time in practice because the propagation will
54 // basically do all the work.
55 //
56 // Note(user): an optimization model can be transformed into a decision problem,
57 // if for instance the objective is fixed, or independent from the rest of the
58 // problem.
59 //
60 // TODO(user): Identify disconnected components and returns a vector of
61 // presolved model? If we go this route, it may be nicer to store the indices
62 // inside the model. We can add a IntegerVariableProto::initial_index;
64  public:
66  std::vector<int>* postsolve_mapping);
67 
68  // Returns false if a non-recoverable error was encountered.
69  //
70  // TODO(user): Make sure this can never run into this case provided that the
71  // initial model is valid!
72  bool Presolve();
73 
74  // Executes presolve method for the given constraint. Public for testing only.
75  bool PresolveOneConstraint(int c);
76 
77  // Public for testing only.
79 
80  private:
81  void PresolveToFixPoint();
82 
83  // Runs the probing.
84  void Probe();
85 
86  // Presolve functions.
87  //
88  // They should return false only if the constraint <-> variable graph didn't
89  // change. This is just an optimization, returning true is always correct.
90  //
91  // Invariant about UNSAT: All these functions should abort right away if
92  // context_.IsUnsat() is true. And the only way to change the status to unsat
93  // is through ABSL_MUST_USE_RESULT function that should also abort right away
94  // the current code. This way we shouldn't keep doing computation on an
95  // inconsistent state.
96  // TODO(user,user): Make these public and unit test.
97  bool PresolveAutomaton(ConstraintProto* ct);
98  bool PresolveCircuit(ConstraintProto* ct);
99  bool PresolveRoutes(ConstraintProto* ct);
100  bool PresolveCumulative(ConstraintProto* ct);
101  bool PresolveNoOverlap(ConstraintProto* ct);
102  bool PresolveReservoir(ConstraintProto* ct);
103  bool PresolveAllDiff(ConstraintProto* ct);
104  bool PresolveTable(ConstraintProto* ct);
105  bool PresolveElement(ConstraintProto* ct);
106  bool PresolveInterval(int c, ConstraintProto* ct);
107  bool PresolveIntDiv(ConstraintProto* ct);
108  bool PresolveIntProd(ConstraintProto* ct);
109  bool PresolveIntMin(ConstraintProto* ct);
110  bool PresolveIntMax(ConstraintProto* ct);
111  bool PresolveLinMin(ConstraintProto* ct);
112  bool PresolveLinMax(ConstraintProto* ct);
113  bool PresolveIntAbs(ConstraintProto* ct);
114  bool PresolveBoolXor(ConstraintProto* ct);
115 
116  bool PresolveAtMostOrExactlyOne(ConstraintProto* ct);
117  bool PresolveAtMostOne(ConstraintProto* ct);
118  bool PresolveExactlyOne(ConstraintProto* ct);
119 
120  bool PresolveBoolAnd(ConstraintProto* ct);
121  bool PresolveBoolOr(ConstraintProto* ct);
122  bool PresolveEnforcementLiteral(ConstraintProto* ct);
123 
124  // Regroups terms and substitute affine relations.
125  // Returns true if the set of variables in the expression changed.
126  template <typename ProtoWithVarsAndCoeffs>
127  bool CanonicalizeLinearExpressionInternal(const ConstraintProto& ct,
128  ProtoWithVarsAndCoeffs* proto,
129  int64* offset);
130  bool CanonicalizeLinearExpression(const ConstraintProto& ct,
131  LinearExpressionProto* exp);
132 
133  // For the linear constraints, we have more than one function.
134  bool CanonicalizeLinear(ConstraintProto* ct);
135  bool PropagateDomainsInLinear(int c, ConstraintProto* ct);
136  bool RemoveSingletonInLinear(ConstraintProto* ct);
137  bool PresolveSmallLinear(ConstraintProto* ct);
138  bool PresolveLinearOnBooleans(ConstraintProto* ct);
139  void PresolveLinearEqualityModuloTwo(ConstraintProto* ct);
140 
141  // To simplify dealing with the two kind of intervals.
142  int64 StartMin(const IntervalConstraintProto& interval) const;
143  int64 EndMax(const IntervalConstraintProto& interval) const;
144  int64 SizeMin(const IntervalConstraintProto& interval) const;
145  int64 SizeMax(const IntervalConstraintProto& interval) const;
146 
147  // SetPPC is short for set packing, partitioning and covering constraints.
148  // These are sum of booleans <=, = and >= 1 respectively.
149  bool ProcessSetPPC();
150 
151  // Removes dominated constraints or fixes some variables for given pair of
152  // setppc constraints. This assumes that literals in constraint c1 is subset
153  // of literals in constraint c2.
154  bool ProcessSetPPCSubset(int c1, int c2, const std::vector<int>& c2_minus_c1,
155  const std::vector<int>& original_constraint_index,
156  std::vector<bool>* marked_for_removal);
157 
158  void PresolvePureSatPart();
159 
160  // Extracts AtMostOne constraint from Linear constraint.
161  void ExtractAtMostOneFromLinear(ConstraintProto* ct);
162 
163  void DivideLinearByGcd(ConstraintProto* ct);
164 
165  void ExtractEnforcementLiteralFromLinearConstraint(int ct_index,
166  ConstraintProto* ct);
167 
168  // Extracts cliques from bool_and and small at_most_one constraints and
169  // transforms them into maximal cliques.
170  void TransformIntoMaxCliques();
171 
172  // Converts bool_or and at_most_one of size 2 to bool_and.
173  void ExtractBoolAnd();
174 
175  void ExpandObjective();
176 
177  void TryToSimplifyDomain(int var);
178 
179  void MergeNoOverlapConstraints();
180 
181  // Boths function are responsible for dealing with affine relations.
182  // The second one returns false on UNSAT.
183  void EncodeAllAffineRelations();
184  bool PresolveAffineRelationIfAny(int var);
185 
186  bool ExploitEquivalenceRelations(int c, ConstraintProto* ct);
187 
188  ABSL_MUST_USE_RESULT bool RemoveConstraint(ConstraintProto* ct);
189  ABSL_MUST_USE_RESULT bool MarkConstraintAsFalse(ConstraintProto* ct);
190 
191  std::vector<int>* postsolve_mapping_;
192  PresolveContext* context_;
193 
194  // Used by CanonicalizeLinearExpressionInternal().
195  std::vector<std::pair<int, int64>> tmp_terms_;
196 };
197 
198 // Convenient wrapper to call the full presolve.
200  std::vector<int>* postsolve_mapping);
201 
202 // Returns the index of exact duplicate constraints in the given proto. That
203 // is, all returned constraints will have an identical constraint before it in
204 // the model_proto.constraints() list. Empty constraints are ignored.
205 //
206 // Visible here for testing. This is meant to be called at the end of the
207 // presolve where constraints have been canonicalized.
208 //
209 // TODO(user): Ignore names? canonicalize constraint further by sorting
210 // enforcement literal list for instance...
211 std::vector<int> FindDuplicateConstraints(const CpModelProto& model_proto);
212 
213 } // namespace sat
214 } // namespace operations_research
215 
216 #endif // OR_TOOLS_SAT_CP_MODEL_PRESOLVE_H_
CpModelPresolver(PresolveContext *context, std::vector< int > *postsolve_mapping)
CpModelProto proto
CpModelProto const * model_proto
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
GurobiMPCallbackContext * context
int64_t int64
bool PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
std::vector< int > FindDuplicateConstraints(const CpModelProto &model_proto)
void ApplyVariableMapping(const std::vector< int > &mapping, const PresolveContext &context)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
IntervalVar * interval
Definition: resource.cc:98