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
29namespace operations_research {
30namespace 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.
39void 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...
211std::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