22#include "absl/container/flat_hash_set.h"
23#include "absl/flags/flag.h"
24#include "absl/log/check.h"
25#include "absl/strings/string_view.h"
26#include "absl/types/span.h"
31 "Interpret floats as integers in all variables and constraints.");
36enum PresolveState { ALWAYS_FALSE, ALWAYS_TRUE, UNDECIDED };
40 for (
int i = 0;
i < values.size(); ++
i) {
41 if (values[i] != 0 && values[i] != 1) {
49bool AtMostOne0OrAtMostOne1(
const std::vector<T>& values) {
53 for (T val : values) {
67void AppendIfNotInSet(T*
value, absl::flat_hash_set<T*>* s,
68 std::vector<T*>* vec) {
69 if (s->insert(
value).second) {
70 vec->push_back(
value);
72 DCHECK_EQ(s->size(), vec->size());
97void Presolver::PresolveBool2Int(Constraint*
ct) {
98 DCHECK_EQ(
ct->type,
"bool2int");
99 if (
ct->arguments[0].HasOneValue() ||
ct->arguments[1].HasOneValue()) {
101 UpdateRuleStats(
"bool2int: rename to int_eq");
105 UpdateRuleStats(
"bool2int: merge boolean and integer variables.");
106 AddVariableSubstitution(
ct->arguments[1].Var(),
ct->arguments[0].Var());
107 ct->MarkAsInactive();
116void Presolver::PresolveStoreAffineMapping(Constraint*
ct) {
117 CHECK_EQ(2,
ct->arguments[1].variables.size());
118 Variable*
const var0 =
ct->arguments[1].variables[0];
119 Variable*
const var1 =
ct->arguments[1].variables[1];
120 const int64_t coeff0 =
ct->arguments[0].values[0];
121 const int64_t coeff1 =
ct->arguments[0].values[1];
122 const int64_t rhs =
ct->arguments[2].Value();
123 if (coeff0 == -1 && !affine_map_.contains(var0)) {
124 affine_map_[var0] = AffineMapping(var1, coeff0, -rhs,
ct);
125 UpdateRuleStats(
"int_lin_eq: store affine mapping");
126 }
else if (coeff1 == -1 && !affine_map_.contains(var1)) {
127 affine_map_[var1] = AffineMapping(var0, coeff0, -rhs,
ct);
128 UpdateRuleStats(
"int_lin_eq: store affine mapping");
132void Presolver::PresolveStoreFlatteningMapping(Constraint*
ct) {
133 CHECK_EQ(3,
ct->arguments[1].variables.size());
134 Variable*
const var0 =
ct->arguments[1].variables[0];
135 Variable*
const var1 =
ct->arguments[1].variables[1];
136 Variable*
const var2 =
ct->arguments[1].variables[2];
137 const int64_t coeff0 =
ct->arguments[0].values[0];
138 const int64_t coeff1 =
ct->arguments[0].values[1];
139 const int64_t coeff2 =
ct->arguments[0].values[2];
140 const int64_t rhs =
ct->arguments[2].Value();
141 if (coeff0 == -1 && coeff2 == 1 && !array2d_index_map_.contains(var0)) {
142 array2d_index_map_[var0] =
143 Array2DIndexMapping(var1, coeff1, var2, -rhs,
ct);
144 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
145 }
else if (coeff0 == -1 && coeff1 == 1 &&
146 !array2d_index_map_.contains(var0)) {
147 array2d_index_map_[var0] =
148 Array2DIndexMapping(var2, coeff2, var1, -rhs,
ct);
149 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
150 }
else if (coeff2 == -1 && coeff1 == 1 &&
151 !array2d_index_map_.contains(var2)) {
152 array2d_index_map_[var2] =
153 Array2DIndexMapping(var0, coeff0, var1, -rhs,
ct);
154 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
155 }
else if (coeff2 == -1 && coeff0 == 1 &&
156 !array2d_index_map_.contains(var2)) {
157 array2d_index_map_[var2] =
158 Array2DIndexMapping(var1, coeff1, var0, -rhs,
ct);
159 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
164bool IsIncreasingAndContiguous(absl::Span<const int64_t> values) {
165 for (
int i = 0;
i < values.size() - 1; ++
i) {
166 if (values[i + 1] != values[i] + 1) {
173bool AreOnesFollowedByMinusOne(
const std::vector<int64_t>& coeffs) {
174 CHECK(!coeffs.empty());
175 for (
int i = 0;
i < coeffs.size() - 1; ++
i) {
176 if (coeffs[i] != 1) {
180 return coeffs.back() == -1;
184bool IsStrictPrefix(
const std::vector<T>& v1,
const std::vector<T>& v2) {
185 if (v1.size() >= v2.size()) {
188 for (
int i = 0;
i < v1.size(); ++
i) {
189 if (v1[i] != v2[i]) {
215void Presolver::PresolveSimplifyElement(Constraint*
ct) {
216 if (
ct->arguments[0].variables.size() != 1)
return;
217 Variable*
const index_var =
ct->arguments[0].Var();
220 if (affine_map_.contains(index_var)) {
221 const AffineMapping& mapping = affine_map_[index_var];
222 const Domain& domain = mapping.variable->domain;
223 if (domain.is_interval && domain.values.empty()) {
227 if (domain.values[0] == 0 && mapping.coefficient == 1 &&
228 mapping.offset > 1 && index_var->domain.is_interval) {
230 const int offset = mapping.offset - 1;
231 const int size =
ct->arguments[1].values.size();
232 for (
int i = 0;
i < size - offset; ++
i) {
233 ct->arguments[1].values[
i] =
ct->arguments[1].values[
i + offset];
235 ct->arguments[1].values.resize(size - offset);
236 affine_map_[index_var].constraint->arguments[2].values[0] = -1;
237 affine_map_[index_var].offset = 1;
238 index_var->domain.values[0] -= offset;
239 index_var->domain.values[1] -= offset;
240 UpdateRuleStats(
"array_int_element: simplify using affine mapping.");
242 }
else if (mapping.offset + mapping.coefficient > 0 &&
243 domain.values[0] > 0) {
244 const std::vector<int64_t>& values =
ct->arguments[1].values;
245 std::vector<int64_t> new_values;
246 for (int64_t i = 1;
i <= domain.values.back(); ++
i) {
247 const int64_t
index =
i * mapping.coefficient + mapping.offset - 1;
251 if (
index > values.size()) {
254 new_values.push_back(values[
index]);
257 UpdateRuleStats(
"array_int_element: simplify using affine mapping.");
258 ct->arguments[0].variables[0] = mapping.variable;
259 ct->arguments[0].variables[0]->domain.IntersectWithInterval(
260 1, new_values.size());
262 ct->arguments[1].values.swap(new_values);
263 if (
ct->arguments[1].values.size() == 1) {
267 ct->presolve_propagation_done =
false;
269 mapping.constraint->MarkAsInactive();
270 index_var->active =
false;
276 if (array2d_index_map_.contains(index_var)) {
277 UpdateRuleStats(
"array_int_element: rewrite as a 2d element");
278 const Array2DIndexMapping& mapping = array2d_index_map_[index_var];
282 std::vector<int64_t> coefs;
283 coefs.push_back(mapping.coefficient);
287 index_var->active =
false;
288 mapping.constraint->MarkAsInactive();
293 if (index_var->domain.Max() <
ct->arguments[1].values.size()) {
295 ct->arguments[1].
values.resize(index_var->domain.Max());
296 ct->presolve_propagation_done =
false;
297 UpdateRuleStats(
"array_int_element: reduce array");
302 if (IsIncreasingAndContiguous(
ct->arguments[1].values) &&
304 const int64_t
start =
ct->arguments[1].values.front();
305 Variable*
const index =
ct->arguments[0].Var();
306 Variable*
const target =
ct->arguments[2].Var();
307 UpdateRuleStats(
"array_int_element: rewrite as a linear constraint");
314 ct->type =
"int_lin_eq";
326void Presolver::PresolveSimplifyExprElement(Constraint*
ct) {
327 if (
ct->arguments[0].variables.size() != 1)
return;
329 Variable*
const index_var =
ct->arguments[0].Var();
330 if (affine_map_.contains(index_var)) {
331 const AffineMapping& mapping = affine_map_[index_var];
332 const Domain& domain = mapping.variable->domain;
333 if ((domain.is_interval && domain.values.empty()) ||
334 domain.values[0] != 1 || mapping.offset + mapping.coefficient <= 0) {
338 const std::vector<Variable*>& vars =
ct->arguments[1].variables;
339 std::vector<Variable*> new_vars;
340 for (int64_t i = domain.values.front();
i <= domain.values.back(); ++
i) {
341 const int64_t
index =
i * mapping.coefficient + mapping.offset - 1;
345 if (
index >= vars.size()) {
348 new_vars.push_back(vars[
index]);
351 UpdateRuleStats(
"array_var_int_element: simplify using affine mapping.");
352 ct->arguments[0].variables[0] = mapping.variable;
354 ct->arguments[1].variables.swap(new_vars);
356 mapping.constraint->MarkAsInactive();
357 index_var->active =
false;
358 }
else if (index_var->domain.is_interval &&
359 index_var->domain.values.size() == 2 &&
360 index_var->domain.Max() <
ct->arguments[1].variables.size()) {
362 ct->arguments[1].variables.resize(index_var->domain.Max());
363 UpdateRuleStats(
"array_var_int_element: reduce array");
369 if (absl::GetFlag(FLAGS_fz_floats_are_ints)) {
372 const std::string&
id =
ct->type;
373 if (
id ==
"int2float") {
375 }
else if (
id ==
"float_lin_le") {
376 ct->type =
"int_lin_le";
377 }
else if (
id ==
"float_lin_eq") {
378 ct->type =
"int_lin_eq";
385 std::vector<Variable*> current_variables;
386 Variable* target_variable =
nullptr;
389 if (target_variable ==
nullptr) {
390 if (
ct->type ==
"int_lin_eq" &&
ct->arguments[0].values.size() == 3 &&
391 AreOnesFollowedByMinusOne(
ct->arguments[0].values) &&
392 ct->arguments[1].values.empty() &&
ct->arguments[2].Value() == 0) {
393 current_variables =
ct->arguments[1].variables;
394 target_variable = current_variables.back();
395 current_variables.pop_back();
396 first_constraint =
ct;
399 if (
ct->type ==
"int_lin_eq" &&
400 AreOnesFollowedByMinusOne(
ct->arguments[0].values) &&
401 ct->arguments[0].values.size() == current_variables.size() + 2 &&
402 IsStrictPrefix(current_variables,
ct->arguments[1].variables)) {
403 current_variables =
ct->arguments[1].variables;
405 ct->type =
"int_plus";
406 ct->arguments.clear();
408 ct->arguments.push_back(
411 target_variable = current_variables.back();
412 current_variables.pop_back();
415 if (first_constraint !=
nullptr) {
416 first_constraint =
nullptr;
419 current_variables.clear();
420 target_variable =
nullptr;
427 if (
ct->active &&
ct->type ==
"bool2int") {
428 PresolveBool2Int(
ct);
429 }
else if (
ct->active &&
ct->type ==
"int_lin_eq" &&
430 ct->arguments[1].variables.size() == 2 &&
431 ct->strong_propagation) {
432 PresolveStoreAffineMapping(
ct);
433 }
else if (
ct->active &&
ct->type ==
"int_lin_eq" &&
434 ct->arguments[1].variables.size() == 3 &&
435 ct->strong_propagation) {
436 PresolveStoreFlatteningMapping(
ct);
439 if (!var_representative_map_.empty()) {
441 SubstituteEverywhere(
model);
442 var_representative_map_.clear();
443 var_representative_vector_.clear();
448 if (
ct->type ==
"array_int_element" ||
ct->type ==
"array_bool_element") {
449 PresolveSimplifyElement(
ct);
451 if (
ct->type ==
"array_var_int_element" ||
452 ct->type ==
"array_var_bool_element") {
453 PresolveSimplifyExprElement(
ct);
458 if (!successful_rules_.empty()) {
459 for (
const auto& rule : successful_rules_) {
460 if (rule.second == 1) {
461 SOLVER_LOG(logger_,
" - rule '", rule.first,
"' was applied 1 time");
463 SOLVER_LOG(logger_,
" - rule '", rule.first,
"' was applied ",
464 rule.second,
" times");
473 CHECK(from !=
nullptr);
474 CHECK(
to !=
nullptr);
476 from = FindRepresentativeOfVar(from);
477 to = FindRepresentativeOfVar(
to);
487 var_representative_map_[from] =
to;
488 var_representative_vector_.push_back(from);
492Variable* Presolver::FindRepresentativeOfVar(Variable*
var) {
493 if (
var ==
nullptr)
return nullptr;
494 Variable* start_var =
var;
497 const auto& it = var_representative_map_.find(
var);
498 Variable* parent = it == var_representative_map_.end() ?
var : it->second;
499 if (parent ==
var)
break;
503 while (start_var !=
var) {
504 Variable*
const parent = var_representative_map_[start_var];
505 var_representative_map_[start_var] =
var;
508 const auto& iter = var_representative_map_.find(
var);
509 return iter == var_representative_map_.end() ?
var : iter->second;
512void Presolver::SubstituteEverywhere(Model*
model) {
514 for (Constraint*
const ct :
model->constraints()) {
515 if (
ct !=
nullptr &&
ct->active) {
516 for (
int i = 0;
i <
ct->arguments.size(); ++
i) {
517 Argument& argument =
ct->arguments[
i];
518 switch (argument.type) {
521 for (
int i = 0;
i < argument.variables.size(); ++
i) {
522 Variable*
const old_var = argument.variables[
i];
523 Variable*
const new_var = FindRepresentativeOfVar(old_var);
524 if (new_var != old_var) {
525 argument.variables[
i] = new_var;
537 for (Annotation*
const ann :
model->mutable_search_annotations()) {
538 SubstituteAnnotation(ann);
541 for (SolutionOutputSpecs*
const output :
model->mutable_output()) {
542 output->variable = FindRepresentativeOfVar(output->variable);
543 for (
int i = 0;
i < output->flat_variables.size(); ++
i) {
544 output->flat_variables[
i] =
545 FindRepresentativeOfVar(output->flat_variables[i]);
550 for (
const auto& iter : var_representative_map_) {
551 iter.second->domain.IntersectWithDomain(iter.first->domain);
555 Variable*
const current_objective =
model->objective();
556 if (current_objective ==
nullptr)
return;
557 Variable*
const new_objective = FindRepresentativeOfVar(current_objective);
558 if (new_objective != current_objective) {
559 model->SetObjective(new_objective);
563void Presolver::SubstituteAnnotation(Annotation* ann) {
568 for (
int i = 0;
i < ann->annotations.size(); ++
i) {
569 SubstituteAnnotation(&ann->annotations[i]);
575 for (
int i = 0;
i < ann->variables.size(); ++
i) {
576 ann->variables[
i] = FindRepresentativeOfVar(ann->variables[i]);
In SWIG mode, we don't want anything besides these top-level includes.
bool IsArrayBoolean(const std::vector< T > &values)
trees with all degrees equal to
ABSL_FLAG(bool, fz_floats_are_ints, false, "Interpret floats as integers in all variables and constraints.")
static Argument IntegerValue(int64_t value)
--— Argument --—
static Argument IntegerList(std::vector< int64_t > values)
static Argument VarRef(Variable *var)
static Argument VarRefArray(std::vector< Variable * > vars)
std::vector< int64_t > values
#define SOLVER_LOG(logger,...)