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 
18 namespace operations_research {
19 namespace 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.
27 void 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 
50 void 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.
81 void 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.
157 void 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.
183 void 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 
246 void 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)) {
290  var = PositiveRef(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 PostsolveElement(const ConstraintProto &ct, std::vector< Domain > *domains)
bool RefIsPositive(int ref)
void PostsolveIntMax(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveResponse(const int64 num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, CpSolverResponse *response)
void PostsolveExactlyOne(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveLinear(const ConstraintProto &ct, const std::vector< bool > &prefer_lower_value, std::vector< Domain > *domains)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void PostsolveClause(const ConstraintProto &ct, std::vector< Domain > *domains)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1479
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...