Google OR-Tools v9.12
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_loader.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <cmath>
18#include <cstdint>
19#include <memory>
20#include <numeric>
21#include <string>
22#include <utility>
23#include <vector>
24
25#include "absl/container/btree_map.h"
26#include "absl/container/btree_set.h"
27#include "absl/container/flat_hash_map.h"
28#include "absl/container/flat_hash_set.h"
29#include "absl/log/check.h"
30#include "absl/meta/type_traits.h"
31#include "absl/strings/str_cat.h"
32#include "absl/types/span.h"
39#include "ortools/sat/circuit.h"
40#include "ortools/sat/clause.h"
42#include "ortools/sat/cp_model.pb.h"
46#include "ortools/sat/diffn.h"
49#include "ortools/sat/integer.h"
54#include "ortools/sat/model.h"
58#include "ortools/sat/sat_parameters.pb.h"
65
66namespace operations_research {
67namespace sat {
68
69namespace {
70
71template <typename Values>
72std::vector<int64_t> ValuesFromProto(const Values& values) {
73 return std::vector<int64_t>(values.begin(), values.end());
74}
75
76void ComputeLinearBounds(const LinearConstraintProto& proto,
77 CpModelMapping* mapping, IntegerTrail* integer_trail,
78 int64_t* sum_min, int64_t* sum_max) {
79 *sum_min = 0;
80 *sum_max = 0;
81
82 for (int i = 0; i < proto.vars_size(); ++i) {
83 const int64_t coeff = proto.coeffs(i);
84 const IntegerVariable var = mapping->Integer(proto.vars(i));
85 const int64_t lb = integer_trail->LowerBound(var).value();
86 const int64_t ub = integer_trail->UpperBound(var).value();
87 if (coeff >= 0) {
88 (*sum_min) += coeff * lb;
89 (*sum_max) += coeff * ub;
90 } else {
91 (*sum_min) += coeff * ub;
92 (*sum_max) += coeff * lb;
93 }
94 }
95}
96
97// We check if the constraint is a sum(ax * xi) == value.
98bool ConstraintIsEq(const LinearConstraintProto& proto) {
99 return proto.domain_size() == 2 && proto.domain(0) == proto.domain(1);
100}
101
102// We check if the constraint is a sum(ax * xi) != value.
103bool ConstraintIsNEq(const LinearConstraintProto& proto,
104 CpModelMapping* mapping, IntegerTrail* integer_trail,
105 int64_t* single_value) {
106 int64_t sum_min = 0;
107 int64_t sum_max = 0;
108 ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max);
109
110 const Domain complement =
111 Domain(sum_min, sum_max)
112 .IntersectionWith(ReadDomainFromProto(proto).Complement());
113 if (complement.IsEmpty()) return false;
114 const int64_t value = complement.Min();
115
116 if (complement.Size() == 1) {
117 if (single_value != nullptr) {
118 *single_value = value;
119 }
120 return true;
121 }
122 return false;
123}
124
125} // namespace
126
127void LoadVariables(const CpModelProto& model_proto,
128 bool view_all_booleans_as_integers, Model* m) {
129 auto* mapping = m->GetOrCreate<CpModelMapping>();
130 const int num_proto_variables = model_proto.variables_size();
131
132 // All [0, 1] variables always have a corresponding Boolean, even if it is
133 // fixed to 0 (domain == [0,0]) or fixed to 1 (domain == [1,1]).
134 {
135 auto* sat_solver = m->GetOrCreate<SatSolver>();
136 CHECK_EQ(sat_solver->NumVariables(), 0);
137
138 BooleanVariable new_var(0);
139 std::vector<BooleanVariable> false_variables;
140 std::vector<BooleanVariable> true_variables;
141
142 mapping->booleans_.resize(num_proto_variables, kNoBooleanVariable);
143 mapping->reverse_boolean_map_.resize(num_proto_variables, -1);
144 for (int i = 0; i < num_proto_variables; ++i) {
145 const auto& domain = model_proto.variables(i).domain();
146 if (domain.size() != 2) continue;
147 if (domain[0] >= 0 && domain[1] <= 1) {
148 mapping->booleans_[i] = new_var;
149 mapping->reverse_boolean_map_[new_var] = i;
150 if (domain[1] == 0) {
151 false_variables.push_back(new_var);
152 } else if (domain[0] == 1) {
153 true_variables.push_back(new_var);
154 }
155 ++new_var;
156 }
157 }
158
159 sat_solver->SetNumVariables(new_var.value());
160 for (const BooleanVariable var : true_variables) {
161 m->Add(ClauseConstraint({sat::Literal(var, true)}));
162 }
163 for (const BooleanVariable var : false_variables) {
164 m->Add(ClauseConstraint({sat::Literal(var, false)}));
165 }
166 }
167
168 // Compute the list of positive variable reference for which we need to
169 // create an IntegerVariable.
170 std::vector<int> var_to_instantiate_as_integer;
171 if (view_all_booleans_as_integers) {
172 var_to_instantiate_as_integer.resize(num_proto_variables);
173 for (int i = 0; i < num_proto_variables; ++i) {
174 var_to_instantiate_as_integer[i] = i;
175 }
176 } else {
177 // Compute the integer variable references used by the model.
178 absl::flat_hash_set<int> used_variables;
179
180 const bool some_linerization =
181 m->GetOrCreate<SatParameters>()->linearization_level() > 0;
182
183 IndexReferences refs;
184 for (int c = 0; c < model_proto.constraints_size(); ++c) {
185 const ConstraintProto& ct = model_proto.constraints(c);
187 for (const int ref : refs.variables) {
188 used_variables.insert(PositiveRef(ref));
189 }
190
191 // We always add a linear relaxation for circuit/route except for
192 // linearization level zero.
193 if (some_linerization) {
194 if (ct.constraint_case() == ConstraintProto::kCircuit) {
195 for (const int ref : ct.circuit().literals()) {
196 used_variables.insert(PositiveRef(ref));
197 }
198 } else if (ct.constraint_case() == ConstraintProto::kRoutes) {
199 for (const int ref : ct.routes().literals()) {
200 used_variables.insert(PositiveRef(ref));
201 }
202 }
203 }
204 }
205
206 // Add the objectives variables that needs to be referenceable as integer
207 // even if they are only used as Booleans.
208 if (model_proto.has_objective()) {
209 for (const int obj_var : model_proto.objective().vars()) {
210 used_variables.insert(PositiveRef(obj_var));
211 }
212 }
213
214 // Make sure any unused variable, that is not already a Boolean is
215 // considered "used".
216 for (int i = 0; i < num_proto_variables; ++i) {
217 if (mapping->booleans_[i] == kNoBooleanVariable) {
218 used_variables.insert(i);
219 }
220 }
221
222 // We want the variable in the problem order.
223 var_to_instantiate_as_integer.assign(used_variables.begin(),
224 used_variables.end());
225 gtl::STLSortAndRemoveDuplicates(&var_to_instantiate_as_integer);
226 }
227 mapping->integers_.resize(num_proto_variables, kNoIntegerVariable);
228
229 // It is important for memory usage to reserve tight vector has we have many
230 // indexed by IntegerVariable. Unfortunately, we create intermediate
231 // IntegerVariable while loading large linear constraint, or when we have
232 // disjoint LP component. So this is a best effort at a tight upper bound.
233 int reservation_size = var_to_instantiate_as_integer.size();
234 for (const ConstraintProto& ct : model_proto.constraints()) {
235 if (ct.constraint_case() != ConstraintProto::kLinear) continue;
236 const int ct_size = ct.linear().vars().size();
237 if (ct_size > 100) {
238 reservation_size += static_cast<int>(std::round(std::sqrt(ct_size)));
239 }
240 }
241 if (model_proto.has_objective()) {
242 reservation_size += 1; // Objective var.
243 const int ct_size = model_proto.objective().vars().size() + 1;
244 if (ct_size > 100) {
245 reservation_size += static_cast<int>(std::round(std::sqrt(ct_size)));
246 }
247 }
248
249 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
250 integer_trail->ReserveSpaceForNumVariables(reservation_size);
251 m->GetOrCreate<GenericLiteralWatcher>()->ReserveSpaceForNumVariables(
252 reservation_size);
253 mapping->reverse_integer_map_.resize(2 * var_to_instantiate_as_integer.size(),
254 -1);
255 for (const int i : var_to_instantiate_as_integer) {
256 const auto& var_proto = model_proto.variables(i);
257 mapping->integers_[i] =
258 integer_trail->AddIntegerVariable(ReadDomainFromProto(var_proto));
259 DCHECK_LT(mapping->integers_[i], mapping->reverse_integer_map_.size());
260 mapping->reverse_integer_map_[mapping->integers_[i]] = i;
261 }
262
263 auto* encoder = m->GetOrCreate<IntegerEncoder>();
264 auto* intervals_repository = m->GetOrCreate<IntervalsRepository>();
265
266 // Link any variable that has both views.
267 for (int i = 0; i < num_proto_variables; ++i) {
268 if (mapping->integers_[i] == kNoIntegerVariable) continue;
269 if (mapping->booleans_[i] == kNoBooleanVariable) continue;
270
271 // Associate with corresponding integer variable.
272 encoder->AssociateToIntegerEqualValue(
273 sat::Literal(mapping->booleans_[i], true), mapping->integers_[i],
274 IntegerValue(1));
275 }
276
277 // Create the interval variables.
278 mapping->intervals_.resize(model_proto.constraints_size(),
280 for (int c = 0; c < model_proto.constraints_size(); ++c) {
281 const ConstraintProto& ct = model_proto.constraints(c);
282 if (ct.constraint_case() != ConstraintProto::ConstraintCase::kInterval) {
283 continue;
284 }
285 if (HasEnforcementLiteral(ct)) {
286 const sat::Literal enforcement_literal =
287 mapping->Literal(ct.enforcement_literal(0));
288 // TODO(user): Fix the constant variable situation. An optional interval
289 // with constant start/end or size cannot share the same constant
290 // variable if it is used in non-optional situation.
291 mapping->intervals_[c] = intervals_repository->CreateInterval(
292 mapping->Affine(ct.interval().start()),
293 mapping->Affine(ct.interval().end()),
294 mapping->Affine(ct.interval().size()), enforcement_literal.Index(),
295 /*add_linear_relation=*/false);
296 } else {
297 mapping->intervals_[c] = intervals_repository->CreateInterval(
298 mapping->Affine(ct.interval().start()),
299 mapping->Affine(ct.interval().end()),
300 mapping->Affine(ct.interval().size()), kNoLiteralIndex,
301 /*add_linear_relation=*/false);
302 }
303 mapping->already_loaded_ct_.insert(&ct);
304 }
305}
306
307void LoadBooleanSymmetries(const CpModelProto& model_proto, Model* m) {
308 auto* mapping = m->GetOrCreate<CpModelMapping>();
309 const SymmetryProto& symmetry = model_proto.symmetry();
310 if (symmetry.permutations().empty()) return;
311
312 // We currently can only use symmetry that touch a subset of variables.
313 const int num_vars = model_proto.variables().size();
314 std::vector<bool> can_be_used_in_symmetry(num_vars, true);
315
316 // First, we currently only support loading symmetry between Booleans.
317 for (int v = 0; v < num_vars; ++v) {
318 if (!mapping->IsBoolean(v)) can_be_used_in_symmetry[v] = false;
319 }
320
321 // Tricky: Moreover, some constraint will causes extra Boolean to be created
322 // and linked with the Boolean in the constraints. We can't use any of the
323 // symmetry that touch these since we potentially miss the component that will
324 // map these extra Booleans between each other.
325 //
326 // TODO(user): We could add these extra Boolean during expansion/presolve so
327 // that we have the symmetry involing them. Or maybe comes up with a different
328 // solution.
329 const int num_constraints = model_proto.constraints().size();
330 for (int c = 0; c < num_constraints; ++c) {
331 const ConstraintProto& ct = model_proto.constraints(c);
332 if (ct.constraint_case() != ConstraintProto::kLinear) continue;
333 if (ct.linear().domain().size() <= 2) continue;
334
335 // A linear with a complex domain might need extra Booleans to be loaded.
336 // Note that it should be fine for the Boolean(s) in enforcement_literal
337 // though.
338 for (const int ref : ct.linear().vars()) {
339 can_be_used_in_symmetry[PositiveRef(ref)] = false;
340 }
341 }
342
343 auto* sat_solver = m->GetOrCreate<SatSolver>();
344 auto* symmetry_handler = m->GetOrCreate<SymmetryPropagator>();
345 sat_solver->AddPropagator(symmetry_handler);
346 const int num_literals = 2 * sat_solver->NumVariables();
347
348 for (const SparsePermutationProto& perm : symmetry.permutations()) {
349 bool can_be_used = true;
350 for (const int var : perm.support()) {
351 if (!can_be_used_in_symmetry[var]) {
352 can_be_used = false;
353 break;
354 }
355 }
356 if (!can_be_used) continue;
357
358 // Convert the variable symmetry to a "literal" one.
359 auto literal_permutation =
360 std::make_unique<SparsePermutation>(num_literals);
361 int support_index = 0;
362 const int num_cycle = perm.cycle_sizes().size();
363 for (int i = 0; i < num_cycle; ++i) {
364 const int size = perm.cycle_sizes(i);
365 const int saved_support_index = support_index;
366 for (int j = 0; j < size; ++j) {
367 const int var = perm.support(support_index++);
368 literal_permutation->AddToCurrentCycle(
369 mapping->Literal(var).Index().value());
370 }
371 literal_permutation->CloseCurrentCycle();
372
373 // Note that we also need to add the corresponding cycle for the negated
374 // literals.
375 support_index = saved_support_index;
376 for (int j = 0; j < size; ++j) {
377 const int var = perm.support(support_index++);
378 literal_permutation->AddToCurrentCycle(
379 mapping->Literal(var).NegatedIndex().value());
380 }
381 literal_permutation->CloseCurrentCycle();
382 }
383 symmetry_handler->AddSymmetry(std::move(literal_permutation));
384 }
385
386 SOLVER_LOG(m->GetOrCreate<SolverLogger>(), "Added ",
387 symmetry_handler->num_permutations(),
388 " symmetry to the SAT solver.");
389}
390
391// The logic assumes that the linear constraints have been presolved, so that
392// equality with a domain bound have been converted to <= or >= and so that we
393// never have any trivial inequalities.
394//
395// TODO(user): Regroup/presolve two encoding like b => x > 2 and the same
396// Boolean b => x > 5. These shouldn't happen if we merge linear constraints.
397void ExtractEncoding(const CpModelProto& model_proto, Model* m) {
398 auto* mapping = m->GetOrCreate<CpModelMapping>();
399 auto* encoder = m->GetOrCreate<IntegerEncoder>();
400 auto* logger = m->GetOrCreate<SolverLogger>();
401 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
402 auto* sat_solver = m->GetOrCreate<SatSolver>();
403
404 // TODO(user): Debug what makes it unsat at this point.
405 if (sat_solver->ModelIsUnsat()) return;
406
407 // Detection of literal equivalent to (i_var == value). We collect all the
408 // half-reified constraint lit => equality or lit => inequality for a given
409 // variable, and we will later sort them to detect equivalence.
410 struct EqualityDetectionHelper {
411 const ConstraintProto* ct;
412 sat::Literal literal;
413 int64_t value;
414 bool is_equality; // false if != instead.
415
416 bool operator<(const EqualityDetectionHelper& o) const {
417 if (literal.Variable() == o.literal.Variable()) {
418 if (value == o.value) return is_equality && !o.is_equality;
419 return value < o.value;
420 }
421 return literal.Variable() < o.literal.Variable();
422 }
423 };
424 std::vector<std::vector<EqualityDetectionHelper>> var_to_equalities(
425 model_proto.variables_size());
426
427 // TODO(user): We will re-add the same implied bounds during probing, so
428 // it might not be necessary to do that here. Also, it might be too early
429 // if some of the literal view used in the LP are created later, but that
430 // should be fixable via calls to implied_bounds->NotifyNewIntegerView().
431 auto* implied_bounds = m->GetOrCreate<ImpliedBounds>();
432 auto* detector = m->GetOrCreate<ProductDetector>();
433
434 // Detection of literal equivalent to (i_var >= bound). We also collect
435 // all the half-refied part and we will sort the vector for detection of the
436 // equivalence.
437 struct InequalityDetectionHelper {
438 const ConstraintProto* ct;
439 sat::Literal literal;
440 IntegerLiteral i_lit;
441
442 bool operator<(const InequalityDetectionHelper& o) const {
443 if (literal.Variable() == o.literal.Variable()) {
444 return i_lit.var < o.i_lit.var;
445 }
446 return literal.Variable() < o.literal.Variable();
447 }
448 };
449 std::vector<InequalityDetectionHelper> inequalities;
450
451 // Loop over all constraints and fill var_to_equalities and inequalities.
452 for (const ConstraintProto& ct : model_proto.constraints()) {
453 if (ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
454 continue;
455 }
456 if (ct.enforcement_literal().size() != 1) continue;
457 if (ct.linear().vars_size() != 1) continue;
458
459 // ct is a linear constraint with one term and one enforcement literal.
460 const sat::Literal enforcement_literal =
461 mapping->Literal(ct.enforcement_literal(0));
462 if (sat_solver->Assignment().LiteralIsFalse(enforcement_literal)) continue;
463
464 const int ref = ct.linear().vars(0);
465 const int var = PositiveRef(ref);
466
467 const Domain domain = ReadDomainFromProto(model_proto.variables(var));
468 const Domain domain_if_enforced =
469 ReadDomainFromProto(ct.linear())
470 .InverseMultiplicationBy(ct.linear().coeffs(0) *
471 (RefIsPositive(ref) ? 1 : -1));
472
473 if (domain_if_enforced.IsEmpty()) {
474 if (!sat_solver->AddUnitClause(enforcement_literal.Negated())) return;
475 continue;
476 }
477
478 // Detect enforcement_literal => (var >= value or var <= value).
479 if (domain_if_enforced.NumIntervals() == 1) {
480 if (domain_if_enforced.Max() >= domain.Max() &&
481 domain_if_enforced.Min() > domain.Min()) {
482 inequalities.push_back({&ct, enforcement_literal,
484 mapping->Integer(var),
485 IntegerValue(domain_if_enforced.Min()))});
486 } else if (domain_if_enforced.Min() <= domain.Min() &&
487 domain_if_enforced.Max() < domain.Max()) {
488 inequalities.push_back({&ct, enforcement_literal,
490 mapping->Integer(var),
491 IntegerValue(domain_if_enforced.Max()))});
492 }
493 }
494
495 // Detect implied bounds. The test is less strict than the above
496 // test.
497 if (domain_if_enforced.Min() > domain.Min()) {
498 implied_bounds->Add(
499 enforcement_literal,
501 mapping->Integer(var), IntegerValue(domain_if_enforced.Min())));
502 }
503 if (domain_if_enforced.Max() < domain.Max()) {
504 implied_bounds->Add(
505 enforcement_literal,
506 IntegerLiteral::LowerOrEqual(mapping->Integer(var),
507 IntegerValue(domain_if_enforced.Max())));
508 }
509
510 // Detect enforcement_literal => (var == value or var != value).
511 //
512 // Note that for domain with 2 values like [0, 1], we will detect both ==
513 // 0 and != 1. Similarly, for a domain in [min, max], we should both
514 // detect (== min) and (<= min), and both detect (== max) and (>= max).
515 {
516 const Domain inter = domain.IntersectionWith(domain_if_enforced);
517 if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
518 if (inter.Min() == 0) {
519 detector->ProcessConditionalZero(enforcement_literal,
520 mapping->Integer(var));
521 }
522 var_to_equalities[var].push_back(
523 {&ct, enforcement_literal, inter.Min(), true});
524 }
525 }
526 {
527 const Domain inter =
528 domain.IntersectionWith(domain_if_enforced.Complement());
529 if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
530 var_to_equalities[var].push_back(
531 {&ct, enforcement_literal, inter.Min(), false});
532 }
533 }
534 }
535
536 // Detect Literal <=> X >= value
537 int num_inequalities = 0;
538 std::sort(inequalities.begin(), inequalities.end());
539 for (int i = 0; i + 1 < inequalities.size(); i++) {
540 if (inequalities[i].literal != inequalities[i + 1].literal.Negated()) {
541 continue;
542 }
543
544 // TODO(user): In these cases, we could fix the enforcement literal right
545 // away or ignore the constraint. Note that it will be done later anyway
546 // though.
547 if (integer_trail->IntegerLiteralIsTrue(inequalities[i].i_lit) ||
548 integer_trail->IntegerLiteralIsFalse(inequalities[i].i_lit)) {
549 continue;
550 }
551 if (integer_trail->IntegerLiteralIsTrue(inequalities[i + 1].i_lit) ||
552 integer_trail->IntegerLiteralIsFalse(inequalities[i + 1].i_lit)) {
553 continue;
554 }
555
556 const auto pair_a = encoder->Canonicalize(inequalities[i].i_lit);
557 const auto pair_b = encoder->Canonicalize(inequalities[i + 1].i_lit);
558 if (pair_a.first == pair_b.second) {
559 ++num_inequalities;
560 encoder->AssociateToIntegerLiteral(inequalities[i].literal,
561 inequalities[i].i_lit);
562 mapping->already_loaded_ct_.insert(inequalities[i].ct);
563 mapping->already_loaded_ct_.insert(inequalities[i + 1].ct);
564 }
565 }
566
567 // Encode the half-inequalities.
568 int num_half_inequalities = 0;
569 for (const auto inequality : inequalities) {
570 if (mapping->ConstraintIsAlreadyLoaded(inequality.ct)) continue;
571 m->Add(
572 Implication(inequality.literal,
573 encoder->GetOrCreateAssociatedLiteral(inequality.i_lit)));
574 if (sat_solver->ModelIsUnsat()) return;
575
576 ++num_half_inequalities;
577 mapping->already_loaded_ct_.insert(inequality.ct);
578 mapping->is_half_encoding_ct_.insert(inequality.ct);
579 }
580 if (!inequalities.empty()) {
581 SOLVER_LOG(logger, "[Encoding] ", num_inequalities,
582 " literals associated to VAR >= value, and ",
583 num_half_inequalities, " half-associations.");
584 }
585
586 // Detect Literal <=> X == value and associate them in the IntegerEncoder.
587 //
588 // TODO(user): Fully encode variable that are almost fully encoded?
589 int num_equalities = 0;
590 int num_half_equalities = 0;
591 int num_fully_encoded = 0;
592 int num_partially_encoded = 0;
593 for (int i = 0; i < var_to_equalities.size(); ++i) {
594 std::vector<EqualityDetectionHelper>& encoding = var_to_equalities[i];
595 std::sort(encoding.begin(), encoding.end());
596 if (encoding.empty()) continue;
597
598 absl::flat_hash_set<int64_t> values;
599 const IntegerVariable var = mapping->integers_[i];
600 for (int j = 0; j + 1 < encoding.size(); j++) {
601 if ((encoding[j].value != encoding[j + 1].value) ||
602 (encoding[j].literal != encoding[j + 1].literal.Negated()) ||
603 (encoding[j].is_equality != true) ||
604 (encoding[j + 1].is_equality != false)) {
605 continue;
606 }
607
608 ++num_equalities;
609 encoder->AssociateToIntegerEqualValue(encoding[j].literal, var,
610 IntegerValue(encoding[j].value));
611 mapping->already_loaded_ct_.insert(encoding[j].ct);
612 mapping->already_loaded_ct_.insert(encoding[j + 1].ct);
613 values.insert(encoding[j].value);
614 }
615
616 // TODO(user): Try to remove it. Normally we caught UNSAT above, but
617 // tests are very flaky (it only happens in parallel). Keeping it there for
618 // the time being.
619 if (sat_solver->ModelIsUnsat()) return;
620
621 // Encode the half-equalities.
622 //
623 // TODO(user): delay this after PropagateEncodingFromEquivalenceRelations()?
624 // Otherwise we might create new Boolean variables for no reason. Note
625 // however, that in the presolve, we should only use the "representative" in
626 // linear constraints, so we should be fine.
627 for (const auto equality : encoding) {
628 if (mapping->ConstraintIsAlreadyLoaded(equality.ct)) continue;
629 if (equality.is_equality) {
630 // If we have just an half-equality, lets not create the <=> literal
631 // but just add two implications. If we don't create hole, we don't
632 // really need the reverse literal. This way it is also possible for
633 // the ExtractElementEncoding() to detect later that actually this
634 // literal is <=> to var == value, and this way we create one less
635 // Boolean for the same result.
636 //
637 // TODO(user): It is not 100% clear what is the best encoding and if
638 // we should create equivalent literal or rely on propagator instead
639 // to push bounds.
640 m->Add(Implication(
641 equality.literal,
642 encoder->GetOrCreateAssociatedLiteral(
643 IntegerLiteral::GreaterOrEqual(var, equality.value))));
644 m->Add(Implication(
645 equality.literal,
646 encoder->GetOrCreateAssociatedLiteral(
647 IntegerLiteral::LowerOrEqual(var, equality.value))));
648 } else {
649 const Literal eq = encoder->GetOrCreateLiteralAssociatedToEquality(
650 var, equality.value);
651 m->Add(Implication(equality.literal, eq.Negated()));
652 }
653
654 ++num_half_equalities;
655 mapping->already_loaded_ct_.insert(equality.ct);
656 mapping->is_half_encoding_ct_.insert(equality.ct);
657 }
658
659 // Update stats.
660 if (encoder->VariableIsFullyEncoded(var)) {
661 ++num_fully_encoded;
662 } else {
663 ++num_partially_encoded;
664 }
665 }
666
667 if (num_equalities > 0 || num_half_equalities > 0) {
668 SOLVER_LOG(logger, "[Encoding] ", num_equalities,
669 " literals associated to VAR == value, and ",
670 num_half_equalities, " half-associations.");
671 }
672 if (num_fully_encoded > 0) {
673 SOLVER_LOG(logger,
674 "[Encoding] num_fully_encoded_variables:", num_fully_encoded);
675 }
676 if (num_partially_encoded > 0) {
677 SOLVER_LOG(logger, "[Encoding] num_partially_encoded_variables:",
678 num_partially_encoded);
679 }
680}
681
682void ExtractElementEncoding(const CpModelProto& model_proto, Model* m) {
683 int num_element_encoded = 0;
684 auto* mapping = m->GetOrCreate<CpModelMapping>();
685 auto* logger = m->GetOrCreate<SolverLogger>();
686 auto* encoder = m->GetOrCreate<IntegerEncoder>();
687 auto* sat_solver = m->GetOrCreate<SatSolver>();
688 auto* implied_bounds = m->GetOrCreate<ImpliedBounds>();
689 auto* element_encodings = m->GetOrCreate<ElementEncodings>();
690
691 // Scan all exactly_one constraints and look for literal => var == value to
692 // detect element encodings.
693 int num_support_clauses = 0;
694 int num_dedicated_propagator = 0;
695 std::vector<Literal> clause;
696 std::vector<Literal> selectors;
697 std::vector<AffineExpression> exprs;
698 std::vector<AffineExpression> negated_exprs;
699 for (int c = 0; c < model_proto.constraints_size(); ++c) {
700 const ConstraintProto& ct = model_proto.constraints(c);
701 if (ct.constraint_case() != ConstraintProto::kExactlyOne) continue;
702
703 // Project the implied values onto each integer variable.
704 absl::btree_map<IntegerVariable, std::vector<ValueLiteralPair>>
705 var_to_value_literal_list;
706 for (const int l : ct.exactly_one().literals()) {
707 const Literal literal = mapping->Literal(l);
708 for (const auto& var_value : implied_bounds->GetImpliedValues(literal)) {
709 var_to_value_literal_list[var_value.first].push_back(
710 {var_value.second, literal});
711 }
712 }
713
714 // Used for logging only.
715 std::vector<IntegerVariable> encoded_variables;
716 std::string encoded_variables_str;
717
718 // Search for variable fully covered by the literals of the exactly_one.
719 for (auto& [var, encoding] : var_to_value_literal_list) {
720 if (encoding.size() < ct.exactly_one().literals_size()) {
721 VLOG(2) << "X" << var.value() << " has " << encoding.size()
722 << " implied values, and a domain of size "
724 ->InitialVariableDomain(var)
725 .Size();
726 continue;
727 }
728
729 // We use the order of literals of the exactly_one.
730 ++num_element_encoded;
731 element_encodings->Add(var, encoding, c);
732 if (VLOG_IS_ON(1)) {
733 encoded_variables.push_back(var);
734 absl::StrAppend(&encoded_variables_str, " X", var.value());
735 }
736
737 // Encode the holes propagation (but we don't create extra literal if they
738 // are not already there). If there are non-encoded values we also add the
739 // direct min/max propagation.
740 bool need_extra_propagation = false;
741 std::sort(encoding.begin(), encoding.end(),
743 for (int i = 0, j = 0; i < encoding.size(); i = j) {
744 j = i + 1;
745 const IntegerValue value = encoding[i].value;
746 while (j < encoding.size() && encoding[j].value == value) ++j;
747
748 if (j - i == 1) {
749 // Lets not create var >= value or var <= value if they do not exist.
750 if (!encoder->IsFixedOrHasAssociatedLiteral(
751 IntegerLiteral::GreaterOrEqual(var, value)) ||
752 !encoder->IsFixedOrHasAssociatedLiteral(
753 IntegerLiteral::LowerOrEqual(var, value))) {
754 need_extra_propagation = true;
755 continue;
756 }
757 encoder->AssociateToIntegerEqualValue(encoding[i].literal, var,
758 value);
759 } else {
760 // We do not create an extra literal if it doesn't exist.
761 if (encoder->GetAssociatedEqualityLiteral(var, value) ==
763 need_extra_propagation = true;
764 continue;
765 }
766
767 // If all literal supporting a value are false, then the value must be
768 // false. Note that such a clause is only useful if there are more
769 // than one literal supporting the value, otherwise we should already
770 // have detected the equivalence.
771 ++num_support_clauses;
772 clause.clear();
773 for (int k = i; k < j; ++k) clause.push_back(encoding[k].literal);
774 const Literal eq_lit =
775 encoder->GetOrCreateLiteralAssociatedToEquality(var, value);
776 clause.push_back(eq_lit.Negated());
777
778 // TODO(user): It should be safe otherwise the exactly_one will have
779 // duplicate literal, but I am not sure that if presolve is off we can
780 // assume that.
781 sat_solver->AddProblemClause(clause);
782 }
783 }
784 if (need_extra_propagation) {
785 ++num_dedicated_propagator;
786 selectors.clear();
787 exprs.clear();
788 negated_exprs.clear();
789 for (const auto [value, literal] : encoding) {
790 selectors.push_back(literal);
791 exprs.push_back(AffineExpression(value));
792 negated_exprs.push_back(AffineExpression(-value));
793 }
794 auto* constraint =
795 new GreaterThanAtLeastOneOfPropagator(var, exprs, selectors, {}, m);
797 m->TakeOwnership(constraint);
798
799 // And the <= side.
800 constraint = new GreaterThanAtLeastOneOfPropagator(
801 NegationOf(var), negated_exprs, selectors, {}, m);
803 m->TakeOwnership(constraint);
804 }
805 }
806 if (encoded_variables.size() > 1 && VLOG_IS_ON(1)) {
807 VLOG(1) << "exactly_one(" << c << ") encodes " << encoded_variables.size()
808 << " variables at the same time: " << encoded_variables_str;
809 }
810 }
811
812 if (num_element_encoded > 0) {
813 SOLVER_LOG(logger,
814 "[Encoding] num_element_encoding: ", num_element_encoded);
815 }
816 if (num_support_clauses > 0) {
817 SOLVER_LOG(logger, "[Encoding] Added ", num_support_clauses,
818 " element support clauses, and ", num_dedicated_propagator,
819 " dedicated propagators.");
820 }
821}
822
823void PropagateEncodingFromEquivalenceRelations(const CpModelProto& model_proto,
824 Model* m) {
825 auto* mapping = m->GetOrCreate<CpModelMapping>();
826 auto* encoder = m->GetOrCreate<IntegerEncoder>();
827 auto* sat_solver = m->GetOrCreate<SatSolver>();
828
829 // Loop over all constraints and find affine ones.
830 int64_t num_associations = 0;
831 int64_t num_set_to_false = 0;
832 for (const ConstraintProto& ct : model_proto.constraints()) {
833 if (!ct.enforcement_literal().empty()) continue;
834 if (ct.constraint_case() != ConstraintProto::kLinear) continue;
835 if (ct.linear().vars_size() != 2) continue;
836 if (!ConstraintIsEq(ct.linear())) continue;
837
838 const IntegerValue rhs(ct.linear().domain(0));
839
840 // Make sure the coefficient are positive.
841 IntegerVariable var1 = mapping->Integer(ct.linear().vars(0));
842 IntegerVariable var2 = mapping->Integer(ct.linear().vars(1));
843 IntegerValue coeff1(ct.linear().coeffs(0));
844 IntegerValue coeff2(ct.linear().coeffs(1));
845 if (coeff1 < 0) {
846 var1 = NegationOf(var1);
847 coeff1 = -coeff1;
848 }
849 if (coeff2 < 0) {
850 var2 = NegationOf(var2);
851 coeff2 = -coeff2;
852 }
853
854 // TODO(user): This is not supposed to happen, but apparently it did on
855 // once on routing_GCM_0001_sat.fzn. Investigate and fix.
856 if (coeff1 == 0 || coeff2 == 0) continue;
857
858 // We first map the >= literals.
859 // It is important to do that first, since otherwise mapping a == literal
860 // might creates the underlying >= and <= literals.
861 for (int i = 0; i < 2; ++i) {
862 for (const auto [value1, literal1] :
863 encoder->PartialGreaterThanEncoding(var1)) {
864 const IntegerValue bound2 = FloorRatio(rhs - value1 * coeff1, coeff2);
865 ++num_associations;
866 encoder->AssociateToIntegerLiteral(
867 literal1, IntegerLiteral::LowerOrEqual(var2, bound2));
868 }
869 std::swap(var1, var2);
870 std::swap(coeff1, coeff2);
871 }
872
873 // Same for the == literals.
874 //
875 // TODO(user): This is similar to LoadEquivalenceAC() for unreified
876 // constraints, but when the later is called, more encoding might have taken
877 // place.
878 for (int i = 0; i < 2; ++i) {
879 const auto copy = encoder->PartialDomainEncoding(var1);
880 for (const auto value_literal : copy) {
881 const IntegerValue value1 = value_literal.value;
882 const IntegerValue intermediate = rhs - value1 * coeff1;
883 if (intermediate % coeff2 != 0) {
884 // Using this function deals properly with UNSAT.
885 ++num_set_to_false;
886 if (!sat_solver->AddUnitClause(value_literal.literal.Negated())) {
887 return;
888 }
889 continue;
890 }
891 ++num_associations;
892 encoder->AssociateToIntegerEqualValue(value_literal.literal, var2,
893 intermediate / coeff2);
894 }
895 std::swap(var1, var2);
896 std::swap(coeff1, coeff2);
897 }
898 }
899
900 if (num_associations > 0) {
901 VLOG(1) << "Num associations from equivalences = " << num_associations;
902 }
903 if (num_set_to_false > 0) {
904 VLOG(1) << "Num literals set to false from equivalences = "
905 << num_set_to_false;
906 }
907}
908
909void DetectOptionalVariables(const CpModelProto& model_proto, Model* m) {
910 const SatParameters& parameters = *(m->GetOrCreate<SatParameters>());
911 if (!parameters.use_optional_variables()) return;
912 if (parameters.enumerate_all_solutions()) return;
913
914 // The variables from the objective cannot be marked as optional!
915 const int num_proto_variables = model_proto.variables_size();
916 std::vector<bool> already_seen(num_proto_variables, false);
917 if (model_proto.has_objective()) {
918 for (const int ref : model_proto.objective().vars()) {
919 already_seen[PositiveRef(ref)] = true;
920 }
921 }
922
923 // Compute for each variables the intersection of the enforcement literals
924 // of the constraints in which they appear.
925 //
926 // TODO(user): This deals with the simplest cases, but we could try to
927 // detect literals that implies all the constraints in which a variable
928 // appear to false. This can be done with a LCA computation in the tree of
929 // Boolean implication (once the presolve remove cycles). Not sure if we can
930 // properly exploit that afterwards though. Do some research!
931 std::vector<std::vector<int>> enforcement_intersection(num_proto_variables);
932 absl::btree_set<int> literals_set;
933 for (int c = 0; c < model_proto.constraints_size(); ++c) {
934 const ConstraintProto& ct = model_proto.constraints(c);
935 if (ct.enforcement_literal().empty()) {
936 for (const int var : UsedVariables(ct)) {
937 already_seen[var] = true;
938 enforcement_intersection[var].clear();
939 }
940 } else {
941 literals_set.clear();
942 literals_set.insert(ct.enforcement_literal().begin(),
943 ct.enforcement_literal().end());
944 for (const int var : UsedVariables(ct)) {
945 if (!already_seen[var]) {
946 enforcement_intersection[var].assign(ct.enforcement_literal().begin(),
947 ct.enforcement_literal().end());
948 } else {
949 // Take the intersection.
950 std::vector<int>& vector_ref = enforcement_intersection[var];
951 int new_size = 0;
952 for (const int literal : vector_ref) {
953 if (literals_set.contains(literal)) {
954 vector_ref[new_size++] = literal;
955 }
956 }
957 vector_ref.resize(new_size);
958 }
959 already_seen[var] = true;
960 }
961 }
962 }
963
964 // Auto-detect optional variables.
965 int num_optionals = 0;
966 for (int var = 0; var < num_proto_variables; ++var) {
967 const IntegerVariableProto& var_proto = model_proto.variables(var);
968 const int64_t min = var_proto.domain(0);
969 const int64_t max = var_proto.domain(var_proto.domain().size() - 1);
970 if (min == max) continue;
971 if (min == 0 && max == 1) continue;
972 if (enforcement_intersection[var].empty()) continue;
973
974 ++num_optionals;
975 }
976
977 if (num_optionals > 0) {
978 SOLVER_LOG(m->GetOrCreate<SolverLogger>(), "Auto-detected ", num_optionals,
979 " optional variables. Note that for now we DO NOT do anything "
980 "with this information.");
981 }
982}
983
984void AddFullEncodingFromSearchBranching(const CpModelProto& model_proto,
985 Model* m) {
986 if (model_proto.search_strategy().empty()) return;
987
988 auto* mapping = m->GetOrCreate<CpModelMapping>();
989 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
990 for (const DecisionStrategyProto& strategy : model_proto.search_strategy()) {
991 if (strategy.domain_reduction_strategy() ==
992 DecisionStrategyProto::SELECT_MEDIAN_VALUE) {
993 for (const LinearExpressionProto& expr : strategy.exprs()) {
994 const int var = expr.vars(0);
995 if (!mapping->IsInteger(var)) continue;
996 const IntegerVariable variable = mapping->Integer(var);
997 if (!integer_trail->IsFixed(variable)) {
998 m->Add(FullyEncodeVariable(variable));
999 }
1000 }
1001 }
1002 }
1003}
1004
1005// ============================================================================
1006// Constraint loading functions.
1007// ============================================================================
1008
1009void LoadBoolOrConstraint(const ConstraintProto& ct, Model* m) {
1010 auto* mapping = m->GetOrCreate<CpModelMapping>();
1011 auto* sat_solver = m->GetOrCreate<SatSolver>();
1012 std::vector<Literal> literals = mapping->Literals(ct.bool_or().literals());
1013 for (const int ref : ct.enforcement_literal()) {
1014 literals.push_back(mapping->Literal(ref).Negated());
1015 }
1016 sat_solver->AddProblemClause(literals);
1017 if (literals.size() == 3) {
1018 m->GetOrCreate<ProductDetector>()->ProcessTernaryClause(literals);
1019 }
1020}
1021
1022void LoadBoolAndConstraint(const ConstraintProto& ct, Model* m) {
1023 auto* mapping = m->GetOrCreate<CpModelMapping>();
1024 std::vector<Literal> literals;
1025 for (const int ref : ct.enforcement_literal()) {
1026 literals.push_back(mapping->Literal(ref).Negated());
1027 }
1028 auto* sat_solver = m->GetOrCreate<SatSolver>();
1029 for (const Literal literal : mapping->Literals(ct.bool_and().literals())) {
1030 literals.push_back(literal);
1031 sat_solver->AddProblemClause(literals);
1032 literals.pop_back();
1033 }
1034}
1035
1036void LoadAtMostOneConstraint(const ConstraintProto& ct, Model* m) {
1037 auto* mapping = m->GetOrCreate<CpModelMapping>();
1038 auto* implications = m->GetOrCreate<BinaryImplicationGraph>();
1039 CHECK(!HasEnforcementLiteral(ct)) << "Not supported.";
1040 if (!implications->AddAtMostOne(
1041 mapping->Literals(ct.at_most_one().literals()))) {
1042 m->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1043 }
1044}
1045
1046void LoadExactlyOneConstraint(const ConstraintProto& ct, Model* m) {
1047 auto* mapping = m->GetOrCreate<CpModelMapping>();
1048 CHECK(!HasEnforcementLiteral(ct)) << "Not supported.";
1049 const auto& literals = mapping->Literals(ct.exactly_one().literals());
1050 m->Add(ExactlyOneConstraint(literals));
1051 if (literals.size() == 3) {
1052 m->GetOrCreate<ProductDetector>()->ProcessTernaryExactlyOne(literals);
1053 }
1054}
1055
1056void 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
1062namespace {
1063
1064// Boolean encoding of:
1065// enforcement_literal => coeff1 * var1 + coeff2 * var2 == rhs;
1066void 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 const auto copy = encoder->FullDomainEncoding(var2);
1079 for (const auto value_literal : copy) {
1080 const IntegerValue target = rhs - value_literal.value * coeff2;
1081 if (!term1_value_to_literal.contains(target)) {
1082 m->Add(EnforcedClause(enforcement_literal,
1083 {value_literal.literal.Negated()}));
1084 } else {
1085 const Literal target_literal = term1_value_to_literal[target];
1086 m->Add(EnforcedClause(enforcement_literal,
1087 {value_literal.literal.Negated(), target_literal}));
1088 m->Add(EnforcedClause(enforcement_literal,
1089 {value_literal.literal, target_literal.Negated()}));
1090
1091 // This "target" can never be reached again, so it is safe to remove it.
1092 // We do that so we know the term1 values that are never reached.
1093 term1_value_to_literal.erase(target);
1094 }
1095 }
1096
1097 // Exclude the values that can never be "matched" by coeff2 * var2.
1098 // We need the std::sort() to be deterministic!
1099 std::vector<Literal> implied_false;
1100 for (const auto entry : term1_value_to_literal) {
1101 implied_false.push_back(entry.second);
1102 }
1103 std::sort(implied_false.begin(), implied_false.end());
1104 for (const Literal l : implied_false) {
1105 m->Add(EnforcedClause(enforcement_literal, {l.Negated()}));
1106 }
1107}
1108
1109// Boolean encoding of:
1110// enforcement_literal => coeff1 * var1 + coeff2 * var2 != rhs;
1111void LoadEquivalenceNeqAC(const std::vector<Literal> enforcement_literal,
1112 IntegerValue coeff1, IntegerVariable var1,
1113 IntegerValue coeff2, IntegerVariable var2,
1114 const IntegerValue rhs, Model* m) {
1115 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1116 CHECK(encoder->VariableIsFullyEncoded(var1));
1117 CHECK(encoder->VariableIsFullyEncoded(var2));
1118 absl::flat_hash_map<IntegerValue, Literal> term1_value_to_literal;
1119 for (const auto value_literal : encoder->FullDomainEncoding(var1)) {
1120 term1_value_to_literal[coeff1 * value_literal.value] =
1121 value_literal.literal;
1122 }
1123 const auto copy = encoder->FullDomainEncoding(var2);
1124 for (const auto value_literal : copy) {
1125 const IntegerValue target_value = rhs - value_literal.value * coeff2;
1126 const auto& it = term1_value_to_literal.find(target_value);
1127 if (it != term1_value_to_literal.end()) {
1128 const Literal target_literal = it->second;
1129 m->Add(EnforcedClause(
1130 enforcement_literal,
1131 {value_literal.literal.Negated(), target_literal.Negated()}));
1132 }
1133 }
1134}
1135
1136bool IsPartOfProductEncoding(const ConstraintProto& ct) {
1137 if (ct.enforcement_literal().size() != 1) return false;
1138 if (ct.linear().vars().size() > 2) return false;
1139 if (ct.linear().domain().size() != 2) return false;
1140 if (ct.linear().domain(0) != 0) return false;
1141 if (ct.linear().domain(1) != 0) return false;
1142 for (const int64_t coeff : ct.linear().coeffs()) {
1143 if (std::abs(coeff) != 1) return false;
1144 }
1145 return true;
1146}
1147
1148} // namespace
1149
1150// TODO(user): We could use a smarter way to determine buckets, like putting
1151// everyone with the same coeff together if possible and the split is ok.
1152void SplitAndLoadIntermediateConstraints(bool lb_required, bool ub_required,
1153 std::vector<IntegerVariable>* vars,
1154 std::vector<int64_t>* coeffs,
1155 Model* m) {
1156 // If we enumerate all solutions, then we want intermediate variables to be
1157 // tight independently of what side is required.
1158 if (m->GetOrCreate<SatParameters>()->enumerate_all_solutions()) {
1159 lb_required = true;
1160 ub_required = true;
1161 }
1162
1163 std::vector<IntegerVariable> bucket_sum_vars;
1164 std::vector<int64_t> bucket_sum_coeffs;
1165 std::vector<IntegerVariable> local_vars;
1166 std::vector<int64_t> local_coeffs;
1167
1168 int64_t i = 0;
1169 const int64_t num_vars = vars->size();
1170 const int64_t num_buckets = static_cast<int>(std::round(std::sqrt(num_vars)));
1171 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1172 for (int64_t b = 0; b < num_buckets; ++b) {
1173 local_vars.clear();
1174 local_coeffs.clear();
1175 int64_t bucket_lb = 0;
1176 int64_t bucket_ub = 0;
1177 int64_t gcd = 0;
1178 const int64_t limit = num_vars * (b + 1);
1179 for (; i * num_buckets < limit; ++i) {
1180 const IntegerVariable var = (*vars)[i];
1181 const int64_t coeff = (*coeffs)[i];
1182 gcd = std::gcd(gcd, std::abs(coeff));
1183 local_vars.push_back(var);
1184 local_coeffs.push_back(coeff);
1185 const int64_t term1 = coeff * integer_trail->LowerBound(var).value();
1186 const int64_t term2 = coeff * integer_trail->UpperBound(var).value();
1187 bucket_lb += std::min(term1, term2);
1188 bucket_ub += std::max(term1, term2);
1189 }
1190 if (gcd == 0) continue;
1191 if (gcd > 1) {
1192 // Everything should be exactly divisible!
1193 for (int64_t& ref : local_coeffs) ref /= gcd;
1194 bucket_lb /= gcd;
1195 bucket_ub /= gcd;
1196 }
1197
1198 const IntegerVariable bucket_sum =
1199 integer_trail->AddIntegerVariable(bucket_lb, bucket_ub);
1200 bucket_sum_vars.push_back(bucket_sum);
1201 bucket_sum_coeffs.push_back(gcd);
1202 local_vars.push_back(bucket_sum);
1203 local_coeffs.push_back(-1);
1204
1205 if (lb_required) {
1206 // We have sum bucket_var >= lb, so we need local_vars >= bucket_var.
1207 m->Add(WeightedSumGreaterOrEqual(local_vars, local_coeffs, 0));
1208 }
1209 if (ub_required) {
1210 // Similarly, bucket_var <= ub, so we need local_vars <= bucket_var
1211 m->Add(WeightedSumLowerOrEqual(local_vars, local_coeffs, 0));
1212 }
1213 }
1214 *vars = bucket_sum_vars;
1215 *coeffs = bucket_sum_coeffs;
1216}
1217
1218void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
1219 auto* mapping = m->GetOrCreate<CpModelMapping>();
1221 if (ct.linear().vars().empty()) {
1222 const Domain rhs = ReadDomainFromProto(ct.linear());
1223 if (rhs.Contains(0)) return;
1224 if (HasEnforcementLiteral(ct)) {
1225 std::vector<Literal> clause;
1226 for (const int ref : ct.enforcement_literal()) {
1227 clause.push_back(mapping->Literal(ref).Negated());
1228 }
1229 m->Add(ClauseConstraint(clause));
1230 } else {
1231 VLOG(1) << "Trivially UNSAT constraint: " << ct;
1232 m->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1233 }
1234 return;
1235 }
1236
1237 if (IsPartOfProductEncoding(ct)) {
1238 const Literal l = mapping->Literal(ct.enforcement_literal(0));
1239 auto* detector = m->GetOrCreate<ProductDetector>();
1240 if (ct.linear().vars().size() == 1) {
1241 // TODO(user): Actually this should never be called since we process
1242 // linear1 in ExtractEncoding().
1243 detector->ProcessConditionalZero(l,
1244 mapping->Integer(ct.linear().vars(0)));
1245 } else if (ct.linear().vars().size() == 2) {
1246 const IntegerVariable x = mapping->Integer(ct.linear().vars(0));
1247 const IntegerVariable y = mapping->Integer(ct.linear().vars(1));
1248 detector->ProcessConditionalEquality(
1249 l, x,
1250 ct.linear().coeffs(0) == ct.linear().coeffs(1) ? NegationOf(y) : y);
1251 }
1252 }
1253
1254 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1255 std::vector<IntegerVariable> vars = mapping->Integers(ct.linear().vars());
1256 std::vector<int64_t> coeffs = ValuesFromProto(ct.linear().coeffs());
1257
1258 // Compute the min/max to relax the bounds if needed.
1259 //
1260 // TODO(user): Reuse ComputeLinearBounds()? but then we need another loop
1261 // to detect if we only have Booleans.
1262 IntegerValue min_sum(0);
1263 IntegerValue max_sum(0);
1264 IntegerValue max_domain_size(0);
1265 bool all_booleans = true;
1266 for (int i = 0; i < vars.size(); ++i) {
1267 if (all_booleans && !mapping->IsBoolean(ct.linear().vars(i))) {
1268 all_booleans = false;
1269 }
1270 const IntegerValue lb = integer_trail->LowerBound(vars[i]);
1271 const IntegerValue ub = integer_trail->UpperBound(vars[i]);
1272 max_domain_size = std::max(max_domain_size, ub - lb + 1);
1273 const IntegerValue term_a = coeffs[i] * lb;
1274 const IntegerValue term_b = coeffs[i] * ub;
1275 min_sum += std::min(term_a, term_b);
1276 max_sum += std::max(term_a, term_b);
1277 }
1278
1279 // Load conditional precedences.
1280 const SatParameters& params = *m->GetOrCreate<SatParameters>();
1281 if (params.auto_detect_greater_than_at_least_one_of() &&
1282 ct.enforcement_literal().size() == 1 && vars.size() <= 2) {
1283 // To avoid overflow in the code below, we tighten the bounds.
1284 int64_t rhs_min = ct.linear().domain(0);
1285 int64_t rhs_max = ct.linear().domain(ct.linear().domain().size() - 1);
1286 rhs_min = std::max(rhs_min, min_sum.value());
1287 rhs_max = std::min(rhs_max, max_sum.value());
1288
1289 auto* repository = m->GetOrCreate<BinaryRelationRepository>();
1290 const Literal lit = mapping->Literal(ct.enforcement_literal(0));
1291 const Domain domain = ReadDomainFromProto(ct.linear());
1292 if (vars.size() == 1) {
1293 repository->Add(lit, {vars[0], coeffs[0]}, {}, rhs_min, rhs_max);
1294 } else if (vars.size() == 2) {
1295 repository->Add(lit, {vars[0], coeffs[0]}, {vars[1], coeffs[1]}, rhs_min,
1296 rhs_max);
1297 }
1298 }
1299
1300 // Load precedences.
1301 if (!HasEnforcementLiteral(ct)) {
1302 auto* precedences = m->GetOrCreate<PrecedenceRelations>();
1303
1304 // To avoid overflow in the code below, we tighten the bounds.
1305 // Note that we detect and do not add trivial relation.
1306 int64_t rhs_min = ct.linear().domain(0);
1307 int64_t rhs_max = ct.linear().domain(ct.linear().domain().size() - 1);
1308 rhs_min = std::max(rhs_min, min_sum.value());
1309 rhs_max = std::min(rhs_max, max_sum.value());
1310
1311 if (vars.size() == 2) {
1312 if (std::abs(coeffs[0]) == std::abs(coeffs[1])) {
1313 const int64_t magnitude = std::abs(coeffs[0]);
1314 IntegerVariable v1 = vars[0];
1315 IntegerVariable v2 = vars[1];
1316 if (coeffs[0] < 0) v1 = NegationOf(v1);
1317 if (coeffs[1] > 0) v2 = NegationOf(v2);
1318
1319 // magnitude * v1 <= magnitude * v2 + rhs_max.
1320 precedences->Add(v1, v2, MathUtil::CeilOfRatio(-rhs_max, magnitude));
1321
1322 // magnitude * v1 >= magnitude * v2 + rhs_min.
1323 precedences->Add(v2, v1, MathUtil::CeilOfRatio(rhs_min, magnitude));
1324 }
1325 } else if (vars.size() == 3) {
1326 for (int i = 0; i < 3; ++i) {
1327 for (int j = 0; j < 3; ++j) {
1328 if (i == j) continue;
1329 if (std::abs(coeffs[i]) != std::abs(coeffs[j])) continue;
1330 const int other = 3 - i - j; // i + j + other = 0 + 1 + 2.
1331
1332 // Make the terms magnitude * v1 - magnitude * v2 ...
1333 const int64_t magnitude = std::abs(coeffs[i]);
1334 IntegerVariable v1 = vars[i];
1335 IntegerVariable v2 = vars[j];
1336 if (coeffs[i] < 0) v1 = NegationOf(v1);
1337 if (coeffs[j] > 0) v2 = NegationOf(v2);
1338
1339 // magnitude * v1 + other_lb <= magnitude * v2 + rhs_max
1340 const int64_t coeff = coeffs[other];
1341 const int64_t other_lb =
1342 coeff > 0
1343 ? coeff * integer_trail->LowerBound(vars[other]).value()
1344 : coeff * integer_trail->UpperBound(vars[other]).value();
1345 precedences->Add(
1346 v1, v2, MathUtil::CeilOfRatio(other_lb - rhs_max, magnitude));
1347
1348 // magnitude * v1 + other_ub >= magnitude * v2 + rhs_min
1349 const int64_t other_ub =
1350 coeff > 0
1351 ? coeff * integer_trail->UpperBound(vars[other]).value()
1352 : coeff * integer_trail->LowerBound(vars[other]).value();
1353 precedences->Add(
1354 v2, v1, MathUtil::CeilOfRatio(rhs_min - other_ub, magnitude));
1355 }
1356 }
1357 }
1358 }
1359
1360 const IntegerValue domain_size_limit(
1361 params.max_domain_size_when_encoding_eq_neq_constraints());
1362 if (ct.linear().vars_size() == 2 && !integer_trail->IsFixed(vars[0]) &&
1363 !integer_trail->IsFixed(vars[1]) &&
1364 max_domain_size <= domain_size_limit) {
1365 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1366 if (params.boolean_encoding_level() > 0 && ConstraintIsEq(ct.linear()) &&
1367 ct.linear().domain(0) != min_sum && ct.linear().domain(0) != max_sum &&
1368 encoder->VariableIsFullyEncoded(vars[0]) &&
1369 encoder->VariableIsFullyEncoded(vars[1])) {
1370 VLOG(3) << "Load AC version of " << ct << ", var0 domain = "
1371 << integer_trail->InitialVariableDomain(vars[0])
1372 << ", var1 domain = "
1373 << integer_trail->InitialVariableDomain(vars[1]);
1374 return LoadEquivalenceAC(mapping->Literals(ct.enforcement_literal()),
1375 IntegerValue(coeffs[0]), vars[0],
1376 IntegerValue(coeffs[1]), vars[1],
1377 IntegerValue(ct.linear().domain(0)), m);
1378 }
1379
1380 int64_t single_value = 0;
1381 if (params.boolean_encoding_level() > 0 &&
1382 ConstraintIsNEq(ct.linear(), mapping, integer_trail, &single_value) &&
1383 single_value != min_sum && single_value != max_sum &&
1384 encoder->VariableIsFullyEncoded(vars[0]) &&
1385 encoder->VariableIsFullyEncoded(vars[1])) {
1386 VLOG(3) << "Load NAC version of " << ct << ", var0 domain = "
1387 << integer_trail->InitialVariableDomain(vars[0])
1388 << ", var1 domain = "
1389 << integer_trail->InitialVariableDomain(vars[1])
1390 << ", value = " << single_value;
1391 return LoadEquivalenceNeqAC(mapping->Literals(ct.enforcement_literal()),
1392 IntegerValue(coeffs[0]), vars[0],
1393 IntegerValue(coeffs[1]), vars[1],
1394 IntegerValue(single_value), m);
1395 }
1396 }
1397
1398 // Note that the domain/enforcement of the main constraint do not change.
1399 // Same for the min/sum and max_sum. The intermediate variables are always
1400 // equal to the intermediate sum, independently of the enforcement.
1401 const bool pseudo_boolean = !HasEnforcementLiteral(ct) &&
1402 ct.linear().domain_size() == 2 && all_booleans;
1403 if (!pseudo_boolean &&
1404 ct.linear().vars().size() > params.linear_split_size()) {
1405 const auto& domain = ct.linear().domain();
1407 domain.size() > 2 || min_sum < domain[0],
1408 domain.size() > 2 || max_sum > domain[1], &vars, &coeffs, m);
1409 }
1410
1411 if (ct.linear().domain_size() == 2) {
1412 const int64_t lb = ct.linear().domain(0);
1413 const int64_t ub = ct.linear().domain(1);
1414 const std::vector<Literal> enforcement_literals =
1415 mapping->Literals(ct.enforcement_literal());
1416 if (all_booleans && enforcement_literals.empty()) {
1417 // TODO(user): we should probably also implement an
1418 // half-reified version of this constraint.
1419 std::vector<LiteralWithCoeff> cst;
1420 for (int i = 0; i < vars.size(); ++i) {
1421 const int ref = ct.linear().vars(i);
1422 cst.push_back({mapping->Literal(ref), coeffs[i]});
1423 }
1424 m->GetOrCreate<SatSolver>()->AddLinearConstraint(
1425 /*use_lower_bound=*/(min_sum < lb), lb,
1426 /*use_upper_bound=*/(max_sum > ub), ub, &cst);
1427 } else {
1428 if (min_sum < lb) {
1429 AddWeightedSumGreaterOrEqual(enforcement_literals, vars, coeffs, lb, m);
1430 }
1431 if (max_sum > ub) {
1432 AddWeightedSumLowerOrEqual(enforcement_literals, vars, coeffs, ub, m);
1433 }
1434 }
1435 return;
1436 }
1437
1438 // We have a linear with a complex Domain, we need to create extra Booleans.
1439
1440 // For enforcement => var \in domain, we can potentially reuse the encoding
1441 // literal directly rather than creating new ones.
1442 const bool is_linear1 = vars.size() == 1 && coeffs[0] == 1;
1443
1444 bool special_case = false;
1445 std::vector<Literal> clause;
1446 std::vector<Literal> for_enumeration;
1447 auto* encoding = m->GetOrCreate<IntegerEncoder>();
1448 const int domain_size = ct.linear().domain_size();
1449 for (int i = 0; i < domain_size; i += 2) {
1450 const int64_t lb = ct.linear().domain(i);
1451 const int64_t ub = ct.linear().domain(i + 1);
1452
1453 // Skip non-reachable intervals.
1454 if (min_sum > ub) continue;
1455 if (max_sum < lb) continue;
1456
1457 // Skip trivial constraint. Note that when this happens, all the intervals
1458 // before where non-reachable.
1459 if (min_sum >= lb && max_sum <= ub) return;
1460
1461 if (is_linear1) {
1462 if (lb == ub) {
1463 clause.push_back(
1464 encoding->GetOrCreateLiteralAssociatedToEquality(vars[0], lb));
1465 continue;
1466 } else if (min_sum >= lb) {
1467 clause.push_back(encoding->GetOrCreateAssociatedLiteral(
1468 IntegerLiteral::LowerOrEqual(vars[0], ub)));
1469 continue;
1470 } else if (max_sum <= ub) {
1471 clause.push_back(encoding->GetOrCreateAssociatedLiteral(
1472 IntegerLiteral::GreaterOrEqual(vars[0], lb)));
1473 continue;
1474 }
1475 }
1476
1477 // If there is just two terms and no enforcement, we don't need to create an
1478 // extra boolean as the second case can be controlled by the negation of the
1479 // first.
1480 if (ct.enforcement_literal().empty() && clause.size() == 1 &&
1481 i + 1 == domain_size) {
1482 special_case = true;
1483 }
1484
1485 const Literal subdomain_literal(
1486 special_case ? clause.back().Negated()
1487 : Literal(m->Add(NewBooleanVariable()), true));
1488 clause.push_back(subdomain_literal);
1489 for_enumeration.push_back(subdomain_literal);
1490
1491 if (min_sum < lb) {
1492 AddWeightedSumGreaterOrEqual({subdomain_literal}, vars, coeffs, lb, m);
1493 }
1494 if (max_sum > ub) {
1495 AddWeightedSumLowerOrEqual({subdomain_literal}, vars, coeffs, ub, m);
1496 }
1497 }
1498
1499 const std::vector<Literal> enforcement_literals =
1500 mapping->Literals(ct.enforcement_literal());
1501
1502 // Make sure all booleans are tights when enumerating all solutions.
1503 if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
1504 Literal linear_is_enforced;
1505 if (enforcement_literals.size() == 1) {
1506 linear_is_enforced = enforcement_literals[0];
1507 } else {
1508 linear_is_enforced = Literal(m->Add(NewBooleanVariable()), true);
1509 std::vector<Literal> maintain_linear_is_enforced;
1510 for (const Literal e_lit : enforcement_literals) {
1511 m->Add(Implication(e_lit.Negated(), linear_is_enforced.Negated()));
1512 maintain_linear_is_enforced.push_back(e_lit.Negated());
1513 }
1514 maintain_linear_is_enforced.push_back(linear_is_enforced);
1515 m->Add(ClauseConstraint(maintain_linear_is_enforced));
1516 }
1517 for (const Literal lit : for_enumeration) {
1518 m->Add(Implication(linear_is_enforced.Negated(), lit.Negated()));
1519 if (special_case) break; // For the unique Boolean var to be false.
1520 }
1521 }
1522
1523 if (!special_case) {
1524 for (const Literal e_lit : enforcement_literals) {
1525 clause.push_back(e_lit.Negated());
1526 }
1527 m->Add(ClauseConstraint(clause));
1528 }
1529}
1530
1531void LoadAllDiffConstraint(const ConstraintProto& ct, Model* m) {
1532 auto* mapping = m->GetOrCreate<CpModelMapping>();
1533 const std::vector<AffineExpression> expressions =
1534 mapping->Affines(ct.all_diff().exprs());
1535 m->Add(AllDifferentOnBounds(expressions));
1536}
1537
1538void LoadIntProdConstraint(const ConstraintProto& ct, Model* m) {
1539 auto* mapping = m->GetOrCreate<CpModelMapping>();
1540 const AffineExpression prod = mapping->Affine(ct.int_prod().target());
1541 std::vector<AffineExpression> terms;
1542 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
1543 terms.push_back(mapping->Affine(expr));
1544 }
1545 switch (terms.size()) {
1546 case 0: {
1547 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1548 auto* sat_solver = m->GetOrCreate<SatSolver>();
1549 if (prod.IsConstant()) {
1550 if (prod.constant.value() != 1) {
1551 sat_solver->NotifyThatModelIsUnsat();
1552 }
1553 } else {
1554 if (!integer_trail->Enqueue(prod.LowerOrEqual(1)) ||
1555 !integer_trail->Enqueue(prod.GreaterOrEqual(1))) {
1556 sat_solver->NotifyThatModelIsUnsat();
1557 }
1558 }
1559 break;
1560 }
1561 case 1: {
1562 LinearConstraintBuilder builder(m, /*lb=*/0, /*ub=*/0);
1563 builder.AddTerm(prod, 1);
1564 builder.AddTerm(terms[0], -1);
1565 LoadLinearConstraint(builder.Build(), m);
1566 break;
1567 }
1568 case 2: {
1569 m->Add(ProductConstraint(terms[0], terms[1], prod));
1570 break;
1571 }
1572 default: {
1573 LOG(FATAL) << "Loading int_prod with arity > 2, should not be here.";
1574 break;
1575 }
1576 }
1577}
1578
1579void LoadIntDivConstraint(const ConstraintProto& ct, Model* m) {
1580 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1581 auto* mapping = m->GetOrCreate<CpModelMapping>();
1582 const AffineExpression div = mapping->Affine(ct.int_div().target());
1583 const AffineExpression num = mapping->Affine(ct.int_div().exprs(0));
1584 const AffineExpression denom = mapping->Affine(ct.int_div().exprs(1));
1585 if (integer_trail->IsFixed(denom)) {
1586 m->Add(FixedDivisionConstraint(num, integer_trail->FixedValue(denom), div));
1587 } else {
1588 if (VLOG_IS_ON(1)) {
1589 LinearConstraintBuilder builder(m);
1590 if (m->GetOrCreate<ProductDecomposer>()->TryToLinearize(num, denom,
1591 &builder)) {
1592 VLOG(1) << "Division " << ct << " can be linearized";
1593 }
1594 }
1595 m->Add(DivisionConstraint(num, denom, div));
1596 }
1597}
1598
1599void LoadIntModConstraint(const ConstraintProto& ct, Model* m) {
1600 auto* mapping = m->GetOrCreate<CpModelMapping>();
1601 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1602
1603 const AffineExpression target = mapping->Affine(ct.int_mod().target());
1604 const AffineExpression expr = mapping->Affine(ct.int_mod().exprs(0));
1605 const AffineExpression mod = mapping->Affine(ct.int_mod().exprs(1));
1606 CHECK(integer_trail->IsFixed(mod));
1607 const IntegerValue fixed_modulo = integer_trail->FixedValue(mod);
1608 m->Add(FixedModuloConstraint(expr, fixed_modulo, target));
1609}
1610
1611void LoadLinMaxConstraint(const ConstraintProto& ct, Model* m) {
1612 if (ct.lin_max().exprs().empty()) {
1613 m->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1614 return;
1615 }
1616
1617 auto* mapping = m->GetOrCreate<CpModelMapping>();
1618 const LinearExpression max = mapping->GetExprFromProto(ct.lin_max().target());
1619 std::vector<LinearExpression> negated_exprs;
1620 negated_exprs.reserve(ct.lin_max().exprs_size());
1621 for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
1622 negated_exprs.push_back(
1623 NegationOf(mapping->GetExprFromProto(ct.lin_max().exprs(i))));
1624 }
1625 // TODO(user): Consider replacing the min propagator by max.
1626 m->Add(IsEqualToMinOf(NegationOf(max), negated_exprs));
1627}
1628
1629void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m) {
1630 auto* mapping = m->GetOrCreate<CpModelMapping>();
1631 AddDisjunctive(mapping->Intervals(ct.no_overlap().intervals()), m);
1632}
1633
1634void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m) {
1635 if (ct.no_overlap_2d().x_intervals().empty()) return;
1636 auto* mapping = m->GetOrCreate<CpModelMapping>();
1637 const std::vector<IntervalVariable> x_intervals =
1638 mapping->Intervals(ct.no_overlap_2d().x_intervals());
1639 const std::vector<IntervalVariable> y_intervals =
1640 mapping->Intervals(ct.no_overlap_2d().y_intervals());
1641 AddNonOverlappingRectangles(x_intervals, y_intervals, m);
1642}
1643
1644void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m) {
1645 auto* mapping = m->GetOrCreate<CpModelMapping>();
1646 const std::vector<IntervalVariable> intervals =
1647 mapping->Intervals(ct.cumulative().intervals());
1648 const AffineExpression capacity = mapping->Affine(ct.cumulative().capacity());
1649 const std::vector<AffineExpression> demands =
1650 mapping->Affines(ct.cumulative().demands());
1651 m->Add(Cumulative(intervals, demands, capacity));
1652}
1653
1654void LoadReservoirConstraint(const ConstraintProto& ct, Model* m) {
1655 auto* mapping = m->GetOrCreate<CpModelMapping>();
1656 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1657 const std::vector<AffineExpression> times =
1658 mapping->Affines(ct.reservoir().time_exprs());
1659 const std::vector<AffineExpression> level_changes =
1660 mapping->Affines(ct.reservoir().level_changes());
1661 std::vector<Literal> presences;
1662 const int size = ct.reservoir().time_exprs().size();
1663 for (int i = 0; i < size; ++i) {
1664 if (!ct.reservoir().active_literals().empty()) {
1665 presences.push_back(mapping->Literal(ct.reservoir().active_literals(i)));
1666 } else {
1667 presences.push_back(encoder->GetTrueLiteral());
1668 }
1669 }
1670 AddReservoirConstraint(times, level_changes, presences,
1671 ct.reservoir().min_level(), ct.reservoir().max_level(),
1672 m);
1673}
1674
1675void LoadCircuitConstraint(const ConstraintProto& ct, Model* m) {
1676 const auto& circuit = ct.circuit();
1677 if (circuit.tails().empty()) return;
1678
1679 std::vector<int> tails(circuit.tails().begin(), circuit.tails().end());
1680 std::vector<int> heads(circuit.heads().begin(), circuit.heads().end());
1681 std::vector<Literal> literals =
1682 m->GetOrCreate<CpModelMapping>()->Literals(circuit.literals());
1683 const int num_nodes = ReindexArcs(&tails, &heads);
1684 LoadSubcircuitConstraint(num_nodes, tails, heads, literals, m);
1685}
1686
1687void LoadRoutesConstraint(const ConstraintProto& ct, Model* m) {
1688 const auto& routes = ct.routes();
1689 if (routes.tails().empty()) return;
1690
1691 std::vector<int> tails(routes.tails().begin(), routes.tails().end());
1692 std::vector<int> heads(routes.heads().begin(), routes.heads().end());
1693 std::vector<Literal> literals =
1694 m->GetOrCreate<CpModelMapping>()->Literals(routes.literals());
1695 const int num_nodes = ReindexArcs(&tails, &heads);
1696 LoadSubcircuitConstraint(num_nodes, tails, heads, literals, m,
1697 /*multiple_subcircuit_through_zero=*/true);
1698}
1699
1700bool LoadConstraint(const ConstraintProto& ct, Model* m) {
1701 switch (ct.constraint_case()) {
1702 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1703 return true;
1704 case ConstraintProto::ConstraintCase::kBoolOr:
1705 LoadBoolOrConstraint(ct, m);
1706 return true;
1707 case ConstraintProto::ConstraintCase::kBoolAnd:
1708 LoadBoolAndConstraint(ct, m);
1709 return true;
1710 case ConstraintProto::ConstraintCase::kAtMostOne:
1712 return true;
1713 case ConstraintProto::ConstraintCase::kExactlyOne:
1715 return true;
1716 case ConstraintProto::ConstraintCase::kBoolXor:
1717 LoadBoolXorConstraint(ct, m);
1718 return true;
1719 case ConstraintProto::ConstraintProto::kLinear:
1720 LoadLinearConstraint(ct, m);
1721 return true;
1722 case ConstraintProto::ConstraintProto::kAllDiff:
1723 LoadAllDiffConstraint(ct, m);
1724 return true;
1725 case ConstraintProto::ConstraintProto::kIntProd:
1726 LoadIntProdConstraint(ct, m);
1727 return true;
1728 case ConstraintProto::ConstraintProto::kIntDiv:
1729 LoadIntDivConstraint(ct, m);
1730 return true;
1731 case ConstraintProto::ConstraintProto::kIntMod:
1732 LoadIntModConstraint(ct, m);
1733 return true;
1734 case ConstraintProto::ConstraintProto::kLinMax:
1735 LoadLinMaxConstraint(ct, m);
1736 return true;
1737 case ConstraintProto::ConstraintProto::kInterval:
1738 // Already dealt with.
1739 return true;
1740 case ConstraintProto::ConstraintProto::kNoOverlap:
1742 return true;
1743 case ConstraintProto::ConstraintProto::kNoOverlap2D:
1745 return true;
1746 case ConstraintProto::ConstraintProto::kCumulative:
1748 return true;
1749 case ConstraintProto::ConstraintProto::kReservoir:
1751 return true;
1752 case ConstraintProto::ConstraintProto::kCircuit:
1753 LoadCircuitConstraint(ct, m);
1754 return true;
1755 case ConstraintProto::ConstraintProto::kRoutes:
1756 LoadRoutesConstraint(ct, m);
1757 return true;
1758 default:
1759 return false;
1760 }
1761}
1762
1763} // namespace sat
1764} // namespace operations_research
Definition model.h:341
Domain IntersectionWith(const Domain &domain) const
bool Contains(int64_t value) const
Domain InverseMultiplicationBy(int64_t coeff) const
static IntegralType CeilOfRatio(IntegralType numerator, IntegralType denominator)
Definition mathutil.h:40
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
std::vector< AffineExpression > Affines(const List &list) const
bool Add(Literal literal, IntegerLiteral integer_literal)
void ReserveSpaceForNumVariables(int num_vars)
Definition integer.cc:822
LiteralIndex Index() const
Definition sat_base.h:91
BooleanVariable Variable() const
Definition sat_base.h:87
T Add(std::function< T(Model *)> f)
Definition model.h:87
bool AddProblemClause(absl::Span< const Literal > literals)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:58
std::function< std::vector< ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
Definition integer.h:1659
void LoadBoolXorConstraint(const ConstraintProto &ct, Model *m)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
void LoadCumulativeConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> LiteralXorIs(const std::vector< Literal > &literals, bool value)
Enforces the XOR of a set of literals to be equal to the given value.
void LoadLinMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadIntProdConstraint(const ConstraintProto &ct, Model *m)
void SplitAndLoadIntermediateConstraints(bool lb_required, bool ub_required, std::vector< IntegerVariable > *vars, std::vector< int64_t > *coeffs, Model *m)
std::function< void(Model *)> WeightedSumGreaterOrEqual(absl::Span< const IntegerVariable > vars, const VectorInt &coefficients, int64_t lower_bound)
Weighted sum >= constant.
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> ProductConstraint(AffineExpression a, AffineExpression b, AffineExpression p)
Adds the constraint: a * b = p.
void DetectOptionalVariables(const CpModelProto &model_proto, Model *m)
Automatically detect optional variables.
void LoadBoolOrConstraint(const ConstraintProto &ct, Model *m)
void LoadSubcircuitConstraint(int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, Model *model, bool multiple_subcircuit_through_zero)
Definition circuit.cc:650
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition sat_solver.h:947
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
enforcement_literals => clause.
Definition sat_solver.h:987
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition integer.h:1477
std::function< void(Model *)> FixedDivisionConstraint(AffineExpression a, IntegerValue b, AffineExpression c)
Adds the constraint: a / b = c where b is a constant.
bool HasEnforcementLiteral(const ConstraintProto &ct)
Small utility functions to deal with half-reified constraints.
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
void LoadVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
std::function< void(Model *)> IsEqualToMinOf(const LinearExpression &min_expr, const std::vector< LinearExpression > &exprs)
void LoadIntModConstraint(const ConstraintProto &ct, Model *m)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> Implication(absl::Span< const Literal > enforcement_literals, IntegerLiteral i)
Definition integer.h:1609
const IntervalVariable kNoIntervalVariable(-1)
void LoadBooleanSymmetries(const CpModelProto &model_proto, Model *m)
std::function< void(Model *)> DivisionConstraint(AffineExpression num, AffineExpression denom, AffineExpression div)
Adds the constraint: num / denom = div. (denom > 0).
void LoadRoutesConstraint(const ConstraintProto &ct, Model *m)
void LoadAtMostOneConstraint(const ConstraintProto &ct, Model *m)
void AddFullEncodingFromSearchBranching(const CpModelProto &model_proto, Model *m)
std::vector< int > UsedVariables(const ConstraintProto &ct)
void LoadCircuitConstraint(const ConstraintProto &ct, Model *m)
void ExtractElementEncoding(const CpModelProto &model_proto, Model *m)
void LoadReservoirConstraint(const ConstraintProto &ct, Model *m)
void AddWeightedSumLowerOrEqual(absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const int64_t > coefficients, int64_t upper_bound, Model *model)
enforcement_literals => sum <= upper_bound
int ReindexArcs(IntContainer *tails, IntContainer *heads, absl::flat_hash_map< int, int > *mapping_output=nullptr)
Definition circuit.h:208
void LoadNoOverlapConstraint(const ConstraintProto &ct, Model *m)
void LoadAllDiffConstraint(const ConstraintProto &ct, Model *m)
void AddDisjunctive(const std::vector< IntervalVariable > &intervals, Model *model)
std::vector< Literal > Literals(absl::Span< const int > input)
Definition sat_base.h:146
void LoadNoOverlap2dConstraint(const ConstraintProto &ct, Model *m)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void LoadBoolAndConstraint(const ConstraintProto &ct, Model *m)
void AddNonOverlappingRectangles(const std::vector< IntervalVariable > &x, const std::vector< IntervalVariable > &y, Model *model)
Definition diffn.cc:150
void LoadExactlyOneConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ExactlyOneConstraint(absl::Span< const Literal > literals)
Definition sat_solver.h:917
bool LoadConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, absl::Span< const AffineExpression > demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition cumulative.cc:44
void PropagateEncodingFromEquivalenceRelations(const CpModelProto &model_proto, Model *m)
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< AffineExpression > deltas, std::vector< Literal > presences, int64_t min_level, int64_t max_level, Model *model)
Definition timetable.cc:32
std::function< void(Model *)> FixedModuloConstraint(AffineExpression a, IntegerValue b, AffineExpression c)
Adds the constraint: a % b = c where b is a constant.
const BooleanVariable kNoBooleanVariable(-1)
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
void AddWeightedSumGreaterOrEqual(absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const int64_t > coefficients, int64_t lower_bound, Model *model)
enforcement_literals => sum >= lower_bound
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< AffineExpression > &expressions)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
void LoadIntDivConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> WeightedSumLowerOrEqual(absl::Span< const IntegerVariable > vars, const VectorInt &coefficients, int64_t upper_bound)
Weighted sum <= constant.
In SWIG mode, we don't want anything besides these top-level includes.
int64_t Min() const
Returns the min of the domain.
Definition model.cc:340
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
var * coeff + constant >= bound.
IntegerLiteral LowerOrEqual(IntegerValue bound) const
var * coeff + constant <= bound.
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
#define SOLVER_LOG(logger,...)
Definition logging.h:109