OR-Tools  8.2
cp_model_loader.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 
16 #include <algorithm>
17 #include <map>
18 #include <memory>
19 #include <set>
20 #include <string>
21 #include <utility>
22 #include <vector>
23 
24 #include "absl/container/flat_hash_map.h"
25 #include "absl/container/flat_hash_set.h"
26 #include "ortools/base/int_type.h"
27 #include "ortools/base/logging.h"
28 #include "ortools/base/map_util.h"
29 #include "ortools/base/stl_util.h"
32 #include "ortools/sat/circuit.h"
34 #include "ortools/sat/cp_model.pb.h"
36 #include "ortools/sat/cumulative.h"
37 #include "ortools/sat/diffn.h"
40 #include "ortools/sat/integer.h"
42 #include "ortools/sat/intervals.h"
45 #include "ortools/sat/sat_base.h"
46 #include "ortools/sat/sat_parameters.pb.h"
47 #include "ortools/sat/sat_solver.h"
48 #include "ortools/sat/symmetry.h"
49 #include "ortools/sat/table.h"
50 #include "ortools/sat/timetable.h"
53 
54 namespace operations_research {
55 namespace sat {
56 
57 namespace {
58 
59 template <typename Values>
60 std::vector<int64> ValuesFromProto(const Values& values) {
61  return std::vector<int64>(values.begin(), values.end());
62 }
63 
64 void ComputeLinearBounds(const LinearConstraintProto& proto,
65  CpModelMapping* mapping, IntegerTrail* integer_trail,
66  int64* sum_min, int64* sum_max) {
67  *sum_min = 0;
68  *sum_max = 0;
69 
70  for (int i = 0; i < proto.vars_size(); ++i) {
71  const int64 coeff = proto.coeffs(i);
72  const IntegerVariable var = mapping->Integer(proto.vars(i));
73  const int64 lb = integer_trail->LowerBound(var).value();
74  const int64 ub = integer_trail->UpperBound(var).value();
75  if (coeff >= 0) {
76  (*sum_min) += coeff * lb;
77  (*sum_max) += coeff * ub;
78  } else {
79  (*sum_min) += coeff * ub;
80  (*sum_max) += coeff * lb;
81  }
82  }
83 }
84 
85 // We check if the constraint is a sum(ax * xi) == value.
86 bool ConstraintIsEq(const LinearConstraintProto& proto) {
87  return proto.domain_size() == 2 && proto.domain(0) == proto.domain(1);
88 }
89 
90 // We check if the constraint is a sum(ax * xi) != value.
91 bool ConstraintIsNEq(const LinearConstraintProto& proto,
92  CpModelMapping* mapping, IntegerTrail* integer_trail,
93  int64* single_value) {
94  int64 sum_min = 0;
95  int64 sum_max = 0;
96  ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max);
97 
98  const Domain complement =
99  Domain(sum_min, sum_max)
100  .IntersectionWith(ReadDomainFromProto(proto).Complement());
101  if (complement.IsEmpty()) return false;
102  const int64 value = complement.Min();
103 
104  if (complement.Size() == 1) {
105  if (single_value != nullptr) {
106  *single_value = value;
107  }
108  return true;
109  }
110  return false;
111 }
112 
113 } // namespace
114 
116  bool view_all_booleans_as_integers,
117  Model* m) {
118  const int num_proto_variables = model_proto.variables_size();
119 
120  // All [0, 1] variables always have a corresponding Boolean, even if it is
121  // fixed to 0 (domain == [0,0]) or fixed to 1 (domain == [1,1]).
122  {
123  auto* sat_solver = m->GetOrCreate<SatSolver>();
124  CHECK_EQ(sat_solver->NumVariables(), 0);
125 
126  BooleanVariable new_var(0);
127  std::vector<BooleanVariable> false_variables;
128  std::vector<BooleanVariable> true_variables;
129 
130  booleans_.resize(num_proto_variables, kNoBooleanVariable);
131  reverse_boolean_map_.resize(num_proto_variables, -1);
132  for (int i = 0; i < num_proto_variables; ++i) {
133  const auto& domain = model_proto.variables(i).domain();
134  if (domain.size() != 2) continue;
135  if (domain[0] >= 0 && domain[1] <= 1) {
136  booleans_[i] = new_var;
137  reverse_boolean_map_[new_var] = i;
138  if (domain[1] == 0) {
139  false_variables.push_back(new_var);
140  } else if (domain[0] == 1) {
141  true_variables.push_back(new_var);
142  }
143  ++new_var;
144  }
145  }
146 
147  sat_solver->SetNumVariables(new_var.value());
148  for (const BooleanVariable var : true_variables) {
149  m->Add(ClauseConstraint({sat::Literal(var, true)}));
150  }
151  for (const BooleanVariable var : false_variables) {
152  m->Add(ClauseConstraint({sat::Literal(var, false)}));
153  }
154  }
155 
156  // Compute the list of positive variable reference for which we need to
157  // create an IntegerVariable.
158  std::vector<int> var_to_instantiate_as_integer;
159  if (view_all_booleans_as_integers) {
160  var_to_instantiate_as_integer.resize(num_proto_variables);
161  for (int i = 0; i < num_proto_variables; ++i) {
162  var_to_instantiate_as_integer[i] = i;
163  }
164  } else {
165  // Compute the integer variable references used by the model.
166  absl::flat_hash_set<int> used_variables;
167 
168  IndexReferences refs;
169  for (int c = 0; c < model_proto.constraints_size(); ++c) {
170  const ConstraintProto& ct = model_proto.constraints(c);
172  for (const int ref : refs.variables) {
173  used_variables.insert(PositiveRef(ref));
174  }
175  }
176 
177  // Add the objectives and search heuristics variables that needs to be
178  // referenceable as integer even if they are only used as Booleans.
179  if (model_proto.has_objective()) {
180  for (const int obj_var : model_proto.objective().vars()) {
181  used_variables.insert(PositiveRef(obj_var));
182  }
183  }
184  for (const DecisionStrategyProto& strategy :
185  model_proto.search_strategy()) {
186  for (const int var : strategy.variables()) {
187  used_variables.insert(PositiveRef(var));
188  }
189  }
190 
191  // Make sure any unused variable, that is not already a Boolean is
192  // considered "used".
193  for (int i = 0; i < num_proto_variables; ++i) {
194  if (booleans_[i] == kNoBooleanVariable) {
195  used_variables.insert(i);
196  }
197  }
198 
199  // We want the variable in the problem order.
200  var_to_instantiate_as_integer.assign(used_variables.begin(),
201  used_variables.end());
202  gtl::STLSortAndRemoveDuplicates(&var_to_instantiate_as_integer);
203  }
204  integers_.resize(num_proto_variables, kNoIntegerVariable);
205 
206  auto* integer_trail = m->GetOrCreate<IntegerTrail>();
207  integer_trail->ReserveSpaceForNumVariables(
208  var_to_instantiate_as_integer.size());
209  reverse_integer_map_.resize(2 * var_to_instantiate_as_integer.size(), -1);
210  for (const int i : var_to_instantiate_as_integer) {
211  const auto& var_proto = model_proto.variables(i);
212  integers_[i] =
213  integer_trail->AddIntegerVariable(ReadDomainFromProto(var_proto));
214  DCHECK_LT(integers_[i], reverse_integer_map_.size());
215  reverse_integer_map_[integers_[i]] = i;
216  }
217 
218  auto* encoder = m->GetOrCreate<IntegerEncoder>();
219  auto* intervals_repository = m->GetOrCreate<IntervalsRepository>();
220 
221  // Link any variable that has both views.
222  for (int i = 0; i < num_proto_variables; ++i) {
223  if (integers_[i] == kNoIntegerVariable) continue;
224  if (booleans_[i] == kNoBooleanVariable) continue;
225 
226  // Associate with corresponding integer variable.
227  encoder->AssociateToIntegerEqualValue(sat::Literal(booleans_[i], true),
228  integers_[i], IntegerValue(1));
229  }
230 
231  // Create the interval variables.
232  intervals_.resize(model_proto.constraints_size(), kNoIntervalVariable);
233  for (int c = 0; c < model_proto.constraints_size(); ++c) {
234  const ConstraintProto& ct = model_proto.constraints(c);
235  if (ct.constraint_case() != ConstraintProto::ConstraintCase::kInterval) {
236  continue;
237  }
238  if (HasEnforcementLiteral(ct)) {
239  const sat::Literal enforcement_literal =
240  Literal(ct.enforcement_literal(0));
241  // TODO(user): Fix the constant variable situation. An optional interval
242  // with constant start/end or size cannot share the same constant
243  // variable if it is used in non-optional situation.
244  if (ct.interval().has_start_view()) {
245  intervals_[c] = intervals_repository->CreateInterval(
246  LoadAffineView(ct.interval().start_view()),
247  LoadAffineView(ct.interval().end_view()),
248  LoadAffineView(ct.interval().size_view()),
249  enforcement_literal.Index(),
250  /*add_linear_relation=*/false);
251  } else {
252  intervals_[c] = m->Add(NewOptionalInterval(
253  Integer(ct.interval().start()), Integer(ct.interval().end()),
254  Integer(ct.interval().size()), enforcement_literal));
255  }
256  } else {
257  if (ct.interval().has_start_view()) {
258  intervals_[c] = intervals_repository->CreateInterval(
259  LoadAffineView(ct.interval().start_view()),
260  LoadAffineView(ct.interval().end_view()),
261  LoadAffineView(ct.interval().size_view()), kNoLiteralIndex,
262  /*add_linear_relation=*/false);
263  } else {
264  intervals_[c] = m->Add(NewInterval(Integer(ct.interval().start()),
265  Integer(ct.interval().end()),
266  Integer(ct.interval().size())));
267  }
268  }
269  already_loaded_ct_.insert(&ct);
270  }
271 }
272 
274  Model* m) {
275  const SatParameters& params = *m->GetOrCreate<SatParameters>();
276  const SymmetryProto symmetry = model_proto.symmetry();
277  if (symmetry.permutations().empty()) return;
278 
279  auto* sat_solver = m->GetOrCreate<SatSolver>();
280  auto* symmetry_handler = m->GetOrCreate<SymmetryPropagator>();
281  sat_solver->AddPropagator(symmetry_handler);
282  const int num_literals = 2 * sat_solver->NumVariables();
283 
284  for (const SparsePermutationProto& perm : symmetry.permutations()) {
285  bool all_bool = true;
286  for (const int var : perm.support()) {
287  if (!IsBoolean(var)) {
288  all_bool = false;
289  break;
290  }
291  }
292  if (!all_bool) continue;
293 
294  // Convert the variable symmetry to a "literal" one.
295  auto literal_permutation =
296  absl::make_unique<SparsePermutation>(num_literals);
297  int support_index = 0;
298  const int num_cycle = perm.cycle_sizes().size();
299  for (int i = 0; i < num_cycle; ++i) {
300  const int size = perm.cycle_sizes(i);
301  const int saved_support_index = support_index;
302  for (int j = 0; j < size; ++j) {
303  const int var = perm.support(support_index++);
304  literal_permutation->AddToCurrentCycle(Literal(var).Index().value());
305  }
306  literal_permutation->CloseCurrentCycle();
307 
308  // Note that we also need to add the corresponding cycle for the negated
309  // literals.
310  support_index = saved_support_index;
311  for (int j = 0; j < size; ++j) {
312  const int var = perm.support(support_index++);
313  literal_permutation->AddToCurrentCycle(
314  Literal(var).NegatedIndex().value());
315  }
316  literal_permutation->CloseCurrentCycle();
317  }
318  symmetry_handler->AddSymmetry(std::move(literal_permutation));
319  }
320 
321  const bool log_info = VLOG_IS_ON(1) || params.log_search_progress();
322  if (log_info) {
323  LOG(INFO) << "Added " << symmetry_handler->num_permutations()
324  << " symmetry to the SAT solver.";
325  }
326 }
327 
328 // The logic assumes that the linear constraints have been presolved, so that
329 // equality with a domain bound have been converted to <= or >= and so that we
330 // never have any trivial inequalities.
331 //
332 // TODO(user): Regroup/presolve two encoding like b => x > 2 and the same
333 // Boolean b => x > 5. These shouldn't happen if we merge linear constraints.
335  Model* m) {
336  auto* encoder = m->GetOrCreate<IntegerEncoder>();
337  auto* integer_trail = m->GetOrCreate<IntegerTrail>();
338  auto* sat_solver = m->GetOrCreate<SatSolver>();
339 
340  // TODO(user): Debug what makes it unsat at this point.
341  if (sat_solver->IsModelUnsat()) return;
342 
343  // Detection of literal equivalent to (i_var == value). We collect all the
344  // half-reified constraint lit => equality or lit => inequality for a given
345  // variable, and we will later sort them to detect equivalence.
346  struct EqualityDetectionHelper {
347  const ConstraintProto* ct;
349  int64 value;
350  bool is_equality; // false if != instead.
351 
352  bool operator<(const EqualityDetectionHelper& o) const {
353  if (literal.Variable() == o.literal.Variable()) {
354  if (value == o.value) return is_equality && !o.is_equality;
355  return value < o.value;
356  }
357  return literal.Variable() < o.literal.Variable();
358  }
359  };
360  std::vector<std::vector<EqualityDetectionHelper>> var_to_equalities(
361  model_proto.variables_size());
362 
363  // TODO(user): We will re-add the same implied bounds during probing, so
364  // it might not be necessary to do that here. Also, it might be too early
365  // if some of the literal view used in the LP are created later, but that
366  // should be fixable via calls to implied_bounds->NotifyNewIntegerView().
367  auto* implied_bounds = m->GetOrCreate<ImpliedBounds>();
368 
369  // Detection of literal equivalent to (i_var >= bound). We also collect
370  // all the half-refied part and we will sort the vector for detection of the
371  // equivalence.
372  struct InequalityDetectionHelper {
373  const ConstraintProto* ct;
375  IntegerLiteral i_lit;
376 
377  bool operator<(const InequalityDetectionHelper& o) const {
378  if (literal.Variable() == o.literal.Variable()) {
379  return i_lit.var < o.i_lit.var;
380  }
381  return literal.Variable() < o.literal.Variable();
382  }
383  };
384  std::vector<InequalityDetectionHelper> inequalities;
385 
386  // Loop over all contraints and fill var_to_equalities and inequalities.
387  for (const ConstraintProto& ct : model_proto.constraints()) {
388  if (ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
389  continue;
390  }
391  if (ct.enforcement_literal().size() != 1) continue;
392  if (ct.linear().vars_size() != 1) continue;
393 
394  // ct is a linear constraint with one term and one enforcement literal.
395  const sat::Literal enforcement_literal = Literal(ct.enforcement_literal(0));
396  const int ref = ct.linear().vars(0);
397  const int var = PositiveRef(ref);
398 
399  const Domain domain = ReadDomainFromProto(model_proto.variables(var));
400  const Domain domain_if_enforced =
401  ReadDomainFromProto(ct.linear())
402  .InverseMultiplicationBy(ct.linear().coeffs(0) *
403  (RefIsPositive(ref) ? 1 : -1));
404 
405  // Detect enforcement_literal => (var >= value or var <= value).
406  if (domain_if_enforced.NumIntervals() == 1) {
407  if (domain_if_enforced.Max() >= domain.Max() &&
408  domain_if_enforced.Min() > domain.Min()) {
409  inequalities.push_back(
410  {&ct, enforcement_literal,
412  Integer(var), IntegerValue(domain_if_enforced.Min()))});
413  implied_bounds->Add(enforcement_literal, inequalities.back().i_lit);
414  } else if (domain_if_enforced.Min() <= domain.Min() &&
415  domain_if_enforced.Max() < domain.Max()) {
416  inequalities.push_back(
417  {&ct, enforcement_literal,
419  Integer(var), IntegerValue(domain_if_enforced.Max()))});
420  implied_bounds->Add(enforcement_literal, inequalities.back().i_lit);
421  }
422  }
423 
424  // Detect enforcement_literal => (var == value or var != value).
425  //
426  // Note that for domain with 2 values like [0, 1], we will detect both ==
427  // 0 and != 1. Similarly, for a domain in [min, max], we should both
428  // detect (== min) and (<= min), and both detect (== max) and (>= max).
429  {
430  const Domain inter = domain.IntersectionWith(domain_if_enforced);
431  if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
432  var_to_equalities[var].push_back(
433  {&ct, enforcement_literal, inter.Min(), true});
434  if (domain.Contains(inter.Min())) {
435  variables_to_encoded_values_[var].insert(inter.Min());
436  }
437  }
438  }
439  {
440  const Domain inter =
441  domain.IntersectionWith(domain_if_enforced.Complement());
442  if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
443  var_to_equalities[var].push_back(
444  {&ct, enforcement_literal, inter.Min(), false});
445  if (domain.Contains(inter.Min())) {
446  variables_to_encoded_values_[var].insert(inter.Min());
447  }
448  }
449  }
450  }
451 
452  // Detect Literal <=> X >= value
453  int num_inequalities = 0;
454  std::sort(inequalities.begin(), inequalities.end());
455  for (int i = 0; i + 1 < inequalities.size(); i++) {
456  if (inequalities[i].literal != inequalities[i + 1].literal.Negated()) {
457  continue;
458  }
459 
460  // TODO(user): In these cases, we could fix the enforcement literal right
461  // away or ignore the constraint. Note that it will be done later anyway
462  // though.
463  if (integer_trail->IntegerLiteralIsTrue(inequalities[i].i_lit) ||
464  integer_trail->IntegerLiteralIsFalse(inequalities[i].i_lit)) {
465  continue;
466  }
467  if (integer_trail->IntegerLiteralIsTrue(inequalities[i + 1].i_lit) ||
468  integer_trail->IntegerLiteralIsFalse(inequalities[i + 1].i_lit)) {
469  continue;
470  }
471 
472  const auto pair_a = encoder->Canonicalize(inequalities[i].i_lit);
473  const auto pair_b = encoder->Canonicalize(inequalities[i + 1].i_lit);
474  if (pair_a.first == pair_b.second) {
475  ++num_inequalities;
476  encoder->AssociateToIntegerLiteral(inequalities[i].literal,
477  inequalities[i].i_lit);
478  already_loaded_ct_.insert(inequalities[i].ct);
479  already_loaded_ct_.insert(inequalities[i + 1].ct);
480  }
481  }
482 
483  // Encode the half-inequalities.
484  int num_half_inequalities = 0;
485  for (const auto inequality : inequalities) {
486  if (ConstraintIsAlreadyLoaded(inequality.ct)) continue;
487  m->Add(
488  Implication(inequality.literal,
489  encoder->GetOrCreateAssociatedLiteral(inequality.i_lit)));
490  if (sat_solver->IsModelUnsat()) return;
491 
492  ++num_half_inequalities;
493  already_loaded_ct_.insert(inequality.ct);
494  is_half_encoding_ct_.insert(inequality.ct);
495  }
496 
497  if (!inequalities.empty()) {
498  VLOG(1) << num_inequalities << " literals associated to VAR >= value, and "
499  << num_half_inequalities << " half-associations.";
500  }
501 
502  // Detect Literal <=> X == value and associate them in the IntegerEncoder.
503  //
504  // TODO(user): Fully encode variable that are almost fully encoded?
505  int num_constraints = 0;
506  int num_equalities = 0;
507  int num_half_equalities = 0;
508  int num_fully_encoded = 0;
509  int num_partially_encoded = 0;
510  for (int i = 0; i < var_to_equalities.size(); ++i) {
511  std::vector<EqualityDetectionHelper>& encoding = var_to_equalities[i];
512  std::sort(encoding.begin(), encoding.end());
513  if (encoding.empty()) continue;
514  num_constraints += encoding.size();
515 
516  absl::flat_hash_set<int64> values;
517  for (int j = 0; j + 1 < encoding.size(); j++) {
518  if ((encoding[j].value != encoding[j + 1].value) ||
519  (encoding[j].literal != encoding[j + 1].literal.Negated()) ||
520  (encoding[j].is_equality != true) ||
521  (encoding[j + 1].is_equality != false)) {
522  continue;
523  }
524 
525  ++num_equalities;
526  encoder->AssociateToIntegerEqualValue(encoding[j].literal, integers_[i],
527  IntegerValue(encoding[j].value));
528  already_loaded_ct_.insert(encoding[j].ct);
529  already_loaded_ct_.insert(encoding[j + 1].ct);
530  values.insert(encoding[j].value);
531  }
532 
533  // TODO(user): Try to remove it. Normally we caught UNSAT above, but
534  // tests are very flaky (it only happens in parallel). Keeping it there for
535  // the time being.
536  if (sat_solver->IsModelUnsat()) return;
537 
538  // Encode the half-equalities.
539  //
540  // TODO(user): delay this after PropagateEncodingFromEquivalenceRelations()?
541  // Otherwise we might create new Boolean variables for no reason. Note
542  // however, that in the presolve, we should only use the "representative" in
543  // linear constraints, so we should be fine.
544  for (const auto equality : encoding) {
545  if (ConstraintIsAlreadyLoaded(equality.ct)) continue;
546  const class Literal eq = encoder->GetOrCreateLiteralAssociatedToEquality(
547  integers_[i], IntegerValue(equality.value));
548  if (equality.is_equality) {
549  m->Add(Implication(equality.literal, eq));
550  } else {
551  m->Add(Implication(equality.literal, eq.Negated()));
552  }
553 
554  ++num_half_equalities;
555  already_loaded_ct_.insert(equality.ct);
556  is_half_encoding_ct_.insert(equality.ct);
557  }
558 
559  // Update stats.
560  if (VLOG_IS_ON(1)) {
561  if (encoder->VariableIsFullyEncoded(integers_[i])) {
562  ++num_fully_encoded;
563  } else {
564  ++num_partially_encoded;
565  }
566  }
567  }
568 
569  if (num_constraints > 0) {
570  VLOG(1) << num_equalities << " literals associated to VAR == value, and "
571  << num_half_equalities << " half-associations.";
572  }
573  if (num_fully_encoded > 0) {
574  VLOG(1) << "num_fully_encoded_variables: " << num_fully_encoded;
575  }
576  if (num_partially_encoded > 0) {
577  VLOG(1) << "num_partially_encoded_variables: " << num_partially_encoded;
578  }
579 }
580 
582  const CpModelProto& model_proto, Model* m) {
583  auto* encoder = m->GetOrCreate<IntegerEncoder>();
584  auto* sat_solver = m->GetOrCreate<SatSolver>();
585 
586  // Loop over all contraints and find affine ones.
587  int64 num_associations = 0;
588  int64 num_set_to_false = 0;
589  for (const ConstraintProto& ct : model_proto.constraints()) {
590  if (!ct.enforcement_literal().empty()) continue;
591  if (ct.constraint_case() != ConstraintProto::kLinear) continue;
592  if (ct.linear().vars_size() != 2) continue;
593  if (!ConstraintIsEq(ct.linear())) continue;
594 
595  const IntegerValue rhs(ct.linear().domain(0));
596 
597  // Make sure the coefficient are positive.
598  IntegerVariable var1 = Integer(ct.linear().vars(0));
599  IntegerVariable var2 = Integer(ct.linear().vars(1));
600  IntegerValue coeff1(ct.linear().coeffs(0));
601  IntegerValue coeff2(ct.linear().coeffs(1));
602  if (coeff1 < 0) {
603  var1 = NegationOf(var1);
604  coeff1 = -coeff1;
605  }
606  if (coeff2 < 0) {
607  var2 = NegationOf(var2);
608  coeff2 = -coeff2;
609  }
610 
611  // TODO(user): This is not supposed to happen, but apparently it did on
612  // once on routing_GCM_0001_sat.fzn. Investigate and fix.
613  if (coeff1 == 0 || coeff2 == 0) continue;
614 
615  // We first map the >= literals.
616  // It is important to do that first, since otherwise mapping a == literal
617  // might creates the underlying >= and <= literals.
618  for (int i = 0; i < 2; ++i) {
619  for (const auto value_literal :
620  encoder->PartialGreaterThanEncoding(var1)) {
621  const IntegerValue value1 = value_literal.first;
622  const IntegerValue bound2 = FloorRatio(rhs - value1 * coeff1, coeff2);
623  ++num_associations;
624  encoder->AssociateToIntegerLiteral(
625  value_literal.second, IntegerLiteral::LowerOrEqual(var2, bound2));
626  }
627  std::swap(var1, var2);
628  std::swap(coeff1, coeff2);
629  }
630 
631  // Same for the == literals.
632  //
633  // TODO(user): This is similar to LoadEquivalenceAC() for unreified
634  // constraints, but when the later is called, more encoding might have taken
635  // place.
636  for (int i = 0; i < 2; ++i) {
637  for (const auto value_literal : encoder->PartialDomainEncoding(var1)) {
638  const IntegerValue value1 = value_literal.value;
639  const IntegerValue intermediate = rhs - value1 * coeff1;
640  if (intermediate % coeff2 != 0) {
641  // Using this function deals properly with UNSAT.
642  ++num_set_to_false;
643  sat_solver->AddUnitClause(value_literal.literal.Negated());
644  continue;
645  }
646  ++num_associations;
647  encoder->AssociateToIntegerEqualValue(value_literal.literal, var2,
648  intermediate / coeff2);
649  }
650  std::swap(var1, var2);
651  std::swap(coeff1, coeff2);
652  }
653  }
654 
655  if (num_associations > 0) {
656  VLOG(1) << "Num associations from equivalences = " << num_associations;
657  }
658  if (num_set_to_false > 0) {
659  VLOG(1) << "Num literals set to false from equivalences = "
660  << num_set_to_false;
661  }
662 }
663 
665  Model* m) {
666  const SatParameters& parameters = *(m->GetOrCreate<SatParameters>());
667  if (!parameters.use_optional_variables()) return;
668  if (parameters.enumerate_all_solutions()) return;
669 
670  // The variables from the objective cannot be marked as optional!
671  const int num_proto_variables = model_proto.variables_size();
672  std::vector<bool> already_seen(num_proto_variables, false);
673  if (model_proto.has_objective()) {
674  for (const int ref : model_proto.objective().vars()) {
675  already_seen[PositiveRef(ref)] = true;
676  }
677  }
678 
679  // Compute for each variables the intersection of the enforcement literals
680  // of the constraints in which they appear.
681  //
682  // TODO(user): This deals with the simplest cases, but we could try to
683  // detect literals that implies all the constaints in which a variable
684  // appear to false. This can be done with a LCA computation in the tree of
685  // Boolean implication (once the presolve remove cycles). Not sure if we can
686  // properly exploit that afterwards though. Do some research!
687  std::vector<std::vector<int>> enforcement_intersection(num_proto_variables);
688  std::set<int> literals_set;
689  for (int c = 0; c < model_proto.constraints_size(); ++c) {
690  const ConstraintProto& ct = model_proto.constraints(c);
691  if (ct.enforcement_literal().empty()) {
692  for (const int var : UsedVariables(ct)) {
693  already_seen[var] = true;
694  enforcement_intersection[var].clear();
695  }
696  } else {
697  literals_set.clear();
698  literals_set.insert(ct.enforcement_literal().begin(),
699  ct.enforcement_literal().end());
700  for (const int var : UsedVariables(ct)) {
701  if (!already_seen[var]) {
702  enforcement_intersection[var].assign(ct.enforcement_literal().begin(),
703  ct.enforcement_literal().end());
704  } else {
705  // Take the intersection.
706  std::vector<int>& vector_ref = enforcement_intersection[var];
707  int new_size = 0;
708  for (const int literal : vector_ref) {
709  if (gtl::ContainsKey(literals_set, literal)) {
710  vector_ref[new_size++] = literal;
711  }
712  }
713  vector_ref.resize(new_size);
714  }
715  already_seen[var] = true;
716  }
717  }
718  }
719 
720  // Auto-detect optional variables.
721  int num_optionals = 0;
722  auto* integer_trail = m->GetOrCreate<IntegerTrail>();
723  for (int var = 0; var < num_proto_variables; ++var) {
724  const IntegerVariableProto& var_proto = model_proto.variables(var);
725  const int64 min = var_proto.domain(0);
726  const int64 max = var_proto.domain(var_proto.domain().size() - 1);
727  if (min == max) continue;
728  if (min == 0 && max == 1) continue;
729  if (enforcement_intersection[var].empty()) continue;
730 
731  ++num_optionals;
732  integer_trail->MarkIntegerVariableAsOptional(
733  Integer(var), Literal(enforcement_intersection[var].front()));
734  }
735  VLOG(2) << "Auto-detected " << num_optionals << " optional variables.";
736 }
737 
738 // ============================================================================
739 // A class that detects when variables should be fully encoded by computing a
740 // fixed point. It also fully encodes such variables.
741 // ============================================================================
742 
744  public:
746  : model_proto_(model_proto),
747  parameters_(*(model->GetOrCreate<SatParameters>())),
748  model_(model),
749  mapping_(model->GetOrCreate<CpModelMapping>()),
750  integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
751  integer_trail_(model->GetOrCreate<IntegerTrail>()) {}
752 
753  void ComputeFixedPoint();
754 
755  private:
756  DEFINE_INT_TYPE(ConstraintIndex, int32);
757 
758  // Constraint ct is interested by (full-encoding) state of variable.
759  void Register(ConstraintIndex ct_index, int variable) {
760  variable = PositiveRef(variable);
761  constraint_is_registered_[ct_index] = true;
762  if (variable_watchers_.size() <= variable) {
763  variable_watchers_.resize(variable + 1);
764  variable_was_added_in_to_propagate_.resize(variable + 1);
765  }
766  variable_watchers_[variable].push_back(ct_index);
767  }
768 
769  void AddVariableToPropagationQueue(int variable) {
770  variable = PositiveRef(variable);
771  if (variable_was_added_in_to_propagate_.size() <= variable) {
772  variable_watchers_.resize(variable + 1);
773  variable_was_added_in_to_propagate_.resize(variable + 1);
774  }
775  if (!variable_was_added_in_to_propagate_[variable]) {
776  variable_was_added_in_to_propagate_[variable] = true;
777  variables_to_propagate_.push_back(variable);
778  }
779  }
780 
781  // Note that we always consider a fixed variable to be fully encoded here.
782  const bool IsFullyEncoded(int v) {
783  const IntegerVariable variable = mapping_->Integer(v);
784  if (v == kNoIntegerVariable) return false;
785  return integer_trail_->IsFixed(variable) ||
786  integer_encoder_->VariableIsFullyEncoded(variable);
787  }
788 
789  const bool VariableIsFixed(int v) {
790  const IntegerVariable variable = mapping_->Integer(v);
791  if (v == kNoIntegerVariable) return false;
792  return integer_trail_->IsFixed(variable);
793  }
794 
795  void FullyEncode(int v) {
796  v = PositiveRef(v);
797  const IntegerVariable variable = mapping_->Integer(v);
798  if (v == kNoIntegerVariable) return;
799  if (!integer_trail_->IsFixed(variable)) {
800  model_->Add(FullyEncodeVariable(variable));
801  }
802  AddVariableToPropagationQueue(v);
803  }
804 
805  bool ProcessConstraint(ConstraintIndex ct_index);
806  bool ProcessElement(ConstraintIndex ct_index);
807  bool ProcessTable(ConstraintIndex ct_index);
808  bool ProcessAutomaton(ConstraintIndex ct_index);
809  bool ProcessLinear(ConstraintIndex ct_index);
810 
811  const CpModelProto& model_proto_;
812  const SatParameters& parameters_;
813 
814  Model* model_;
815  CpModelMapping* mapping_;
816  IntegerEncoder* integer_encoder_;
817  IntegerTrail* integer_trail_;
818 
819  std::vector<bool> variable_was_added_in_to_propagate_;
820  std::vector<int> variables_to_propagate_;
821  std::vector<std::vector<ConstraintIndex>> variable_watchers_;
822 
823  absl::StrongVector<ConstraintIndex, bool> constraint_is_finished_;
824  absl::StrongVector<ConstraintIndex, bool> constraint_is_registered_;
825 
826  absl::flat_hash_map<int, absl::flat_hash_set<int>>
827  variables_to_equal_or_diff_variables_;
828 };
829 
830 // We only add to the propagation queue variable that are fully encoded.
831 // Note that if a variable was already added once, we never add it again.
833  const int num_constraints = model_proto_.constraints_size();
834  const int num_vars = model_proto_.variables_size();
835  constraint_is_finished_.assign(num_constraints, false);
836  constraint_is_registered_.assign(num_constraints, false);
837 
838  // Process all constraint once.
839  for (ConstraintIndex ct_index(0); ct_index < num_constraints; ++ct_index) {
840  constraint_is_finished_[ct_index] = ProcessConstraint(ct_index);
841  }
842 
843  // We run a heuristics to decide if we want to fully encode a variable or not.
844  // We decide to fully encode a variable if:
845  // - a variable appears in enough a1 * x1 + a2 + x2 ==/!= value and the
846  // domain is small.
847  // - the number of values that appears in b => x ==/!= value that are not
848  // the bounds of the variables is more that half the size of the domain.
849  // . - the size of the domain is > 2
850  int num_variables_fully_encoded_by_heuristics = 0;
851  for (int var = 0; var < num_vars; ++var) {
852  if (!mapping_->IsInteger(var) || IsFullyEncoded(var)) continue;
853  const IntegerVariableProto& int_var_proto = model_proto_.variables(var);
854  const Domain domain = ReadDomainFromProto(int_var_proto);
855  int64 domain_size = domain.Size();
856  int64 num_diff_or_equal_var_constraints = 0;
857  int64 num_potential_encoded_values_without_bounds = 0;
858 
859  if (domain_size <= 2) continue;
860 
861  const absl::flat_hash_set<int64>& value_set =
862  mapping_->PotentialEncodedValues(var);
863  for (const int value : value_set) {
864  if (value > domain.Min() && value < domain.Max() &&
865  domain.Contains(value)) {
866  num_potential_encoded_values_without_bounds++;
867  }
868  }
869 
870  const auto& it = variables_to_equal_or_diff_variables_.find(var);
871  if (it != variables_to_equal_or_diff_variables_.end()) {
872  num_diff_or_equal_var_constraints = it->second.size();
873  }
874 
875  if (num_potential_encoded_values_without_bounds >= domain_size / 2 ||
876  (num_diff_or_equal_var_constraints >= domain_size / 2 &&
877  domain_size < 16)) {
878  VLOG(3) << model_proto_.variables(var).ShortDebugString()
879  << " is encoded with "
880  << num_potential_encoded_values_without_bounds
881  << " unary constraints, and " << num_diff_or_equal_var_constraints
882  << " binary constraints on a domain of size " << domain_size;
883  FullyEncode(var);
884  num_variables_fully_encoded_by_heuristics++;
885  }
886  }
887  if (num_variables_fully_encoded_by_heuristics > 0) {
888  VLOG(2) << num_variables_fully_encoded_by_heuristics
889  << " variables fully encoded after model introspection.";
890  }
891 
892  // Make sure all fully encoded variables of interest are in the queue.
893  for (int v = 0; v < variable_watchers_.size(); v++) {
894  if (!variable_watchers_[v].empty() && IsFullyEncoded(v)) {
895  AddVariableToPropagationQueue(v);
896  }
897  }
898 
899  // Loop until no additional variable can be fully encoded.
900  while (!variables_to_propagate_.empty()) {
901  const int variable = variables_to_propagate_.back();
902  variables_to_propagate_.pop_back();
903  for (const ConstraintIndex ct_index : variable_watchers_[variable]) {
904  if (constraint_is_finished_[ct_index]) continue;
905  constraint_is_finished_[ct_index] = ProcessConstraint(ct_index);
906  }
907  }
908 }
909 
910 // Returns true if the constraint has finished encoding what it wants.
911 bool FullEncodingFixedPointComputer::ProcessConstraint(
912  ConstraintIndex ct_index) {
913  const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
914  switch (ct.constraint_case()) {
915  case ConstraintProto::ConstraintProto::kElement:
916  return ProcessElement(ct_index);
917  case ConstraintProto::ConstraintProto::kTable:
918  return ProcessTable(ct_index);
919  case ConstraintProto::ConstraintProto::kAutomaton:
920  return ProcessAutomaton(ct_index);
921  case ConstraintProto::ConstraintProto::kLinear:
922  return ProcessLinear(ct_index);
923  default:
924  return true;
925  }
926 }
927 
928 bool FullEncodingFixedPointComputer::ProcessElement(ConstraintIndex ct_index) {
929  const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
930 
931  // Index must always be full encoded.
932  FullyEncode(ct.element().index());
933 
934  const int target = ct.element().target();
935 
936  // If target is fixed, do not encode variables.
937  if (VariableIsFixed(target)) return true;
938 
939  // If target is a constant or fully encoded, variables must be fully encoded.
940  if (IsFullyEncoded(target)) {
941  for (const int v : ct.element().vars()) FullyEncode(v);
942  }
943 
944  // If all non-target variables are fully encoded, target must be too.
945  bool all_variables_are_fully_encoded = true;
946  for (const int v : ct.element().vars()) {
947  if (v == target) continue;
948  if (!IsFullyEncoded(v)) {
949  all_variables_are_fully_encoded = false;
950  break;
951  }
952  }
953  if (all_variables_are_fully_encoded) {
954  if (!IsFullyEncoded(target)) FullyEncode(target);
955  return true;
956  }
957 
958  // If some variables are not fully encoded, register on those.
959  if (constraint_is_registered_[ct_index]) {
960  for (const int v : ct.element().vars()) Register(ct_index, v);
961  Register(ct_index, target);
962  }
963  return false;
964 }
965 
966 bool FullEncodingFixedPointComputer::ProcessTable(ConstraintIndex ct_index) {
967  const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
968 
969  if (ct.table().negated()) return true;
970 
971  for (const int variable : ct.table().vars()) {
972  FullyEncode(variable);
973  }
974 
975  return true;
976 }
977 
978 bool FullEncodingFixedPointComputer::ProcessAutomaton(
979  ConstraintIndex ct_index) {
980  const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
981  for (const int variable : ct.automaton().vars()) {
982  FullyEncode(variable);
983  }
984  return true;
985 }
986 
987 bool FullEncodingFixedPointComputer::ProcessLinear(ConstraintIndex ct_index) {
988  // We are only interested in linear equations of the form:
989  // [b =>] a1 * x1 + a2 * x2 ==|!= value
990  const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
991  if (parameters_.boolean_encoding_level() == 0 ||
992  ct.linear().vars_size() != 2) {
993  return true;
994  }
995 
996  if (!ConstraintIsEq(ct.linear()) &&
997  !ConstraintIsNEq(ct.linear(), mapping_, integer_trail_, nullptr)) {
998  return true;
999  }
1000 
1001  const int var0 = ct.linear().vars(0);
1002  const int var1 = ct.linear().vars(1);
1003  if (!IsFullyEncoded(var0)) {
1004  variables_to_equal_or_diff_variables_[var0].insert(var1);
1005  }
1006  if (!IsFullyEncoded(var1)) {
1007  variables_to_equal_or_diff_variables_[var1].insert(var0);
1008  }
1009  return true;
1010 }
1011 
1012 void MaybeFullyEncodeMoreVariables(const CpModelProto& model_proto, Model* m) {
1014  fixpoint.ComputeFixedPoint();
1015 }
1016 
1017 // ============================================================================
1018 // Constraint loading functions.
1019 // ============================================================================
1020 
1021 void LoadBoolOrConstraint(const ConstraintProto& ct, Model* m) {
1022  auto* mapping = m->GetOrCreate<CpModelMapping>();
1023  std::vector<Literal> literals = mapping->Literals(ct.bool_or().literals());
1024  for (const int ref : ct.enforcement_literal()) {
1025  literals.push_back(mapping->Literal(ref).Negated());
1026  }
1027  m->Add(ClauseConstraint(literals));
1028 }
1029 
1030 void LoadBoolAndConstraint(const ConstraintProto& ct, Model* m) {
1031  auto* mapping = m->GetOrCreate<CpModelMapping>();
1032  std::vector<Literal> literals;
1033  for (const int ref : ct.enforcement_literal()) {
1034  literals.push_back(mapping->Literal(ref).Negated());
1035  }
1036  auto* sat_solver = m->GetOrCreate<SatSolver>();
1037  for (const Literal literal : mapping->Literals(ct.bool_and().literals())) {
1038  literals.push_back(literal);
1039  sat_solver->AddProblemClause(literals);
1040  literals.pop_back();
1041  }
1042 }
1043 
1044 void LoadAtMostOneConstraint(const ConstraintProto& ct, Model* m) {
1045  auto* mapping = m->GetOrCreate<CpModelMapping>();
1046  CHECK(!HasEnforcementLiteral(ct)) << "Not supported.";
1047  m->Add(AtMostOneConstraint(mapping->Literals(ct.at_most_one().literals())));
1048 }
1049 
1050 void LoadExactlyOneConstraint(const ConstraintProto& ct, Model* m) {
1051  auto* mapping = m->GetOrCreate<CpModelMapping>();
1052  CHECK(!HasEnforcementLiteral(ct)) << "Not supported.";
1053  m->Add(ExactlyOneConstraint(mapping->Literals(ct.exactly_one().literals())));
1054 }
1055 
1056 void LoadBoolXorConstraint(const ConstraintProto& ct, Model* m) {
1057  auto* mapping = m->GetOrCreate<CpModelMapping>();
1058  CHECK(!HasEnforcementLiteral(ct)) << "Not supported.";
1059  m->Add(LiteralXorIs(mapping->Literals(ct.bool_xor().literals()), true));
1060 }
1061 
1062 namespace {
1063 
1064 // Boolean encoding of:
1065 // enforcement_literal => coeff1 * var1 + coeff2 * var2 == rhs;
1066 void LoadEquivalenceAC(const std::vector<Literal> enforcement_literal,
1067  IntegerValue coeff1, IntegerVariable var1,
1068  IntegerValue coeff2, IntegerVariable var2,
1069  const IntegerValue rhs, Model* m) {
1070  auto* encoder = m->GetOrCreate<IntegerEncoder>();
1071  CHECK(encoder->VariableIsFullyEncoded(var1));
1072  CHECK(encoder->VariableIsFullyEncoded(var2));
1073  absl::flat_hash_map<IntegerValue, Literal> term1_value_to_literal;
1074  for (const auto value_literal : encoder->FullDomainEncoding(var1)) {
1075  term1_value_to_literal[coeff1 * value_literal.value] =
1076  value_literal.literal;
1077  }
1078  for (const auto value_literal : encoder->FullDomainEncoding(var2)) {
1079  const IntegerValue target = rhs - value_literal.value * coeff2;
1080  if (!gtl::ContainsKey(term1_value_to_literal, target)) {
1081  m->Add(EnforcedClause(enforcement_literal,
1082  {value_literal.literal.Negated()}));
1083  } else {
1084  const Literal target_literal = term1_value_to_literal[target];
1085  m->Add(EnforcedClause(enforcement_literal,
1086  {value_literal.literal.Negated(), target_literal}));
1087  m->Add(EnforcedClause(enforcement_literal,
1088  {value_literal.literal, target_literal.Negated()}));
1089 
1090  // This "target" can never be reached again, so it is safe to remove it.
1091  // We do that so we know the term1 values that are never reached.
1092  term1_value_to_literal.erase(target);
1093  }
1094  }
1095 
1096  // Exclude the values that can never be "matched" by coeff2 * var2.
1097  // We need the std::sort() to be deterministic!
1098  std::vector<Literal> implied_false;
1099  for (const auto entry : term1_value_to_literal) {
1100  implied_false.push_back(entry.second);
1101  }
1102  std::sort(implied_false.begin(), implied_false.end());
1103  for (const Literal l : implied_false) {
1104  m->Add(EnforcedClause(enforcement_literal, {l.Negated()}));
1105  }
1106 }
1107 
1108 // Boolean encoding of:
1109 // enforcement_literal => coeff1 * var1 + coeff2 * var2 != rhs;
1110 void LoadEquivalenceNeqAC(const std::vector<Literal> enforcement_literal,
1111  IntegerValue coeff1, IntegerVariable var1,
1112  IntegerValue coeff2, IntegerVariable var2,
1113  const IntegerValue rhs, Model* m) {
1114  auto* encoder = m->GetOrCreate<IntegerEncoder>();
1115  CHECK(encoder->VariableIsFullyEncoded(var1));
1116  CHECK(encoder->VariableIsFullyEncoded(var2));
1117  absl::flat_hash_map<IntegerValue, Literal> term1_value_to_literal;
1118  for (const auto value_literal : encoder->FullDomainEncoding(var1)) {
1119  term1_value_to_literal[coeff1 * value_literal.value] =
1120  value_literal.literal;
1121  }
1122  for (const auto value_literal : encoder->FullDomainEncoding(var2)) {
1123  const IntegerValue target_value = rhs - value_literal.value * coeff2;
1124  const auto& it = term1_value_to_literal.find(target_value);
1125  if (it != term1_value_to_literal.end()) {
1126  const Literal target_literal = it->second;
1127  m->Add(EnforcedClause(
1128  enforcement_literal,
1129  {value_literal.literal.Negated(), target_literal.Negated()}));
1130  }
1131  }
1132 }
1133 
1134 } // namespace
1135 
1136 void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
1137  auto* mapping = m->GetOrCreate<CpModelMapping>();
1138  if (ct.linear().vars().empty()) {
1139  const Domain rhs = ReadDomainFromProto(ct.linear());
1140  if (rhs.Contains(0)) return;
1141  if (HasEnforcementLiteral(ct)) {
1142  std::vector<Literal> clause;
1143  for (const int ref : ct.enforcement_literal()) {
1144  clause.push_back(mapping->Literal(ref).Negated());
1145  }
1146  m->Add(ClauseConstraint(clause));
1147  } else {
1148  VLOG(1) << "Trivially UNSAT constraint: " << ct.DebugString();
1149  m->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1150  }
1151  return;
1152  }
1153 
1154  auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1155  const std::vector<IntegerVariable> vars =
1156  mapping->Integers(ct.linear().vars());
1157  const std::vector<int64> coeffs = ValuesFromProto(ct.linear().coeffs());
1158 
1159  // Compute the min/max to relax the bounds if needed.
1160  //
1161  // TODO(user): Reuse ComputeLinearBounds()? but then we need another loop
1162  // to detect if we only have Booleans.
1163  IntegerValue min_sum(0);
1164  IntegerValue max_sum(0);
1165  IntegerValue max_domain_size(0);
1166  bool all_booleans = true;
1167  for (int i = 0; i < vars.size(); ++i) {
1168  if (all_booleans && !mapping->IsBoolean(ct.linear().vars(i))) {
1169  all_booleans = false;
1170  }
1171  const IntegerValue lb = integer_trail->LowerBound(vars[i]);
1172  const IntegerValue ub = integer_trail->UpperBound(vars[i]);
1173  max_domain_size = std::max(max_domain_size, ub - lb + 1);
1174  const IntegerValue term_a = coeffs[i] * lb;
1175  const IntegerValue term_b = coeffs[i] * ub;
1176  min_sum += std::min(term_a, term_b);
1177  max_sum += std::max(term_a, term_b);
1178  }
1179 
1180  if (ct.linear().vars_size() == 2 && !integer_trail->IsFixed(vars[0]) &&
1181  !integer_trail->IsFixed(vars[1]) && max_domain_size < 16) {
1182  const SatParameters& params = *m->GetOrCreate<SatParameters>();
1183  auto* encoder = m->GetOrCreate<IntegerEncoder>();
1184  if (params.boolean_encoding_level() > 0 && ConstraintIsEq(ct.linear()) &&
1185  ct.linear().domain(0) != min_sum && ct.linear().domain(0) != max_sum &&
1186  encoder->VariableIsFullyEncoded(vars[0]) &&
1187  encoder->VariableIsFullyEncoded(vars[1])) {
1188  VLOG(3) << "Load AC version of " << ct.DebugString() << ", var0 domain = "
1189  << integer_trail->InitialVariableDomain(vars[0])
1190  << ", var1 domain = "
1191  << integer_trail->InitialVariableDomain(vars[1]);
1192  return LoadEquivalenceAC(mapping->Literals(ct.enforcement_literal()),
1193  IntegerValue(coeffs[0]), vars[0],
1194  IntegerValue(coeffs[1]), vars[1],
1195  IntegerValue(ct.linear().domain(0)), m);
1196  }
1197 
1198  int64 single_value = 0;
1199  if (params.boolean_encoding_level() > 0 &&
1200  ConstraintIsNEq(ct.linear(), mapping, integer_trail, &single_value) &&
1201  single_value != min_sum && single_value != max_sum &&
1202  encoder->VariableIsFullyEncoded(vars[0]) &&
1203  encoder->VariableIsFullyEncoded(vars[1])) {
1204  VLOG(3) << "Load NAC version of " << ct.DebugString()
1205  << ", var0 domain = "
1206  << integer_trail->InitialVariableDomain(vars[0])
1207  << ", var1 domain = "
1208  << integer_trail->InitialVariableDomain(vars[1])
1209  << ", value = " << single_value;
1210  return LoadEquivalenceNeqAC(mapping->Literals(ct.enforcement_literal()),
1211  IntegerValue(coeffs[0]), vars[0],
1212  IntegerValue(coeffs[1]), vars[1],
1213  IntegerValue(single_value), m);
1214  }
1215  }
1216 
1217  if (ct.linear().domain_size() == 2) {
1218  int64 lb = ct.linear().domain(0);
1219  int64 ub = ct.linear().domain(1);
1220  if (min_sum >= lb) lb = kint64min;
1221  if (max_sum <= ub) ub = kint64max;
1222 
1223  if (!HasEnforcementLiteral(ct)) {
1224  if (all_booleans) {
1225  // TODO(user): we should probably also implement an
1226  // half-reified version of this constraint.
1227  std::vector<LiteralWithCoeff> cst;
1228  for (int i = 0; i < vars.size(); ++i) {
1229  const int ref = ct.linear().vars(i);
1230  cst.push_back({mapping->Literal(ref), coeffs[i]});
1231  }
1232  m->Add(BooleanLinearConstraint(lb, ub, &cst));
1233  } else {
1234  if (lb != kint64min) {
1235  m->Add(WeightedSumGreaterOrEqual(vars, coeffs, lb));
1236  }
1237  if (ub != kint64max) {
1238  m->Add(WeightedSumLowerOrEqual(vars, coeffs, ub));
1239  }
1240  }
1241  } else {
1242  const std::vector<Literal> enforcement_literals =
1243  mapping->Literals(ct.enforcement_literal());
1244  if (lb != kint64min) {
1245  m->Add(ConditionalWeightedSumGreaterOrEqual(enforcement_literals, vars,
1246  coeffs, lb));
1247  }
1248  if (ub != kint64max) {
1249  m->Add(ConditionalWeightedSumLowerOrEqual(enforcement_literals, vars,
1250  coeffs, ub));
1251  }
1252  }
1253  } else {
1254  // In this case, we can create just one Boolean instead of two since one
1255  // is the negation of the other.
1256  const bool special_case =
1257  ct.enforcement_literal().empty() && ct.linear().domain_size() == 4;
1258 
1259  std::vector<Literal> clause;
1260  for (int i = 0; i < ct.linear().domain_size(); i += 2) {
1261  int64 lb = ct.linear().domain(i);
1262  int64 ub = ct.linear().domain(i + 1);
1263  if (min_sum >= lb) lb = kint64min;
1264  if (max_sum <= ub) ub = kint64max;
1265 
1266  const Literal subdomain_literal(
1267  special_case && i > 0 ? clause.back().Negated()
1268  : Literal(m->Add(NewBooleanVariable()), true));
1269  clause.push_back(subdomain_literal);
1270 
1271  if (lb != kint64min) {
1272  m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars,
1273  coeffs, lb));
1274  }
1275  if (ub != kint64max) {
1276  m->Add(ConditionalWeightedSumLowerOrEqual({subdomain_literal}, vars,
1277  coeffs, ub));
1278  }
1279  }
1280  for (const int ref : ct.enforcement_literal()) {
1281  clause.push_back(mapping->Literal(ref).Negated());
1282  }
1283  if (!special_case) m->Add(ClauseConstraint(clause));
1284  }
1285 }
1286 
1287 void LoadAllDiffConstraint(const ConstraintProto& ct, Model* m) {
1288  auto* mapping = m->GetOrCreate<CpModelMapping>();
1289  const std::vector<IntegerVariable> vars =
1290  mapping->Integers(ct.all_diff().vars());
1291  // If all variables are fully encoded and domains are not too large, use
1292  // arc-consistent reasoning. Otherwise, use bounds-consistent reasoning.
1293  IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
1294  IntegerEncoder* encoder = m->GetOrCreate<IntegerEncoder>();
1295  int num_fully_encoded = 0;
1296  int64 max_domain_size = 0;
1297  for (const IntegerVariable variable : vars) {
1298  if (encoder->VariableIsFullyEncoded(variable)) num_fully_encoded++;
1299 
1300  IntegerValue lb = integer_trail->LowerBound(variable);
1301  IntegerValue ub = integer_trail->UpperBound(variable);
1302  const int64 domain_size = ub.value() - lb.value() + 1;
1303  max_domain_size = std::max(max_domain_size, domain_size);
1304  }
1305 
1306  if (num_fully_encoded == vars.size() && max_domain_size < 1024) {
1307  m->Add(AllDifferentBinary(vars));
1308  m->Add(AllDifferentAC(vars));
1309  } else {
1310  m->Add(AllDifferentOnBounds(vars));
1311  }
1312 }
1313 
1314 void LoadIntProdConstraint(const ConstraintProto& ct, Model* m) {
1315  auto* mapping = m->GetOrCreate<CpModelMapping>();
1316  const IntegerVariable prod = mapping->Integer(ct.int_prod().target());
1317  const std::vector<IntegerVariable> vars =
1318  mapping->Integers(ct.int_prod().vars());
1319  CHECK_EQ(vars.size(), 2) << "General int_prod not supported yet.";
1320  m->Add(ProductConstraint(vars[0], vars[1], prod));
1321 }
1322 
1323 void LoadIntDivConstraint(const ConstraintProto& ct, Model* m) {
1324  auto* mapping = m->GetOrCreate<CpModelMapping>();
1325  const IntegerVariable div = mapping->Integer(ct.int_div().target());
1326  const std::vector<IntegerVariable> vars =
1327  mapping->Integers(ct.int_div().vars());
1328  if (m->Get(IsFixed(vars[1]))) {
1329  const IntegerValue denom(m->Get(Value(vars[1])));
1330  if (denom == 1) {
1331  m->Add(Equality(vars[0], div));
1332  } else {
1333  m->Add(FixedDivisionConstraint(vars[0], denom, div));
1334  }
1335  } else {
1336  m->Add(DivisionConstraint(vars[0], vars[1], div));
1337  }
1338 }
1339 
1340 void LoadIntMinConstraint(const ConstraintProto& ct, Model* m) {
1341  auto* mapping = m->GetOrCreate<CpModelMapping>();
1342  const IntegerVariable min = mapping->Integer(ct.int_min().target());
1343  const std::vector<IntegerVariable> vars =
1344  mapping->Integers(ct.int_min().vars());
1345  m->Add(IsEqualToMinOf(min, vars));
1346 }
1347 
1348 LinearExpression GetExprFromProto(const LinearExpressionProto& expr_proto,
1349  const CpModelMapping& mapping) {
1350  LinearExpression expr;
1351  expr.vars = mapping.Integers(expr_proto.vars());
1352  for (int j = 0; j < expr_proto.coeffs_size(); ++j) {
1353  expr.coeffs.push_back(IntegerValue(expr_proto.coeffs(j)));
1354  }
1355  expr.offset = IntegerValue(expr_proto.offset());
1356  return CanonicalizeExpr(expr);
1357 }
1358 
1359 void LoadLinMaxConstraint(const ConstraintProto& ct, Model* m) {
1360  auto* mapping = m->GetOrCreate<CpModelMapping>();
1361  const LinearExpression max =
1362  GetExprFromProto(ct.lin_max().target(), *mapping);
1363  std::vector<LinearExpression> negated_exprs;
1364  negated_exprs.reserve(ct.lin_max().exprs_size());
1365  for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
1366  negated_exprs.push_back(
1367  NegationOf(GetExprFromProto(ct.lin_max().exprs(i), *mapping)));
1368  }
1369  // TODO(user): Consider replacing the min propagator by max.
1370  m->Add(IsEqualToMinOf(NegationOf(max), negated_exprs));
1371 }
1372 
1373 void LoadIntMaxConstraint(const ConstraintProto& ct, Model* m) {
1374  auto* mapping = m->GetOrCreate<CpModelMapping>();
1375  const IntegerVariable max = mapping->Integer(ct.int_max().target());
1376  const std::vector<IntegerVariable> vars =
1377  mapping->Integers(ct.int_max().vars());
1378  m->Add(IsEqualToMaxOf(max, vars));
1379 }
1380 
1381 void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m) {
1382  auto* mapping = m->GetOrCreate<CpModelMapping>();
1383  m->Add(Disjunctive(mapping->Intervals(ct.no_overlap().intervals())));
1384 }
1385 
1386 void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m) {
1387  if (ct.no_overlap_2d().x_intervals().empty()) return;
1388  auto* mapping = m->GetOrCreate<CpModelMapping>();
1389  const std::vector<IntervalVariable> x_intervals =
1390  mapping->Intervals(ct.no_overlap_2d().x_intervals());
1391  const std::vector<IntervalVariable> y_intervals =
1392  mapping->Intervals(ct.no_overlap_2d().y_intervals());
1394  x_intervals, y_intervals,
1395  !ct.no_overlap_2d().boxes_with_null_area_can_overlap()));
1396 }
1397 
1398 void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m) {
1399  auto* mapping = m->GetOrCreate<CpModelMapping>();
1400  const std::vector<IntervalVariable> intervals =
1401  mapping->Intervals(ct.cumulative().intervals());
1402  const AffineExpression capacity(mapping->Integer(ct.cumulative().capacity()));
1403  std::vector<AffineExpression> demands;
1404  for (const IntegerVariable var :
1405  mapping->Integers(ct.cumulative().demands())) {
1406  demands.push_back(AffineExpression(var));
1407  }
1408  m->Add(Cumulative(intervals, demands, capacity));
1409 }
1410 
1411 void LoadReservoirConstraint(const ConstraintProto& ct, Model* m) {
1412  auto* mapping = m->GetOrCreate<CpModelMapping>();
1413  auto* encoder = m->GetOrCreate<IntegerEncoder>();
1414  std::vector<AffineExpression> times;
1415  std::vector<IntegerValue> deltas;
1416  std::vector<Literal> presences;
1417  const int size = ct.reservoir().times().size();
1418  for (int i = 0; i < size; ++i) {
1419  times.push_back(mapping->Integer(ct.reservoir().times(i)));
1420  deltas.push_back(IntegerValue(ct.reservoir().demands(i)));
1421  if (!ct.reservoir().actives().empty()) {
1422  presences.push_back(mapping->Literal(ct.reservoir().actives(i)));
1423  } else {
1424  presences.push_back(encoder->GetTrueLiteral());
1425  }
1426  }
1427  AddReservoirConstraint(times, deltas, presences, ct.reservoir().min_level(),
1428  ct.reservoir().max_level(), m);
1429 }
1430 
1431 // If a variable is constant and its value appear in no other variable domains,
1432 // then the literal encoding the index and the one encoding the target at this
1433 // value are equivalent.
1434 bool DetectEquivalencesInElementConstraint(const ConstraintProto& ct,
1435  Model* m) {
1436  auto* mapping = m->GetOrCreate<CpModelMapping>();
1437  IntegerEncoder* encoder = m->GetOrCreate<IntegerEncoder>();
1438  IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
1439 
1440  const IntegerVariable index = mapping->Integer(ct.element().index());
1441  const IntegerVariable target = mapping->Integer(ct.element().target());
1442  const std::vector<IntegerVariable> vars =
1443  mapping->Integers(ct.element().vars());
1444  CHECK(!m->Get(IsFixed(index)));
1445  CHECK(!m->Get(IsFixed(target)));
1446 
1447  Domain union_of_non_constant_domains;
1448  std::map<IntegerValue, int> constant_to_num;
1449  for (const auto literal_value : m->Add(FullyEncodeVariable(index))) {
1450  const int i = literal_value.value.value();
1451  if (m->Get(IsFixed(vars[i]))) {
1452  const IntegerValue value(m->Get(Value(vars[i])));
1453  constant_to_num[value]++;
1454  } else {
1455  union_of_non_constant_domains = union_of_non_constant_domains.UnionWith(
1456  integer_trail->InitialVariableDomain(vars[i]));
1457  }
1458  }
1459 
1460  // Bump the number if the constant appear in union_of_non_constant_domains.
1461  for (const auto entry : constant_to_num) {
1462  if (union_of_non_constant_domains.Contains(entry.first.value())) {
1463  constant_to_num[entry.first]++;
1464  }
1465  }
1466 
1467  // Use the literal from the index encoding to encode the target at the
1468  // "unique" values.
1469  bool is_one_to_one_mapping = true;
1470  for (const auto literal_value : m->Add(FullyEncodeVariable(index))) {
1471  const int i = literal_value.value.value();
1472  if (!m->Get(IsFixed(vars[i]))) {
1473  is_one_to_one_mapping = false;
1474  continue;
1475  }
1476 
1477  const IntegerValue value(m->Get(Value(vars[i])));
1478  if (constant_to_num[value] == 1) {
1479  const Literal r = literal_value.literal;
1480  encoder->AssociateToIntegerEqualValue(r, target, value);
1481  } else {
1482  is_one_to_one_mapping = false;
1483  }
1484  }
1485 
1486  return is_one_to_one_mapping;
1487 }
1488 
1489 // TODO(user): Be more efficient when the element().vars() are constants.
1490 // Ideally we should avoid creating them as integer variable since we don't
1491 // use them.
1492 void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m) {
1493  auto* mapping = m->GetOrCreate<CpModelMapping>();
1494  const IntegerVariable index = mapping->Integer(ct.element().index());
1495  const IntegerVariable target = mapping->Integer(ct.element().target());
1496  const std::vector<IntegerVariable> vars =
1497  mapping->Integers(ct.element().vars());
1498  CHECK(!m->Get(IsFixed(index)));
1499 
1500  // We always fully encode the index on an element constraint.
1501  const auto encoding = m->Add(FullyEncodeVariable((index)));
1502  std::vector<Literal> selectors;
1503  std::vector<IntegerVariable> possible_vars;
1504  for (const auto literal_value : encoding) {
1505  const int i = literal_value.value.value();
1506  CHECK_GE(i, 0);
1507  CHECK_LT(i, vars.size());
1508  possible_vars.push_back(vars[i]);
1509  selectors.push_back(literal_value.literal);
1510  const Literal r = literal_value.literal;
1511 
1512  if (vars[i] == target) continue;
1513  if (m->Get(IsFixed(target))) {
1514  const int64 value = m->Get(Value(target));
1515  m->Add(ImpliesInInterval(r, vars[i], value, value));
1516  } else if (m->Get(IsFixed(vars[i]))) {
1517  const int64 value = m->Get(Value(vars[i]));
1518  m->Add(ImpliesInInterval(r, target, value, value));
1519  } else {
1520  m->Add(ConditionalLowerOrEqualWithOffset(vars[i], target, 0, r));
1521  m->Add(ConditionalLowerOrEqualWithOffset(target, vars[i], 0, r));
1522  }
1523  }
1524 
1525  if (!m->Get(IsFixed(target))) {
1526  m->Add(PartialIsOneOfVar(target, possible_vars, selectors));
1527  }
1528 }
1529 
1530 // Arc-Consistent encoding of the element constraint as SAT clauses.
1531 // The constraint enforces vars[index] == target.
1532 //
1533 // The AC propagation can be decomposed in three rules:
1534 // Rule 1: dom(index) == i => dom(vars[i]) == dom(target).
1535 // Rule 2: dom(target) \subseteq \Union_{i \in dom(index)} dom(vars[i]).
1536 // Rule 3: dom(index) \subseteq { i | |dom(vars[i]) \inter dom(target)| > 0 }.
1537 //
1538 // We encode this in a way similar to the table constraint, except that the
1539 // set of admissible tuples is not explicit.
1540 // First, we add Booleans selected[i][value] <=> (index == i /\ vars[i] ==
1541 // value). Rules 1 and 2 are enforced by target == value <=> \Or_{i}
1542 // selected[i][value]. Rule 3 is enforced by index == i <=> \Or_{value}
1543 // selected[i][value].
1544 void LoadElementConstraintAC(const ConstraintProto& ct, Model* m) {
1545  auto* mapping = m->GetOrCreate<CpModelMapping>();
1546  const IntegerVariable index = mapping->Integer(ct.element().index());
1547  const IntegerVariable target = mapping->Integer(ct.element().target());
1548  const std::vector<IntegerVariable> vars =
1549  mapping->Integers(ct.element().vars());
1550  CHECK(!m->Get(IsFixed(index)));
1551  CHECK(!m->Get(IsFixed(target)));
1552 
1553  absl::flat_hash_map<IntegerValue, Literal> target_map;
1554  const auto target_encoding = m->Add(FullyEncodeVariable(target));
1555  for (const auto literal_value : target_encoding) {
1556  target_map[literal_value.value] = literal_value.literal;
1557  }
1558 
1559  // For i \in index and value in vars[i], make (index == i /\ vars[i] == value)
1560  // literals and store them by value in vectors.
1561  absl::flat_hash_map<IntegerValue, std::vector<Literal>> value_to_literals;
1562  const auto index_encoding = m->Add(FullyEncodeVariable(index));
1563  IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
1564  for (const auto literal_value : index_encoding) {
1565  const int i = literal_value.value.value();
1566  const Literal i_lit = literal_value.literal;
1567 
1568  // Special case where vars[i] == value /\ i_lit is actually i_lit.
1569  if (m->Get(IsFixed(vars[i]))) {
1570  value_to_literals[integer_trail->LowerBound(vars[i])].push_back(i_lit);
1571  continue;
1572  }
1573 
1574  const auto var_encoding = m->Add(FullyEncodeVariable(vars[i]));
1575  std::vector<Literal> var_selected_literals;
1576  for (const auto var_literal_value : var_encoding) {
1577  const IntegerValue value = var_literal_value.value;
1578  const Literal var_is_value = var_literal_value.literal;
1579 
1580  if (!gtl::ContainsKey(target_map, value)) {
1581  // No need to add to value_to_literals, selected[i][value] is always
1582  // false.
1583  m->Add(Implication(i_lit, var_is_value.Negated()));
1584  continue;
1585  }
1586 
1587  const Literal var_is_value_and_selected =
1588  Literal(m->Add(NewBooleanVariable()), true);
1589  m->Add(ReifiedBoolAnd({i_lit, var_is_value}, var_is_value_and_selected));
1590  value_to_literals[value].push_back(var_is_value_and_selected);
1591  var_selected_literals.push_back(var_is_value_and_selected);
1592  }
1593  // index == i <=> \Or_{value} selected[i][value].
1594  m->Add(ReifiedBoolOr(var_selected_literals, i_lit));
1595  }
1596 
1597  // target == value <=> \Or_{i \in index} (vars[i] == value /\ index == i).
1598  for (const auto& entry : target_map) {
1599  const IntegerValue value = entry.first;
1600  const Literal target_is_value = entry.second;
1601 
1602  if (!gtl::ContainsKey(value_to_literals, value)) {
1603  m->Add(ClauseConstraint({target_is_value.Negated()}));
1604  } else {
1605  m->Add(ReifiedBoolOr(value_to_literals[value], target_is_value));
1606  }
1607  }
1608 }
1609 
1610 namespace {
1611 
1612 // This Boolean encoding is enough for consistency, but does not propagate as
1613 // much as LoadElementConstraintAC(). However, setting any of the non-propagated
1614 // Booleans to its "wrong" value will result directly in a conflict, so the
1615 // solver will easily learn an AC encoding...
1616 //
1617 // The advantage is that this does not introduce extra BooleanVariables.
1618 void LoadElementConstraintHalfAC(const ConstraintProto& ct, Model* m) {
1619  auto* mapping = m->GetOrCreate<CpModelMapping>();
1620  const IntegerVariable index = mapping->Integer(ct.element().index());
1621  const IntegerVariable target = mapping->Integer(ct.element().target());
1622  const std::vector<IntegerVariable> vars =
1623  mapping->Integers(ct.element().vars());
1624  CHECK(!m->Get(IsFixed(index)));
1625  CHECK(!m->Get(IsFixed(target)));
1626 
1627  m->Add(FullyEncodeVariable(target));
1628  for (const auto value_literal : m->Add(FullyEncodeVariable(index))) {
1629  const int i = value_literal.value.value();
1630  m->Add(FullyEncodeVariable(vars[i]));
1631  LoadEquivalenceAC({value_literal.literal}, IntegerValue(1), vars[i],
1632  IntegerValue(-1), target, IntegerValue(0), m);
1633  }
1634 }
1635 
1636 void LoadBooleanElement(const ConstraintProto& ct, Model* m) {
1637  auto* mapping = m->GetOrCreate<CpModelMapping>();
1638  const IntegerVariable index = mapping->Integer(ct.element().index());
1639  const std::vector<Literal> literals = mapping->Literals(ct.element().vars());
1640  const Literal target = mapping->Literal(ct.element().target());
1641 
1642  if (m->Get(IsFixed(index))) {
1643  m->Add(Equality(target, literals[m->Get(Value(index))]));
1644  return;
1645  }
1646 
1647  std::vector<Literal> all_true;
1648  std::vector<Literal> all_false;
1649  for (const auto value_literal : m->Add(FullyEncodeVariable(index))) {
1650  const Literal a_lit = literals[value_literal.value.value()];
1651  const Literal i_lit = value_literal.literal;
1652  m->Add(ClauseConstraint({i_lit.Negated(), a_lit.Negated(), target}));
1653  m->Add(ClauseConstraint({i_lit.Negated(), a_lit, target.Negated()}));
1654  all_true.push_back(a_lit.Negated());
1655  all_false.push_back(a_lit);
1656  }
1657  all_true.push_back(target);
1658  all_false.push_back(target.Negated());
1659  m->Add(ClauseConstraint(all_true));
1660  m->Add(ClauseConstraint(all_false));
1661  // TODO(user): Investigate filtering this with active literals.
1662 }
1663 
1664 } // namespace
1665 
1666 void LoadElementConstraint(const ConstraintProto& ct, Model* m) {
1667  auto* mapping = m->GetOrCreate<CpModelMapping>();
1668  const IntegerVariable index = mapping->Integer(ct.element().index());
1669 
1670  bool boolean_array = true;
1671  for (const int ref : ct.element().vars()) {
1672  if (!mapping->IsBoolean(ref)) {
1673  boolean_array = false;
1674  break;
1675  }
1676  }
1677  if (boolean_array && !mapping->IsBoolean(ct.element().target())) {
1678  // Should have been reduced but presolve.
1679  VLOG(1) << "Fix boolean_element not propagated on target";
1680  boolean_array = false;
1681  }
1682 
1683  // TODO(user): Move this to presolve. Leads to a larger discussion on
1684  // adding full encoding to model during presolve.
1685  if (boolean_array) {
1686  LoadBooleanElement(ct, m);
1687  return;
1688  }
1689 
1690  const IntegerVariable target = mapping->Integer(ct.element().target());
1691  const std::vector<IntegerVariable> vars =
1692  mapping->Integers(ct.element().vars());
1693 
1694  // Retrict the domain of index in case there was no presolve.
1696  index, Domain(0, vars.size() - 1))) {
1697  return;
1698  }
1699 
1700  // This returns true if there is nothing else to do after the equivalences
1701  // of the form (index literal <=> target_literal) have been added.
1702  if (!m->Get(IsFixed(index)) && !m->Get(IsFixed(target)) &&
1704  return;
1705  }
1706 
1707  // Special case when index is fixed.
1708  if (m->Get(IsFixed(index))) {
1709  m->Add(Equality(target, vars[m->Get(Value(index))]));
1710  return;
1711  }
1712 
1713  // Special case when target is fixed.
1714  if (m->Get(IsFixed(target))) {
1715  return LoadElementConstraintBounds(ct, m);
1716  }
1717 
1718  IntegerEncoder* encoder = m->GetOrCreate<IntegerEncoder>();
1719  const bool target_is_AC = encoder->VariableIsFullyEncoded(target);
1720 
1721  int num_AC_variables = 0;
1722  const int num_vars = ct.element().vars().size();
1723  for (const int v : ct.element().vars()) {
1724  IntegerVariable variable = mapping->Integer(v);
1725  const bool is_full =
1726  m->Get(IsFixed(variable)) || encoder->VariableIsFullyEncoded(variable);
1727  if (is_full) num_AC_variables++;
1728  }
1729 
1730  const SatParameters& params = *m->GetOrCreate<SatParameters>();
1731  if (params.boolean_encoding_level() > 0 &&
1732  (target_is_AC || num_AC_variables >= num_vars - 1)) {
1733  if (params.boolean_encoding_level() > 1) {
1735  } else {
1736  LoadElementConstraintHalfAC(ct, m);
1737  }
1738  } else {
1740  }
1741 }
1742 
1743 void LoadTableConstraint(const ConstraintProto& ct, Model* m) {
1744  auto* mapping = m->GetOrCreate<CpModelMapping>();
1745  const std::vector<IntegerVariable> vars =
1746  mapping->Integers(ct.table().vars());
1747  const std::vector<int64> values = ValuesFromProto(ct.table().values());
1748  const int num_vars = vars.size();
1749  const int num_tuples = values.size() / num_vars;
1750  std::vector<std::vector<int64>> tuples(num_tuples);
1751  int count = 0;
1752  for (int i = 0; i < num_tuples; ++i) {
1753  for (int j = 0; j < num_vars; ++j) {
1754  tuples[i].push_back(values[count++]);
1755  }
1756  }
1757  if (ct.table().negated()) {
1758  AddNegatedTableConstraint(vars, std::move(tuples), m);
1759  } else {
1760  AddTableConstraint(vars, std::move(tuples), m);
1761  }
1762 }
1763 
1764 void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m) {
1765  auto* mapping = m->GetOrCreate<CpModelMapping>();
1766  const std::vector<IntegerVariable> vars =
1767  mapping->Integers(ct.automaton().vars());
1768 
1769  const int num_transitions = ct.automaton().transition_tail_size();
1770  std::vector<std::vector<int64>> transitions;
1771  transitions.reserve(num_transitions);
1772  for (int i = 0; i < num_transitions; ++i) {
1773  transitions.push_back({ct.automaton().transition_tail(i),
1774  ct.automaton().transition_label(i),
1775  ct.automaton().transition_head(i)});
1776  }
1777 
1778  const int64 starting_state = ct.automaton().starting_state();
1779  const std::vector<int64> final_states =
1780  ValuesFromProto(ct.automaton().final_states());
1781  m->Add(TransitionConstraint(vars, transitions, starting_state, final_states));
1782 }
1783 
1784 // From vector of n IntegerVariables, returns an n x n matrix of Literal
1785 // such that matrix[i][j] is the Literal corresponding to vars[i] == j.
1786 std::vector<std::vector<Literal>> GetSquareMatrixFromIntegerVariables(
1787  const std::vector<IntegerVariable>& vars, Model* m) {
1788  const int n = vars.size();
1789  const Literal kTrueLiteral =
1790  m->GetOrCreate<IntegerEncoder>()->GetTrueLiteral();
1791  const Literal kFalseLiteral =
1792  m->GetOrCreate<IntegerEncoder>()->GetFalseLiteral();
1793  std::vector<std::vector<Literal>> matrix(
1794  n, std::vector<Literal>(n, kFalseLiteral));
1795  for (int i = 0; i < n; i++) {
1796  for (int j = 0; j < n; j++) {
1797  if (m->Get(IsFixed(vars[i]))) {
1798  const int value = m->Get(Value(vars[i]));
1799  DCHECK_LE(0, value);
1800  DCHECK_LT(value, n);
1801  matrix[i][value] = kTrueLiteral;
1802  } else {
1803  const auto encoding = m->Add(FullyEncodeVariable(vars[i]));
1804  for (const auto& entry : encoding) {
1805  const int value = entry.value.value();
1806  DCHECK_LE(0, value);
1807  DCHECK_LT(value, n);
1808  matrix[i][value] = entry.literal;
1809  }
1810  }
1811  }
1812  }
1813  return matrix;
1814 }
1815 
1816 void LoadCircuitConstraint(const ConstraintProto& ct, Model* m) {
1817  const auto& circuit = ct.circuit();
1818  if (circuit.tails().empty()) return;
1819 
1820  std::vector<int> tails(circuit.tails().begin(), circuit.tails().end());
1821  std::vector<int> heads(circuit.heads().begin(), circuit.heads().end());
1822  std::vector<Literal> literals =
1823  m->GetOrCreate<CpModelMapping>()->Literals(circuit.literals());
1824  const int num_nodes = ReindexArcs(&tails, &heads);
1825  m->Add(SubcircuitConstraint(num_nodes, tails, heads, literals));
1826 }
1827 
1828 void LoadRoutesConstraint(const ConstraintProto& ct, Model* m) {
1829  const auto& routes = ct.routes();
1830  if (routes.tails().empty()) return;
1831 
1832  std::vector<int> tails(routes.tails().begin(), routes.tails().end());
1833  std::vector<int> heads(routes.heads().begin(), routes.heads().end());
1834  std::vector<Literal> literals =
1835  m->GetOrCreate<CpModelMapping>()->Literals(routes.literals());
1836  const int num_nodes = ReindexArcs(&tails, &heads);
1837  m->Add(SubcircuitConstraint(num_nodes, tails, heads, literals,
1838  /*multiple_subcircuit_through_zero=*/true));
1839 }
1840 
1841 bool LoadConstraint(const ConstraintProto& ct, Model* m) {
1842  switch (ct.constraint_case()) {
1843  case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1844  return true;
1845  case ConstraintProto::ConstraintCase::kBoolOr:
1847  return true;
1848  case ConstraintProto::ConstraintCase::kBoolAnd:
1850  return true;
1851  case ConstraintProto::ConstraintCase::kAtMostOne:
1853  return true;
1854  case ConstraintProto::ConstraintCase::kExactlyOne:
1856  return true;
1857  case ConstraintProto::ConstraintCase::kBoolXor:
1859  return true;
1860  case ConstraintProto::ConstraintProto::kLinear:
1862  return true;
1863  case ConstraintProto::ConstraintProto::kAllDiff:
1865  return true;
1866  case ConstraintProto::ConstraintProto::kIntProd:
1868  return true;
1869  case ConstraintProto::ConstraintProto::kIntDiv:
1871  return true;
1872  case ConstraintProto::ConstraintProto::kIntMin:
1874  return true;
1875  case ConstraintProto::ConstraintProto::kLinMax:
1877  return true;
1878  case ConstraintProto::ConstraintProto::kIntMax:
1880  return true;
1881  case ConstraintProto::ConstraintProto::kInterval:
1882  // Already dealt with.
1883  return true;
1884  case ConstraintProto::ConstraintProto::kNoOverlap:
1886  return true;
1887  case ConstraintProto::ConstraintProto::kNoOverlap2D:
1889  return true;
1890  case ConstraintProto::ConstraintProto::kCumulative:
1892  return true;
1893  case ConstraintProto::ConstraintProto::kReservoir:
1895  return true;
1896  case ConstraintProto::ConstraintProto::kElement:
1898  return true;
1899  case ConstraintProto::ConstraintProto::kTable:
1900  LoadTableConstraint(ct, m);
1901  return true;
1902  case ConstraintProto::ConstraintProto::kAutomaton:
1904  return true;
1905  case ConstraintProto::ConstraintProto::kCircuit:
1907  return true;
1908  case ConstraintProto::ConstraintProto::kRoutes:
1910  return true;
1911  default:
1912  return false;
1913  }
1914 }
1915 
1916 } // namespace sat
1917 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define VLOG(verboselevel)
Definition: base/logging.h:978
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
size_type size() const
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
Domain Complement() const
Returns the set Int64 ∖ D.
int64 Size() const
Returns the number of elements in the domain.
int NumIntervals() const
Basic read-only std::vector<> wrapping to view a Domain as a sorted list of non-adjacent intervals.
Domain InverseMultiplicationBy(const int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
int64 Min() const
Returns the min value of the domain.
Domain UnionWith(const Domain &domain) const
Returns the union of D and 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.
std::vector< sat::Literal > Literals(const ProtoIndices &indices) const
AffineExpression LoadAffineView(const LinearExpressionProto &exp) const
std::vector< IntegerVariable > Integers(const List &list) const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
void LoadBooleanSymmetries(const CpModelProto &model_proto, Model *m)
bool ConstraintIsAlreadyLoaded(const ConstraintProto *ct) const
IntegerVariable Integer(int ref) const
sat::Literal Literal(int ref) const
void DetectOptionalVariables(const CpModelProto &model_proto, Model *m)
const absl::flat_hash_set< int64 > & PotentialEncodedValues(int var)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
void PropagateEncodingFromEquivalenceRelations(const CpModelProto &model_proto, Model *m)
void CreateVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
FullEncodingFixedPointComputer(const CpModelProto &model_proto, Model *model)
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
Definition: integer.cc:308
bool VariableIsFullyEncoded(IntegerVariable var) const
Definition: integer.cc:68
void ReserveSpaceForNumVariables(int num_vars)
Definition: integer.cc:592
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
LiteralIndex Index() const
Definition: sat_base.h:84
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Definition: sat/model.h:87
T Add(std::function< T(Model *)> f)
This makes it possible to have a nicer API on the client side, and it allows both of these forms:
Definition: sat/model.h:81
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
Definition: sat/model.h:106
bool AddProblemClause(absl::Span< const Literal > literals)
Definition: sat_solver.cc:203
SatParameters parameters
CpModelProto proto
CpModelProto const * model_proto
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int INFO
Definition: log_severity.h:31
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
void LoadTableConstraint(const ConstraintProto &ct, Model *m)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
std::function< void(Model *)> ConditionalWeightedSumLowerOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
Definition: integer_expr.h:426
std::function< void(Model *)> AllDifferentAC(const std::vector< IntegerVariable > &variables)
std::function< void(Model *)> NonOverlappingRectangles(const std::vector< IntervalVariable > &x, const std::vector< IntervalVariable > &y, bool is_strict)
Definition: diffn.h:155
std::function< void(Model *)> IsEqualToMaxOf(IntegerVariable max_var, const std::vector< IntegerVariable > &vars)
Definition: integer_expr.h:741
void LoadExactlyOneConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:404
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:876
void LoadIntProdConstraint(const ConstraintProto &ct, Model *m)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
std::vector< int > UsedVariables(const ConstraintProto &ct)
void LoadBoolOrConstraint(const ConstraintProto &ct, Model *m)
bool RefIsPositive(int ref)
std::function< void(Model *)> DivisionConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable c)
Definition: integer_expr.h:810
void MaybeFullyEncodeMoreVariables(const CpModelProto &model_proto, Model *m)
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> TransitionConstraint(const std::vector< IntegerVariable > &vars, const std::vector< std::vector< int64 >> &automaton, int64 initial_state, const std::vector< int64 > &final_states)
Definition: sat/table.cc:591
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
Definition: intervals.h:662
std::function< void(Model *)> PartialIsOneOfVar(IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
std::function< void(Model *)> LiteralXorIs(const std::vector< Literal > &literals, bool value)
std::function< void(Model *)> ConditionalLowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
Definition: precedences.h:419
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
std::function< void(Model *)> SubcircuitConstraint(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, bool multiple_subcircuit_through_zero)
Definition: circuit.cc:471
std::function< int64(const Model &)> Value(IntegerVariable v)
Definition: integer.h:1487
bool HasEnforcementLiteral(const ConstraintProto &ct)
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< IntegerVariable > &vars)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >Model *)> FullyEncodeVariable(IntegerVariable var)
Definition: integer.h:1587
bool DetectEquivalencesInElementConstraint(const ConstraintProto &ct, Model *m)
void LoadCumulativeConstraint(const ConstraintProto &ct, Model *m)
void LoadRoutesConstraint(const ConstraintProto &ct, Model *m)
void LoadReservoirConstraint(const ConstraintProto &ct, Model *m)
void AddTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 >> tuples, Model *model)
Definition: sat/table.cc:248
void LoadBoolAndConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
Definition: sat_solver.h:852
void LoadLinMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadBoolXorConstraint(const ConstraintProto &ct, Model *m)
LinearExpression GetExprFromProto(const LinearExpressionProto &expr_proto, const CpModelMapping &mapping)
const IntegerVariable kNoIntegerVariable(-1)
const IntervalVariable kNoIntervalVariable(-1)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
Definition: intervals.h:632
LinearExpression CanonicalizeExpr(const LinearExpression &expr)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
Definition: integer.h:1524
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:35
std::function< void(Model *)> ImpliesInInterval(Literal in_interval, IntegerVariable v, int64 lb, int64 ub)
Definition: integer.h:1564
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
Definition: sat_solver.h:950
std::vector< std::vector< Literal > > GetSquareMatrixFromIntegerVariables(const std::vector< IntegerVariable > &vars, Model *m)
void LoadIntDivConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ConditionalWeightedSumGreaterOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:514
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
Definition: integer.h:1537
std::function< void(Model *)> FixedDivisionConstraint(IntegerVariable a, IntegerValue b, IntegerVariable c)
Definition: integer_expr.h:823
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< IntegerValue > deltas, std::vector< Literal > presences, int64 min_level, int64 max_level, Model *model)
Definition: timetable.cc:27
int ReindexArcs(IntContainer *tails, IntContainer *heads)
Definition: circuit.h:168
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:30
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
Definition: integer_expr.h:299
void LoadAtMostOneConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> AllDifferentBinary(const std::vector< IntegerVariable > &vars)
void LoadCircuitConstraint(const ConstraintProto &ct, Model *m)
void LoadIntMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadNoOverlapConstraint(const ConstraintProto &ct, Model *m)
void LoadAllDiffConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:968
void AddNegatedTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 >> tuples, Model *model)
Definition: sat/table.cc:457
void LoadElementConstraint(const ConstraintProto &ct, Model *m)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
void LoadAutomatonConstraint(const ConstraintProto &ct, Model *m)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
std::function< void(Model *)> IsEqualToMinOf(IntegerVariable min_var, const std::vector< IntegerVariable > &vars)
Definition: integer_expr.h:672
void LoadNoOverlap2dConstraint(const ConstraintProto &ct, Model *m)
void LoadIntMinConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> AtMostOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:890
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1479
const BooleanVariable kNoBooleanVariable(-1)
std::function< void(Model *)> ProductConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable p)
Definition: integer_expr.h:769
void LoadElementConstraintAC(const ConstraintProto &ct, Model *m)
void LoadElementConstraintBounds(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ReifiedBoolOr(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:934
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 capacity
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41