OR-Tools  8.2
sat/table.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
14#include "ortools/sat/table.h"
15
16#include <algorithm>
17#include <memory>
18#include <set>
19#include <utility>
20
21#include "absl/container/flat_hash_map.h"
22#include "absl/container/flat_hash_set.h"
23#include "absl/strings/str_cat.h"
24#include "absl/strings/str_join.h"
31#include "ortools/sat/util.h"
33
34namespace operations_research {
35namespace sat {
36
37namespace {
38
39// Converts the vector representation returned by FullDomainEncoding() to a map.
40absl::flat_hash_map<IntegerValue, Literal> GetEncoding(IntegerVariable var,
41 Model* model) {
42 absl::flat_hash_map<IntegerValue, Literal> encoding;
43 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
44 for (const auto& entry : encoder->FullDomainEncoding(var)) {
45 encoding[entry.value] = entry.literal;
46 }
47 return encoding;
48}
49
50// Add the implications and clauses to link one column of a table to the Literal
51// controling if the lines are possible or not. The column has the given values,
52// and the Literal of the column variable can be retrieved using the encoding
53// map. Thew tuples_with_any vector provides a list of line_literals that will
54// support any value.
55void ProcessOneColumn(
56 const std::vector<Literal>& line_literals,
57 const std::vector<IntegerValue>& values,
58 const absl::flat_hash_map<IntegerValue, Literal>& encoding,
59 const std::vector<Literal>& tuples_with_any, Model* model) {
60 CHECK_EQ(line_literals.size(), values.size());
61 std::vector<std::pair<IntegerValue, Literal>> pairs;
62
63 // If a value is false (i.e not possible), then the tuple with this value
64 // is false too (i.e not possible). Conversely, if the tuple is selected,
65 // the value must be selected.
66 for (int i = 0; i < values.size(); ++i) {
67 const IntegerValue v = values[i];
68 if (!encoding.contains(v)) {
69 model->Add(ClauseConstraint({line_literals[i].Negated()}));
70 } else {
71 pairs.emplace_back(v, line_literals[i]);
72 model->Add(Implication(line_literals[i], gtl::FindOrDie(encoding, v)));
73 }
74 }
75
76 // Regroup literal with the same value and add for each the clause: If all the
77 // tuples containing a value are false, then this value must be false too.
78 std::sort(pairs.begin(), pairs.end());
79 std::vector<Literal> clause = tuples_with_any;
80 for (int i = 0; i < pairs.size();) {
81 // We always keep the tuples_with_any at the beginning of the clause.
82 clause.resize(tuples_with_any.size());
83
84 const IntegerValue value = pairs[i].first;
85 for (; i < pairs.size() && pairs[i].first == value; ++i) {
86 clause.push_back(pairs[i].second);
87 }
88
89 // And the "value" literal and load the clause.
90 clause.push_back(gtl::FindOrDie(encoding, value).Negated());
91 model->Add(ClauseConstraint(clause));
92 }
93}
94
95// Simpler encoding for table constraints with 2 variables.
96void AddSizeTwoTable(
97 absl::Span<const IntegerVariable> vars,
98 const std::vector<std::vector<int64>>& tuples,
99 const std::vector<absl::flat_hash_set<int64>>& values_per_var,
100 Model* model) {
101 const int n = vars.size();
102 CHECK_EQ(n, 2);
103 IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();
104
105 std::vector<absl::flat_hash_map<IntegerValue, Literal>> encodings(n);
106 for (int i = 0; i < n; ++i) {
107 const std::vector<int64> reached_values(values_per_var[i].begin(),
108 values_per_var[i].end());
109 integer_trail->UpdateInitialDomain(vars[i],
110 Domain::FromValues(reached_values));
111 if (values_per_var.size() > 1) {
112 model->Add(FullyEncodeVariable(vars[i]));
113 encodings[i] = GetEncoding(vars[i], model);
114 }
115 }
116
117 // One variable is fixed. Propagation is complete.
118 if (values_per_var[0].size() == 1 || values_per_var[1].size() == 1) return;
119
120 std::map<LiteralIndex, std::vector<Literal>> left_to_right;
121 std::map<LiteralIndex, std::vector<Literal>> right_to_left;
122
123 for (const auto& tuple : tuples) {
124 const IntegerValue left_value(tuple[0]);
125 const IntegerValue right_value(tuple[1]);
126 if (!encodings[0].contains(left_value) ||
127 !encodings[1].contains(right_value)) {
128 continue;
129 }
130
131 const Literal left = gtl::FindOrDie(encodings[0], left_value);
132 const Literal right = gtl::FindOrDie(encodings[1], right_value);
133 left_to_right[left.Index()].push_back(right);
134 right_to_left[right.Index()].push_back(left);
135 }
136
137 int num_implications = 0;
138 int num_clause_added = 0;
139 int num_large_clause_added = 0;
140 std::vector<Literal> clause;
141 auto add_support_constraint =
142 [model, &num_clause_added, &num_large_clause_added, &num_implications,
143 &clause](LiteralIndex lit, const std::vector<Literal>& supports,
144 int max_support_size) {
145 if (supports.size() == max_support_size) return;
146 if (supports.size() == 1) {
147 model->Add(Implication(Literal(lit), supports.front()));
148 num_implications++;
149 } else {
150 clause.assign(supports.begin(), supports.end());
151 clause.push_back(Literal(lit).Negated());
152 model->Add(ClauseConstraint(clause));
153 num_clause_added++;
154 if (supports.size() > max_support_size / 2) {
155 num_large_clause_added++;
156 }
157 }
158 };
159
160 for (const auto& it : left_to_right) {
161 add_support_constraint(it.first, it.second, values_per_var[1].size());
162 }
163 for (const auto& it : right_to_left) {
164 add_support_constraint(it.first, it.second, values_per_var[0].size());
165 }
166 VLOG(2) << "Table: 2 variables, " << tuples.size() << " tuples encoded using "
167 << num_clause_added << " clauses, " << num_large_clause_added
168 << " large clauses, " << num_implications << " implications";
169}
170
171// This method heuristically explores subsets of variables and decide if the
172// projection of all tuples nearly fills all the possible combination of
173// projected variables domains.
174//
175// In that case, it creates the complement of the projected tuples and add that
176// as a forbidden assignment constraint.
177void ExploreSubsetOfVariablesAndAddNegatedTables(
178 const std::vector<std::vector<int64>>& tuples,
179 const std::vector<std::vector<int64>>& var_domains,
180 absl::Span<const IntegerVariable> vars, Model* model) {
181 const int num_vars = var_domains.size();
182 for (int start = 0; start < num_vars; ++start) {
183 const int limit = start == 0 ? num_vars : std::min(num_vars, start + 3);
184 for (int end = start + 1; end < limit; ++end) {
185 // TODO(user,user): If we add negated table for more than one value of
186 // end, because the set of variables will be included in each other, we
187 // could reduce the number of clauses added. I.e if we excluded
188 // (x=2, y=3) there is no need to exclude any of the tuples
189 // (x=2, y=3, z=*).
190
191 // Compute the maximum number of such prefix tuples.
192 int64 max_num_prefix_tuples = 1;
193 for (int i = start; i <= end; ++i) {
194 max_num_prefix_tuples =
195 CapProd(max_num_prefix_tuples, var_domains[i].size());
196 }
197
198 // Abort early.
199 if (max_num_prefix_tuples > 2 * tuples.size()) break;
200
201 absl::flat_hash_set<absl::Span<const int64>> prefixes;
202 bool skip = false;
203 for (const std::vector<int64>& tuple : tuples) {
204 prefixes.insert(absl::MakeSpan(&tuple[start], end - start + 1));
205 if (prefixes.size() == max_num_prefix_tuples) {
206 // Nothing to add with this range [start..end].
207 skip = true;
208 break;
209 }
210 }
211 if (skip) continue;
212 const int num_prefix_tuples = prefixes.size();
213
214 std::vector<std::vector<int64>> negated_tuples;
215
216 int created = 0;
217 if (num_prefix_tuples < max_num_prefix_tuples &&
218 max_num_prefix_tuples < num_prefix_tuples * 2) {
219 std::vector<int64> tmp_tuple;
220 for (int i = 0; i < max_num_prefix_tuples; ++i) {
221 tmp_tuple.clear();
222 int index = i;
223 for (int j = start; j <= end; ++j) {
224 tmp_tuple.push_back(var_domains[j][index % var_domains[j].size()]);
225 index /= var_domains[j].size();
226 }
227 if (!prefixes.contains(tmp_tuple)) {
228 negated_tuples.push_back(tmp_tuple);
229 created++;
230 }
231 }
232 AddNegatedTableConstraint(vars.subspan(start, end - start + 1),
233 negated_tuples, model);
234 VLOG(2) << " add negated tables with " << created
235 << " tuples on the range [" << start << "," << end << "]";
236 }
237 }
238 }
239}
240
241} // namespace
242
243// Makes a static decomposition of a table constraint into clauses.
244// This uses an auxiliary vector of Literals tuple_literals.
245// For every column col, and every value val of that column,
246// the decomposition uses clauses corresponding to the equivalence:
247// (\/_{row | tuples[row][col] = val} tuple_literals[row]) <=> (vars[col] = val)
248void AddTableConstraint(absl::Span<const IntegerVariable> vars,
249 std::vector<std::vector<int64>> tuples, Model* model) {
250 const int n = vars.size();
251 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
252 const int num_original_tuples = tuples.size();
253
254 // Compute the set of possible values for each variable (from the table).
255 // Remove invalid tuples along the way.
256 std::vector<absl::flat_hash_set<int64>> values_per_var(n);
257 int index = 0;
258 for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
259 bool keep = true;
260 for (int i = 0; i < n; ++i) {
261 const int64 value = tuples[tuple_index][i];
262 if (!values_per_var[i].contains(value) /* cached */ &&
263 !integer_trail->InitialVariableDomain(vars[i]).Contains(value)) {
264 keep = false;
265 break;
266 }
267 }
268 if (keep) {
269 std::swap(tuples[tuple_index], tuples[index]);
270 for (int i = 0; i < n; ++i) {
271 values_per_var[i].insert(tuples[index][i]);
272 }
273 index++;
274 }
275 }
276 tuples.resize(index);
277 const int num_valid_tuples = tuples.size();
278
279 if (tuples.empty()) {
280 model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
281 return;
282 }
283
284 if (n == 2) {
285 AddSizeTwoTable(vars, tuples, values_per_var, model);
286 return;
287 }
288
289 // It is easier to compute this before compression, as compression will merge
290 // tuples.
291 int num_prefix_tuples = 0;
292 {
293 absl::flat_hash_set<absl::Span<const int64>> prefixes;
294 for (const std::vector<int64>& tuple : tuples) {
295 prefixes.insert(absl::MakeSpan(tuple.data(), n - 1));
296 }
297 num_prefix_tuples = prefixes.size();
298 }
299
300 std::vector<std::vector<int64>> var_domains(n);
301 for (int j = 0; j < n; ++j) {
302 var_domains[j].assign(values_per_var[j].begin(), values_per_var[j].end());
303 std::sort(var_domains[j].begin(), var_domains[j].end());
304 }
305 CHECK_GT(vars.size(), 2);
306 ExploreSubsetOfVariablesAndAddNegatedTables(tuples, var_domains, vars, model);
307
308 // The variable domains have been computed. Fully encode variables.
309 // Note that in some corner cases (like duplicate vars), as we call
310 // UpdateInitialDomain(), the domain of other variable could become more
311 // restricted that values_per_var. For now, we do not try to reach a fixed
312 // point here.
313 std::vector<absl::flat_hash_map<IntegerValue, Literal>> encodings(n);
314 for (int i = 0; i < n; ++i) {
315 const std::vector<int64> reached_values(values_per_var[i].begin(),
316 values_per_var[i].end());
317 integer_trail->UpdateInitialDomain(vars[i],
318 Domain::FromValues(reached_values));
319 if (values_per_var.size() > 1) {
320 model->Add(FullyEncodeVariable(vars[i]));
321 encodings[i] = GetEncoding(vars[i], model);
322 }
323 }
324
325 // Compress tuples.
326 const int64 any_value = kint64min;
327 std::vector<int64> domain_sizes;
328 for (int i = 0; i < n; ++i) {
329 domain_sizes.push_back(values_per_var[i].size());
330 }
331 CompressTuples(domain_sizes, any_value, &tuples);
332 const int num_compressed_tuples = tuples.size();
333
334 // Detect if prefix tuples are all different.
335 const bool prefixes_are_all_different = num_prefix_tuples == num_valid_tuples;
336 if (VLOG_IS_ON(2)) {
337 // Compute the maximum number of prefix tuples.
338 int64 max_num_prefix_tuples = 1;
339 for (int i = 0; i + 1 < n; ++i) {
340 max_num_prefix_tuples =
341 CapProd(max_num_prefix_tuples, values_per_var[i].size());
342 }
343
344 std::string message = absl::StrCat(
345 "Table: ", n, " variables, original tuples = ", num_original_tuples);
346 if (num_valid_tuples != num_original_tuples) {
347 absl::StrAppend(&message, ", valid tuples = ", num_valid_tuples);
348 }
349 if (prefixes_are_all_different) {
350 if (num_prefix_tuples < max_num_prefix_tuples) {
351 absl::StrAppend(&message, ", partial prefix = ", num_prefix_tuples, "/",
352 max_num_prefix_tuples);
353 } else {
354 absl::StrAppend(&message, ", full prefix = true");
355 }
356 } else {
357 absl::StrAppend(&message, ", num prefix tuples = ", num_prefix_tuples);
358 }
359 if (num_compressed_tuples != num_valid_tuples) {
360 absl::StrAppend(&message,
361 ", compressed tuples = ", num_compressed_tuples);
362 }
363 VLOG(2) << message;
364 }
365
366 if (tuples.size() == 1) {
367 // Nothing more to do.
368 return;
369 }
370
371 // Create one Boolean variable per tuple to indicate if it can still be
372 // selected or not. Note that we don't enforce exactly one tuple to be
373 // selected because these variables are just used by this constraint, so
374 // only the information "can't be selected" is important.
375 //
376 // TODO(user): If a value in one column is unique, we don't need to
377 // create a new BooleanVariable corresponding to this line since we can use
378 // the one corresponding to this value in that column.
379 //
380 // Note that if there is just one tuple, there is no need to create such
381 // variables since they are not used.
382 std::vector<Literal> tuple_literals;
383 tuple_literals.reserve(tuples.size());
384 if (tuples.size() == 2) {
385 tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true);
386 tuple_literals.emplace_back(tuple_literals[0].Negated());
387 } else if (tuples.size() > 2) {
388 for (int i = 0; i < tuples.size(); ++i) {
389 tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true);
390 }
391 model->Add(ClauseConstraint(tuple_literals));
392 }
393
394 std::vector<Literal> active_tuple_literals;
395 std::vector<IntegerValue> active_values;
396 std::vector<Literal> any_tuple_literals;
397 for (int i = 0; i < n; ++i) {
398 if (values_per_var[i].size() == 1) continue;
399
400 active_tuple_literals.clear();
401 active_values.clear();
402 any_tuple_literals.clear();
403 for (int j = 0; j < tuple_literals.size(); ++j) {
404 const int64 v = tuples[j][i];
405
406 if (v == any_value) {
407 any_tuple_literals.push_back(tuple_literals[j]);
408 } else {
409 active_tuple_literals.push_back(tuple_literals[j]);
410 active_values.push_back(IntegerValue(v));
411 }
412 }
413
414 if (!active_tuple_literals.empty()) {
415 ProcessOneColumn(active_tuple_literals, active_values, encodings[i],
416 any_tuple_literals, model);
417 }
418 }
419
420 if (prefixes_are_all_different) {
421 // The first n-1 columns are all different, this encodes the implication
422 // table (tuple of size n - 1) implies value. We can add an optional
423 // propagation that should lead to better explanation.
424 // For each tuple, we add a clause prefix => last value.
425 std::vector<Literal> clause;
426 for (int j = 0; j < tuples.size(); ++j) {
427 clause.clear();
428 bool tuple_is_valid = true;
429 for (int i = 0; i + 1 < n; ++i) {
430 // Ignore fixed variables.
431 if (values_per_var[i].size() == 1) continue;
432
433 const int64 v = tuples[j][i];
434 // Ignored 'any' created during compression.
435 if (v == any_value) continue;
436
437 const IntegerValue value(v);
438 if (!encodings[i].contains(value)) {
439 tuple_is_valid = false;
440 break;
441 }
442 clause.push_back(gtl::FindOrDie(encodings[i], value).Negated());
443 }
444 if (!tuple_is_valid) continue;
445
446 // Add the target of the implication.
447 const IntegerValue target_value = IntegerValue(tuples[j][n - 1]);
448 if (!encodings[n - 1].contains(target_value)) continue;
449 const Literal target_literal =
450 gtl::FindOrDie(encodings[n - 1], target_value);
451 clause.push_back(target_literal);
452 model->Add(ClauseConstraint(clause));
453 }
454 }
455}
456
457void AddNegatedTableConstraint(absl::Span<const IntegerVariable> vars,
458 std::vector<std::vector<int64>> tuples,
459 Model* model) {
460 const int n = vars.size();
461 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
462 auto* integer_encoder = model->GetOrCreate<IntegerEncoder>();
463
464 // Remove unreachable tuples.
465 int index = 0;
466 while (index < tuples.size()) {
467 bool remove = false;
468 for (int i = 0; i < n; ++i) {
469 if (!integer_trail->InitialVariableDomain(vars[i]).Contains(
470 tuples[index][i])) {
471 remove = true;
472 break;
473 }
474 }
475 if (remove) {
476 tuples[index] = tuples.back();
477 tuples.pop_back();
478 } else {
479 index++;
480 }
481 }
482
483 if (tuples.empty()) {
484 return;
485 }
486
487 // Compress tuples.
488 const int64 any_value = kint64min;
489 std::vector<int64> domain_sizes;
490 for (int i = 0; i < n; ++i) {
491 domain_sizes.push_back(
492 integer_trail->InitialVariableDomain(vars[i]).Size());
493 }
494 CompressTuples(domain_sizes, any_value, &tuples);
495
496 // Collect all relevant var == value literal.
497 std::vector<absl::flat_hash_map<int64, Literal>> mapping(n);
498 for (int i = 0; i < n; ++i) {
499 for (const auto pair : integer_encoder->PartialDomainEncoding(vars[i])) {
500 mapping[i][pair.value.value()] = pair.literal;
501 }
502 }
503
504 // For each tuple, forbid the variables values to be this tuple.
505 std::vector<Literal> clause;
506 for (const std::vector<int64>& tuple : tuples) {
507 bool add_tuple = true;
508 clause.clear();
509 for (int i = 0; i < n; ++i) {
510 const int64 value = tuple[i];
511 if (value == any_value) continue;
512
513 // If a literal associated to var == value exist, use it, otherwise
514 // just use (and eventually create) the two literals var >= value + 1
515 // and var <= value - 1.
516 if (mapping[i].contains(value)) {
517 clause.push_back(gtl::FindOrDie(mapping[i], value).Negated());
518 } else {
519 const int64 lb = model->Get(LowerBound(vars[i]));
520 const int64 ub = model->Get(UpperBound(vars[i]));
521
522 // TODO(user): test the full initial domain instead of just checking
523 // the bounds. That shouldn't change too much since the literals added
524 // below will be trivially true or false though.
525 if (value < lb || value > ub) {
526 add_tuple = false;
527 break;
528 }
529 if (value > lb) {
530 clause.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
531 IntegerLiteral::LowerOrEqual(vars[i], IntegerValue(value - 1))));
532 }
533 if (value < ub) {
534 clause.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
536 IntegerValue(value + 1))));
537 }
538 }
539 }
540 if (add_tuple) model->Add(ClauseConstraint(clause));
541 }
542}
543
544std::function<void(Model*)> LiteralTableConstraint(
545 const std::vector<std::vector<Literal>>& literal_tuples,
546 const std::vector<Literal>& line_literals) {
547 return [=](Model* model) {
548 CHECK_EQ(literal_tuples.size(), line_literals.size());
549 const int num_tuples = line_literals.size();
550 if (num_tuples == 0) return;
551 const int tuple_size = literal_tuples[0].size();
552 if (tuple_size == 0) return;
553 for (int i = 1; i < num_tuples; ++i) {
554 CHECK_EQ(tuple_size, literal_tuples[i].size());
555 }
556
557 absl::flat_hash_map<LiteralIndex, std::vector<LiteralIndex>>
558 line_literals_per_literal;
559 for (int i = 0; i < num_tuples; ++i) {
560 const LiteralIndex selected_index = line_literals[i].Index();
561 for (const Literal l : literal_tuples[i]) {
562 line_literals_per_literal[l.Index()].push_back(selected_index);
563 }
564 }
565
566 // line_literals[i] == true => literal_tuples[i][j] == true.
567 // literal_tuples[i][j] == false => line_literals[i] == false.
568 for (int i = 0; i < num_tuples; ++i) {
569 const Literal line_is_selected = line_literals[i];
570 for (const Literal lit : literal_tuples[i]) {
571 model->Add(Implication(line_is_selected, lit));
572 }
573 }
574
575 // Exactly one selected literal is true.
576 model->Add(ExactlyOneConstraint(line_literals));
577
578 // If all selected literals of the lines containing a literal are false,
579 // then the literal is false.
580 for (const auto& p : line_literals_per_literal) {
581 std::vector<Literal> clause;
582 for (const auto& index : p.second) {
583 clause.push_back(Literal(index));
584 }
585 clause.push_back(Literal(p.first).Negated());
586 model->Add(ClauseConstraint(clause));
587 }
588 };
589}
590
591std::function<void(Model*)> TransitionConstraint(
592 const std::vector<IntegerVariable>& vars,
593 const std::vector<std::vector<int64>>& automaton, int64 initial_state,
594 const std::vector<int64>& final_states) {
595 return [=](Model* model) {
596 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
597 const int n = vars.size();
598 CHECK_GT(n, 0) << "No variables in TransitionConstraint().";
599
600 // Test precondition.
601 {
602 std::set<std::pair<int64, int64>> unique_transition_checker;
603 for (const std::vector<int64>& transition : automaton) {
604 CHECK_EQ(transition.size(), 3);
605 const std::pair<int64, int64> p{transition[0], transition[1]};
606 CHECK(!gtl::ContainsKey(unique_transition_checker, p))
607 << "Duplicate outgoing transitions with value " << transition[1]
608 << " from state " << transition[0] << ".";
609 unique_transition_checker.insert(p);
610 }
611 }
612
613 // Construct a table with the possible values of each vars.
614 std::vector<absl::flat_hash_set<int64>> possible_values(n);
615 for (int time = 0; time < n; ++time) {
616 const auto domain = integer_trail->InitialVariableDomain(vars[time]);
617 for (const std::vector<int64>& transition : automaton) {
618 // TODO(user): quadratic algo, improve!
619 if (domain.Contains(transition[1])) {
620 possible_values[time].insert(transition[1]);
621 }
622 }
623 }
624
625 // Compute the set of reachable state at each time point.
626 std::vector<std::set<int64>> reachable_states(n + 1);
627 reachable_states[0].insert(initial_state);
628 reachable_states[n] = {final_states.begin(), final_states.end()};
629
630 // Forward.
631 //
632 // TODO(user): filter using the domain of vars[time] that may not contain
633 // all the possible transitions.
634 for (int time = 0; time + 1 < n; ++time) {
635 for (const std::vector<int64>& transition : automaton) {
636 if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
637 if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
638 reachable_states[time + 1].insert(transition[2]);
639 }
640 }
641
642 // Backward.
643 for (int time = n - 1; time > 0; --time) {
644 std::set<int64> new_set;
645 for (const std::vector<int64>& transition : automaton) {
646 if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
647 if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
648 if (!gtl::ContainsKey(reachable_states[time + 1], transition[2]))
649 continue;
650 new_set.insert(transition[0]);
651 }
652 reachable_states[time].swap(new_set);
653 }
654
655 // We will model at each time step the current automaton state using Boolean
656 // variables. We will have n+1 time step. At time zero, we start in the
657 // initial state, and at time n we should be in one of the final states. We
658 // don't need to create Booleans at at time when there is just one possible
659 // state (like at time zero).
660 absl::flat_hash_map<IntegerValue, Literal> encoding;
661 absl::flat_hash_map<IntegerValue, Literal> in_encoding;
662 absl::flat_hash_map<IntegerValue, Literal> out_encoding;
663 for (int time = 0; time < n; ++time) {
664 // All these vector have the same size. We will use them to enforce a
665 // local table constraint representing one step of the automaton at the
666 // given time.
667 std::vector<Literal> tuple_literals;
668 std::vector<IntegerValue> in_states;
669 std::vector<IntegerValue> transition_values;
670 std::vector<IntegerValue> out_states;
671 for (const std::vector<int64>& transition : automaton) {
672 if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
673 if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
674 if (!gtl::ContainsKey(reachable_states[time + 1], transition[2]))
675 continue;
676
677 // TODO(user): if this transition correspond to just one in-state or
678 // one-out state or one variable value, we could reuse the corresponding
679 // Boolean variable instead of creating a new one!
680 tuple_literals.push_back(
681 Literal(model->Add(NewBooleanVariable()), true));
682 in_states.push_back(IntegerValue(transition[0]));
683
684 transition_values.push_back(IntegerValue(transition[1]));
685
686 // On the last step we don't need to distinguish the output states, so
687 // we use zero.
688 out_states.push_back(time + 1 == n ? IntegerValue(0)
689 : IntegerValue(transition[2]));
690 }
691
692 // Fully instantiate vars[time].
693 // Tricky: because we started adding constraints that can propagate, the
694 // possible values returned by encoding might not contains all the value
695 // computed in transition_values.
696 {
697 std::vector<IntegerValue> s = transition_values;
699
700 encoding.clear();
701 if (s.size() > 1) {
702 std::vector<int64> values;
703 values.reserve(s.size());
704 for (IntegerValue v : s) values.push_back(v.value());
705 integer_trail->UpdateInitialDomain(vars[time],
706 Domain::FromValues(values));
707 model->Add(FullyEncodeVariable(vars[time]));
708 encoding = GetEncoding(vars[time], model);
709 } else {
710 // Fix vars[time] to its unique possible value.
711 CHECK_EQ(s.size(), 1);
712 const int64 unique_value = s.begin()->value();
713 model->Add(LowerOrEqual(vars[time], unique_value));
714 model->Add(GreaterOrEqual(vars[time], unique_value));
715 }
716 }
717
718 // For each possible out states, create one Boolean variable.
719 {
720 std::vector<IntegerValue> s = out_states;
722
723 out_encoding.clear();
724 if (s.size() == 2) {
725 const BooleanVariable var = model->Add(NewBooleanVariable());
726 out_encoding[s.front()] = Literal(var, true);
727 out_encoding[s.back()] = Literal(var, false);
728 } else if (s.size() > 1) {
729 for (const IntegerValue state : s) {
730 const Literal l = Literal(model->Add(NewBooleanVariable()), true);
731 out_encoding[state] = l;
732 }
733 }
734 }
735
736 // Now we link everything together.
737 //
738 // Note that we do not need the ExactlyOneConstraint(tuple_literals)
739 // because it is already implicitely encoded since we have exactly one
740 // transition value.
741 if (!in_encoding.empty()) {
742 ProcessOneColumn(tuple_literals, in_states, in_encoding, {}, model);
743 }
744 if (!encoding.empty()) {
745 ProcessOneColumn(tuple_literals, transition_values, encoding, {},
746 model);
747 }
748 if (!out_encoding.empty()) {
749 ProcessOneColumn(tuple_literals, out_states, out_encoding, {}, model);
750 }
751 in_encoding = out_encoding;
752 }
753 };
754}
755
756} // namespace sat
757} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define VLOG(verboselevel)
Definition: base/logging.h:978
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
bool Contains(int64 value) const
Returns true iff value is in Domain.
const Domain & InitialVariableDomain(IntegerVariable var) const
Definition: integer.cc:644
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
static const int64 kint64min
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
void AddNegatedTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 > > tuples, Model *model)
Definition: sat/table.cc:457
std::function< void(Model *)> LiteralTableConstraint(const std::vector< std::vector< Literal > > &literal_tuples, const std::vector< Literal > &line_literals)
Definition: sat/table.cc:544
std::function< std::vector< IntegerEncoder::ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
Definition: integer.h:1587
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1467
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
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< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
Definition: integer.h:1495
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1509
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:876
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
Definition: integer.h:1537
void AddTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 > > tuples, Model *model)
Definition: sat/table.cc:248
void CompressTuples(absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 > > *tuples)
Definition: sat/util.cc:112
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapProd(int64 x, int64 y)
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
std::string message
Definition: trace.cc:395
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41