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"
40absl::flat_hash_map<IntegerValue, Literal> GetEncoding(IntegerVariable
var,
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;
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;
66 for (
int i = 0; i < values.size(); ++i) {
67 const IntegerValue v = values[i];
68 if (!encoding.contains(v)) {
71 pairs.emplace_back(v, line_literals[i]);
78 std::sort(pairs.begin(), pairs.end());
79 std::vector<Literal> clause = tuples_with_any;
80 for (
int i = 0; i < pairs.size();) {
82 clause.resize(tuples_with_any.size());
84 const IntegerValue
value = pairs[i].first;
85 for (; i < pairs.size() && pairs[i].first ==
value; ++i) {
86 clause.push_back(pairs[i].second);
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,
101 const int n = vars.size();
103 IntegerTrail*
const integer_trail =
model->GetOrCreate<IntegerTrail>();
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],
111 if (values_per_var.size() > 1) {
113 encodings[i] = GetEncoding(vars[i],
model);
118 if (values_per_var[0].size() == 1 || values_per_var[1].size() == 1)
return;
120 std::map<LiteralIndex, std::vector<Literal>> left_to_right;
121 std::map<LiteralIndex, std::vector<Literal>> right_to_left;
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)) {
133 left_to_right[left.Index()].push_back(right);
134 right_to_left[right.Index()].push_back(left);
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) {
150 clause.assign(supports.begin(), supports.end());
151 clause.push_back(Literal(lit).Negated());
154 if (supports.size() > max_support_size / 2) {
155 num_large_clause_added++;
160 for (
const auto& it : left_to_right) {
161 add_support_constraint(it.first, it.second, values_per_var[1].size());
163 for (
const auto& it : right_to_left) {
164 add_support_constraint(it.first, it.second, values_per_var[0].size());
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";
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) {
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());
199 if (max_num_prefix_tuples > 2 * tuples.size())
break;
201 absl::flat_hash_set<absl::Span<const int64>> prefixes;
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) {
212 const int num_prefix_tuples = prefixes.size();
214 std::vector<std::vector<int64>> negated_tuples;
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) {
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();
227 if (!prefixes.contains(tmp_tuple)) {
228 negated_tuples.push_back(tmp_tuple);
233 negated_tuples,
model);
234 VLOG(2) <<
" add negated tables with " << created
235 <<
" tuples on the range [" << start <<
"," << end <<
"]";
249 std::vector<std::vector<int64>> tuples,
Model*
model) {
250 const int n = vars.size();
252 const int num_original_tuples = tuples.size();
256 std::vector<absl::flat_hash_set<int64>> values_per_var(n);
258 for (
int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
260 for (
int i = 0; i < n; ++i) {
262 if (!values_per_var[i].contains(
value) &&
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]);
276 tuples.resize(
index);
277 const int num_valid_tuples = tuples.size();
279 if (tuples.empty()) {
285 AddSizeTwoTable(vars, tuples, values_per_var,
model);
291 int num_prefix_tuples = 0;
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));
297 num_prefix_tuples = prefixes.size();
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());
306 ExploreSubsetOfVariablesAndAddNegatedTables(tuples, var_domains, vars,
model);
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());
319 if (values_per_var.size() > 1) {
321 encodings[i] = GetEncoding(vars[i],
model);
327 std::vector<int64> domain_sizes;
328 for (
int i = 0; i < n; ++i) {
329 domain_sizes.push_back(values_per_var[i].size());
332 const int num_compressed_tuples = tuples.size();
335 const bool prefixes_are_all_different = num_prefix_tuples == num_valid_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());
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);
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);
354 absl::StrAppend(&
message,
", full prefix = true");
357 absl::StrAppend(&
message,
", num prefix tuples = ", num_prefix_tuples);
359 if (num_compressed_tuples != num_valid_tuples) {
361 ", compressed tuples = ", num_compressed_tuples);
366 if (tuples.size() == 1) {
382 std::vector<Literal> tuple_literals;
383 tuple_literals.reserve(tuples.size());
384 if (tuples.size() == 2) {
386 tuple_literals.emplace_back(tuple_literals[0].Negated());
387 }
else if (tuples.size() > 2) {
388 for (
int i = 0; i < tuples.size(); ++i) {
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;
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];
406 if (v == any_value) {
407 any_tuple_literals.push_back(tuple_literals[j]);
409 active_tuple_literals.push_back(tuple_literals[j]);
410 active_values.push_back(IntegerValue(v));
414 if (!active_tuple_literals.empty()) {
415 ProcessOneColumn(active_tuple_literals, active_values, encodings[i],
416 any_tuple_literals,
model);
420 if (prefixes_are_all_different) {
425 std::vector<Literal> clause;
426 for (
int j = 0; j < tuples.size(); ++j) {
428 bool tuple_is_valid =
true;
429 for (
int i = 0; i + 1 < n; ++i) {
431 if (values_per_var[i].size() == 1)
continue;
433 const int64 v = tuples[j][i];
435 if (v == any_value)
continue;
437 const IntegerValue
value(v);
438 if (!encodings[i].contains(
value)) {
439 tuple_is_valid =
false;
444 if (!tuple_is_valid)
continue;
447 const IntegerValue target_value = IntegerValue(tuples[j][n - 1]);
448 if (!encodings[n - 1].contains(target_value))
continue;
451 clause.push_back(target_literal);
458 std::vector<std::vector<int64>> tuples,
460 const int n = vars.size();
466 while (
index < tuples.size()) {
468 for (
int i = 0; i < n; ++i) {
469 if (!integer_trail->InitialVariableDomain(vars[i]).Contains(
476 tuples[
index] = tuples.back();
483 if (tuples.empty()) {
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());
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;
505 std::vector<Literal> clause;
506 for (
const std::vector<int64>& tuple : tuples) {
507 bool add_tuple =
true;
509 for (
int i = 0; i < n; ++i) {
511 if (
value == any_value)
continue;
516 if (mapping[i].contains(
value)) {
525 if (value < lb || value > ub) {
530 clause.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
534 clause.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
536 IntegerValue(
value + 1))));
545 const std::vector<std::vector<Literal>>& literal_tuples,
546 const std::vector<Literal>& line_literals) {
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());
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);
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]) {
580 for (
const auto& p : line_literals_per_literal) {
581 std::vector<Literal> clause;
582 for (
const auto&
index : p.second) {
592 const std::vector<IntegerVariable>& vars,
593 const std::vector<std::vector<int64>>& automaton,
int64 initial_state,
594 const std::vector<int64>& final_states) {
597 const int n = vars.size();
598 CHECK_GT(n, 0) <<
"No variables in TransitionConstraint().";
602 std::set<std::pair<int64, int64>> unique_transition_checker;
603 for (
const std::vector<int64>& transition : automaton) {
605 const std::pair<int64, int64> p{transition[0], transition[1]};
607 <<
"Duplicate outgoing transitions with value " << transition[1]
608 <<
" from state " << transition[0] <<
".";
609 unique_transition_checker.insert(p);
614 std::vector<absl::flat_hash_set<int64>> possible_values(n);
617 for (
const std::vector<int64>& transition : automaton) {
619 if (domain.Contains(transition[1])) {
620 possible_values[
time].insert(transition[1]);
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()};
635 for (
const std::vector<int64>& transition : automaton) {
638 reachable_states[
time + 1].insert(transition[2]);
644 std::set<int64> new_set;
645 for (
const std::vector<int64>& transition : automaton) {
650 new_set.insert(transition[0]);
652 reachable_states[
time].swap(new_set);
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;
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) {
680 tuple_literals.push_back(
682 in_states.push_back(IntegerValue(transition[0]));
684 transition_values.push_back(IntegerValue(transition[1]));
688 out_states.push_back(
time + 1 == n ? IntegerValue(0)
689 : IntegerValue(transition[2]));
697 std::vector<IntegerValue> s = transition_values;
702 std::vector<int64> values;
703 values.reserve(s.size());
704 for (IntegerValue v : s) values.push_back(v.value());
708 encoding = GetEncoding(vars[
time],
model);
712 const int64 unique_value = s.begin()->value();
720 std::vector<IntegerValue> s = out_states;
723 out_encoding.clear();
728 }
else if (s.size() > 1) {
729 for (
const IntegerValue state : s) {
731 out_encoding[state] = l;
741 if (!in_encoding.empty()) {
742 ProcessOneColumn(tuple_literals, in_states, in_encoding, {},
model);
744 if (!encoding.empty()) {
745 ProcessOneColumn(tuple_literals, transition_values, encoding, {},
748 if (!out_encoding.empty()) {
749 ProcessOneColumn(tuple_literals, out_states, out_encoding, {},
model);
751 in_encoding = out_encoding;
#define CHECK_EQ(val1, val2)
#define CHECK_GT(val1, val2)
#define VLOG(verboselevel)
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
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Class that owns everything related to a particular optimization model.
static const int64 kint64min
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
bool ContainsKey(const Collection &collection, const Key &key)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
void AddNegatedTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 > > tuples, Model *model)
std::function< void(Model *)> LiteralTableConstraint(const std::vector< std::vector< Literal > > &literal_tuples, const std::vector< Literal > &line_literals)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
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)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
void AddTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 > > tuples, Model *model)
void CompressTuples(absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 > > *tuples)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapProd(int64 x, int64 y)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
#define VLOG_IS_ON(verboselevel)