OR-Tools  8.2
cp_model_postsolve.cc
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
15
17
18namespace operations_research {
19namespace sat {
20
21// This postsolve is "special". If the clause is not satisfied, we fix the
22// first literal in the clause to true (even if it was fixed to false). This
23// allows to handle more complex presolve operations used by the SAT presolver.
24//
25// Also, any "free" Boolean should be fixed to some value for the subsequent
26// postsolve steps.
27void PostsolveClause(const ConstraintProto& ct, std::vector<Domain>* domains) {
28 const int size = ct.bool_or().literals_size();
29 CHECK_NE(size, 0);
30 bool satisfied = false;
31 for (int i = 0; i < size; ++i) {
32 const int ref = ct.bool_or().literals(i);
33 const int var = PositiveRef(ref);
34 if ((*domains)[var].IsFixed()) {
35 if ((*domains)[var].FixedValue() == (RefIsPositive(ref) ? 1 : 0)) {
36 satisfied = true;
37 }
38 } else {
39 // We still need to assign free variable. Any value should work.
40 (*domains)[PositiveRef(ref)] = Domain(0);
41 }
42 }
43 if (satisfied) return;
44
45 // Change the value of the first variable (which was chosen at presolve).
46 const int first_ref = ct.bool_or().literals(0);
47 (*domains)[PositiveRef(first_ref)] = Domain(RefIsPositive(first_ref) ? 1 : 0);
48}
49
50void PostsolveExactlyOne(const ConstraintProto& ct,
51 std::vector<Domain>* domains) {
52 bool satisfied = false;
53 std::vector<int> free_variables;
54 for (const int ref : ct.exactly_one().literals()) {
55 const int var = PositiveRef(ref);
56 if ((*domains)[var].IsFixed()) {
57 if ((*domains)[var].FixedValue() == (RefIsPositive(ref) ? 1 : 0)) {
58 CHECK(!satisfied) << "Two variables at one in exactly one.";
59 satisfied = true;
60 }
61 } else {
62 free_variables.push_back(ref);
63 }
64 }
65 if (!satisfied) {
66 // Fix one at true.
67 CHECK(!free_variables.empty()) << "All zero in exactly one";
68 const int ref = free_variables.back();
69 (*domains)[PositiveRef(ref)] = Domain(RefIsPositive(ref) ? 1 : 0);
70 free_variables.pop_back();
71 }
72
73 // Fix any free variable left at false.
74 for (const int ref : free_variables) {
75 (*domains)[PositiveRef(ref)] = Domain(RefIsPositive(ref) ? 0 : 1);
76 }
77}
78
79// Here we simply assign all non-fixed variable to a feasible value. Which
80// should always exists by construction.
81void PostsolveLinear(const ConstraintProto& ct,
82 const std::vector<bool>& prefer_lower_value,
83 std::vector<Domain>* domains) {
84 int64 fixed_activity = 0;
85 const int size = ct.linear().vars().size();
86 std::vector<int> free_vars;
87 std::vector<int64> free_coeffs;
88 for (int i = 0; i < size; ++i) {
89 const int var = ct.linear().vars(i);
90 const int64 coeff = ct.linear().coeffs(i);
91 CHECK_LT(var, domains->size());
92 if (coeff == 0) continue;
93 if ((*domains)[var].IsFixed()) {
94 fixed_activity += (*domains)[var].FixedValue() * coeff;
95 } else {
96 free_vars.push_back(var);
97 free_coeffs.push_back(coeff);
98 }
99 }
100 if (free_vars.empty()) return;
101
102 // Fast track for the most common case.
103 const Domain initial_rhs = ReadDomainFromProto(ct.linear());
104 if (free_vars.size() == 1) {
105 const int var = free_vars[0];
106 const Domain domain = initial_rhs.AdditionWith(Domain(-fixed_activity))
107 .InverseMultiplicationBy(free_coeffs[0])
108 .IntersectionWith((*domains)[var]);
109 const int64 value = prefer_lower_value[var] ? domain.Min() : domain.Max();
110 (*domains)[var] = Domain(value);
111 return;
112 }
113
114 // The postsolve code is a bit involved if there is more than one free
115 // variable, we have to postsolve them one by one.
116 //
117 // Here we recompute the same domains as during the presolve. Everything is
118 // like if we where substiting the variable one by one:
119 // terms[i] + fixed_activity \in rhs_domains[i]
120 // In the reverse order.
121 std::vector<Domain> rhs_domains;
122 rhs_domains.push_back(initial_rhs);
123 for (int i = 0; i + 1 < free_vars.size(); ++i) {
124 // Note that these should be exactly the same computation as the one done
125 // during presolve and should be exact. However, we have some tests that do
126 // not comply, so we don't check exactness here. Also, as long as we don't
127 // get empty domain below, and the complexity of the domain do not explode
128 // here, we should be fine.
129 Domain term = (*domains)[free_vars[i]].MultiplicationBy(-free_coeffs[i]);
130 rhs_domains.push_back(term.AdditionWith(rhs_domains.back()));
131 }
132 for (int i = free_vars.size() - 1; i >= 0; --i) {
133 // Choose a value for free_vars[i] that fall into rhs_domains[i] -
134 // fixed_activity. This will crash if the intersection is empty, but it
135 // shouldn't be.
136 const int var = free_vars[i];
137 const int64 coeff = free_coeffs[i];
138 const Domain domain = rhs_domains[i]
139 .AdditionWith(Domain(-fixed_activity))
141 .IntersectionWith((*domains)[var]);
142
143 // TODO(user): I am not 100% that the algo here might cover all the presolve
144 // case, so if this fail, it might indicate an issue here and not in the
145 // presolve/solver code.
146 CHECK(!domain.IsEmpty()) << ct.ShortDebugString();
147 const int64 value = prefer_lower_value[var] ? domain.Min() : domain.Max();
148 (*domains)[var] = Domain(value);
149
150 fixed_activity += coeff * value;
151 }
152 DCHECK(initial_rhs.Contains(fixed_activity));
153}
154
155// We assign any non fixed lhs variables to their minimum value. Then we assign
156// the target to the max. This should always be feasible.
157void PostsolveIntMax(const ConstraintProto& ct, std::vector<Domain>* domains) {
158 int64 m = kint64min;
159 for (const int ref : ct.int_max().vars()) {
160 const int var = PositiveRef(ref);
161 if (!(*domains)[var].IsFixed()) {
162 // Assign to minimum value.
163 const int64 value =
164 RefIsPositive(ref) ? (*domains)[var].Min() : (*domains)[var].Max();
165 (*domains)[var] = Domain(value);
166 }
167
168 const int64 value = (*domains)[var].FixedValue();
169 m = std::max(m, RefIsPositive(ref) ? value : -value);
170 }
171 const int target_ref = ct.int_max().target();
172 const int target_var = PositiveRef(target_ref);
173 if (RefIsPositive(target_ref)) {
174 (*domains)[target_var] = (*domains)[target_var].IntersectionWith(Domain(m));
175 } else {
176 (*domains)[target_var] =
177 (*domains)[target_var].IntersectionWith(Domain(-m));
178 }
179 CHECK(!(*domains)[target_var].IsEmpty());
180}
181
182// We only support 3 cases in the presolve currently.
183void PostsolveElement(const ConstraintProto& ct, std::vector<Domain>* domains) {
184 const int index_ref = ct.element().index();
185 const int index_var = PositiveRef(index_ref);
186 const int target_ref = ct.element().target();
187 const int target_var = PositiveRef(target_ref);
188
189 // Deal with non-fixed target and non-fixed index. This only happen if
190 // whatever the value of the index and selected variable, we can choose a
191 // valid target, so we just fix the index to its min value in this case.
192 if (!(*domains)[target_var].IsFixed() && !(*domains)[index_var].IsFixed()) {
193 const int64 index_value = (*domains)[index_var].Min();
194 (*domains)[index_var] = Domain(index_value);
195
196 // If the selected variable is not fixed, we also need to fix it.
197 const int selected_ref = ct.element().vars(
198 RefIsPositive(index_ref) ? index_value : -index_value);
199 const int selected_var = PositiveRef(selected_ref);
200 if (!(*domains)[selected_var].IsFixed()) {
201 (*domains)[selected_var] = Domain((*domains)[selected_var].Min());
202 }
203 }
204
205 // Deal with fixed index (and constant vars).
206 if ((*domains)[index_var].IsFixed()) {
207 const int64 index_value = (*domains)[index_var].FixedValue();
208 const int selected_ref = ct.element().vars(
209 RefIsPositive(index_ref) ? index_value : -index_value);
210 const int selected_var = PositiveRef(selected_ref);
211 const int64 selected_value = (*domains)[selected_var].FixedValue();
212 (*domains)[target_var] = (*domains)[target_var].IntersectionWith(
213 Domain(RefIsPositive(target_ref) == RefIsPositive(selected_ref)
214 ? selected_value
215 : -selected_value));
216 DCHECK(!(*domains)[target_var].IsEmpty());
217 return;
218 }
219
220 // Deal with fixed target (and constant vars).
221 const int64 target_value = (*domains)[target_var].FixedValue();
222 int selected_index_value = -1;
223 for (int i = 0; i < ct.element().vars().size(); ++i) {
224 const int ref = ct.element().vars(i);
225 const int var = PositiveRef(ref);
226 const int64 value = (*domains)[var].FixedValue();
227 if (RefIsPositive(target_ref) == RefIsPositive(ref)) {
228 if (value == target_value) {
229 selected_index_value = i;
230 break;
231 }
232 } else {
233 if (value == -target_value) {
234 selected_index_value = i;
235 break;
236 }
237 }
238 }
239
240 CHECK_NE(selected_index_value, -1);
241 (*domains)[index_var] = (*domains)[index_var].IntersectionWith(Domain(
242 RefIsPositive(index_var) ? selected_index_value : -selected_index_value));
243 DCHECK(!(*domains)[index_var].IsEmpty());
244}
245
246void PostsolveResponse(const int64 num_variables_in_original_model,
247 const CpModelProto& mapping_proto,
248 const std::vector<int>& postsolve_mapping,
249 CpSolverResponse* response) {
250 // Map back the sufficient assumptions for infeasibility.
251 for (int& ref :
252 *(response->mutable_sufficient_assumptions_for_infeasibility())) {
253 ref = RefIsPositive(ref) ? postsolve_mapping[ref]
254 : NegatedRef(postsolve_mapping[PositiveRef(ref)]);
255 }
256
257 // Abort if no solution or something is wrong.
258 if (response->status() != CpSolverStatus::FEASIBLE &&
259 response->status() != CpSolverStatus::OPTIMAL) {
260 return;
261 }
262 if (response->solution_size() != postsolve_mapping.size()) return;
263
264 // Read the initial variable domains, either from the fixed solution of the
265 // presolved problems or from the mapping model.
266 std::vector<Domain> domains(mapping_proto.variables_size());
267 for (int i = 0; i < postsolve_mapping.size(); ++i) {
268 CHECK_LE(postsolve_mapping[i], domains.size());
269 domains[postsolve_mapping[i]] = Domain(response->solution(i));
270 }
271 for (int i = 0; i < domains.size(); ++i) {
272 if (domains[i].IsEmpty()) {
273 domains[i] = ReadDomainFromProto(mapping_proto.variables(i));
274 }
275 CHECK(!domains[i].IsEmpty());
276 }
277
278 // Some free variable should be fixed towards their good objective direction.
279 //
280 // TODO(user): currently the objective is not part of the mapping_proto, so
281 // this shouldn't matter for our current presolve reduction.
282 CHECK(!mapping_proto.has_objective());
283 std::vector<bool> prefer_lower_value(domains.size(), true);
284 if (mapping_proto.has_objective()) {
285 const int size = mapping_proto.objective().vars().size();
286 for (int i = 0; i < size; ++i) {
287 int var = mapping_proto.objective().vars(i);
288 int64 coeff = mapping_proto.objective().coeffs(i);
289 if (!RefIsPositive(var)) {
291 coeff = -coeff;
292 }
293 prefer_lower_value[i] = (coeff >= 0);
294 }
295 }
296
297 // Process the constraints in reverse order.
298 const int num_constraints = mapping_proto.constraints_size();
299 for (int i = num_constraints - 1; i >= 0; i--) {
300 const ConstraintProto& ct = mapping_proto.constraints(i);
301
302 // We should only encounter assigned enforcement literal.
303 bool enforced = true;
304 for (const int ref : ct.enforcement_literal()) {
305 if (domains[PositiveRef(ref)].FixedValue() ==
306 (RefIsPositive(ref) ? 0 : 1)) {
307 enforced = false;
308 break;
309 }
310 }
311 if (!enforced) continue;
312
313 switch (ct.constraint_case()) {
314 case ConstraintProto::kBoolOr:
315 PostsolveClause(ct, &domains);
316 break;
317 case ConstraintProto::kExactlyOne:
318 PostsolveExactlyOne(ct, &domains);
319 break;
320 case ConstraintProto::kLinear:
321 PostsolveLinear(ct, prefer_lower_value, &domains);
322 break;
323 case ConstraintProto::kIntMax:
324 PostsolveIntMax(ct, &domains);
325 break;
326 case ConstraintProto::kElement:
327 PostsolveElement(ct, &domains);
328 break;
329 default:
330 // This should never happen as we control what kind of constraint we
331 // add to the mapping_proto;
332 LOG(FATAL) << "Unsupported constraint: " << ct.ShortDebugString();
333 }
334 }
335
336 // Fill the response. Maybe fix some still unfixed variable.
337 response->mutable_solution()->Clear();
338 CHECK_LE(num_variables_in_original_model, domains.size());
339 for (int i = 0; i < num_variables_in_original_model; ++i) {
340 if (prefer_lower_value[i]) {
341 response->add_solution(domains[i].Min());
342 } else {
343 response->add_solution(domains[i].Max());
344 }
345 }
346}
347
348} // namespace sat
349} // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
We call domain any subset of Int64 = [kint64min, kint64max].
Domain MultiplicationBy(int64 coeff, bool *exact=nullptr) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e * coeff}.
Domain InverseMultiplicationBy(const int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
Domain AdditionWith(const Domain &domain) const
Returns {x ∈ Int64, ∃ a ∈ D, ∃ b ∈ domain, x = a + b}.
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
bool IsEmpty() const
Returns true if this is the empty set.
bool Contains(int64 value) const
Returns true iff value is in Domain.
SharedResponseManager * response
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
static const int64 kint64min
const int FATAL
Definition: log_severity.h:32
void PostsolveLinear(const ConstraintProto &ct, const std::vector< bool > &prefer_lower_value, std::vector< Domain > *domains)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void PostsolveResponse(const int64 num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, CpSolverResponse *response)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1479
void PostsolveElement(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveExactlyOne(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveClause(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveIntMax(const ConstraintProto &ct, std::vector< Domain > *domains)
bool RefIsPositive(int ref)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...