OR-Tools  8.2
linear_constraint.cc
Go to the documentation of this file.
1 // Copyright 2010-2018 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
15 
16 #include "ortools/base/mathutil.h"
18 #include "ortools/sat/integer.h"
19 
20 namespace operations_research {
21 namespace sat {
22 
23 void LinearConstraintBuilder::AddTerm(IntegerVariable var, IntegerValue coeff) {
24  // We can either add var or NegationOf(var), and we always choose the
25  // positive one.
26  if (VariableIsPositive(var)) {
27  terms_.push_back({var, coeff});
28  } else {
29  terms_.push_back({NegationOf(var), -coeff});
30  }
31 }
32 
34  IntegerValue coeff) {
35  // We can either add var or NegationOf(var), and we always choose the
36  // positive one.
37  if (expr.var != kNoIntegerVariable) {
38  if (VariableIsPositive(expr.var)) {
39  terms_.push_back({expr.var, coeff * expr.coeff});
40  } else {
41  terms_.push_back({NegationOf(expr.var), -coeff * expr.coeff});
42  }
43  }
44  if (lb_ > kMinIntegerValue) lb_ -= coeff * expr.constant;
45  if (ub_ < kMaxIntegerValue) ub_ -= coeff * expr.constant;
46 }
47 
49  if (lb_ > kMinIntegerValue) lb_ -= value;
50  if (ub_ < kMaxIntegerValue) ub_ -= value;
51 }
52 
53 ABSL_MUST_USE_RESULT bool LinearConstraintBuilder::AddLiteralTerm(
54  Literal lit, IntegerValue coeff) {
55  bool has_direct_view = encoder_.GetLiteralView(lit) != kNoIntegerVariable;
56  bool has_opposite_view =
57  encoder_.GetLiteralView(lit.Negated()) != kNoIntegerVariable;
58 
59  // If a literal has both views, we want to always keep the same
60  // representative: the smallest IntegerVariable. Note that AddTerm() will
61  // also make sure to use the associated positive variable.
62  if (has_direct_view && has_opposite_view) {
63  if (encoder_.GetLiteralView(lit) <=
64  encoder_.GetLiteralView(lit.Negated())) {
65  has_opposite_view = false;
66  } else {
67  has_direct_view = false;
68  }
69  }
70  if (has_direct_view) {
71  AddTerm(encoder_.GetLiteralView(lit), coeff);
72  return true;
73  }
74  if (has_opposite_view) {
75  AddTerm(encoder_.GetLiteralView(lit.Negated()), -coeff);
76  if (lb_ > kMinIntegerValue) lb_ -= coeff;
77  if (ub_ < kMaxIntegerValue) ub_ -= coeff;
78  return true;
79  }
80  return false;
81 }
82 
84  std::vector<std::pair<IntegerVariable, IntegerValue>>* terms,
85  LinearConstraint* constraint) {
86  constraint->vars.clear();
87  constraint->coeffs.clear();
88 
89  // Sort and add coeff of duplicate variables. Note that a variable and
90  // its negation will appear one after another in the natural order.
91  std::sort(terms->begin(), terms->end());
92  IntegerVariable previous_var = kNoIntegerVariable;
93  IntegerValue current_coeff(0);
94  for (const std::pair<IntegerVariable, IntegerValue> entry : *terms) {
95  if (previous_var == entry.first) {
96  current_coeff += entry.second;
97  } else if (previous_var == NegationOf(entry.first)) {
98  current_coeff -= entry.second;
99  } else {
100  if (current_coeff != 0) {
101  constraint->vars.push_back(previous_var);
102  constraint->coeffs.push_back(current_coeff);
103  }
104  previous_var = entry.first;
105  current_coeff = entry.second;
106  }
107  }
108  if (current_coeff != 0) {
109  constraint->vars.push_back(previous_var);
110  constraint->coeffs.push_back(current_coeff);
111  }
112 }
113 
115  LinearConstraint result;
116  result.lb = lb_;
117  result.ub = ub_;
118  CleanTermsAndFillConstraint(&terms_, &result);
119  return result;
120 }
121 
123  const LinearConstraint& constraint,
125  double activity = 0;
126  for (int i = 0; i < constraint.vars.size(); ++i) {
127  const IntegerVariable var = constraint.vars[i];
128  const IntegerValue coeff = constraint.coeffs[i];
129  activity += coeff.value() * values[var];
130  }
131  return activity;
132 }
133 
134 double ComputeL2Norm(const LinearConstraint& constraint) {
135  double sum = 0.0;
136  for (const IntegerValue coeff : constraint.coeffs) {
137  sum += ToDouble(coeff) * ToDouble(coeff);
138  }
139  return std::sqrt(sum);
140 }
141 
142 IntegerValue ComputeInfinityNorm(const LinearConstraint& constraint) {
143  IntegerValue result(0);
144  for (const IntegerValue coeff : constraint.coeffs) {
145  result = std::max(result, IntTypeAbs(coeff));
146  }
147  return result;
148 }
149 
150 double ScalarProduct(const LinearConstraint& constraint1,
151  const LinearConstraint& constraint2) {
152  DCHECK(std::is_sorted(constraint1.vars.begin(), constraint1.vars.end()));
153  DCHECK(std::is_sorted(constraint2.vars.begin(), constraint2.vars.end()));
154  double scalar_product = 0.0;
155  int index_1 = 0;
156  int index_2 = 0;
157  while (index_1 < constraint1.vars.size() &&
158  index_2 < constraint2.vars.size()) {
159  if (constraint1.vars[index_1] == constraint2.vars[index_2]) {
160  scalar_product += ToDouble(constraint1.coeffs[index_1]) *
161  ToDouble(constraint2.coeffs[index_2]);
162  index_1++;
163  index_2++;
164  } else if (constraint1.vars[index_1] > constraint2.vars[index_2]) {
165  index_2++;
166  } else {
167  index_1++;
168  }
169  }
170  return scalar_product;
171 }
172 
173 namespace {
174 
175 // TODO(user): Template for any integer type and expose this?
176 IntegerValue ComputeGcd(const std::vector<IntegerValue>& values) {
177  if (values.empty()) return IntegerValue(1);
178  int64 gcd = 0;
179  for (const IntegerValue value : values) {
180  gcd = MathUtil::GCD64(gcd, std::abs(value.value()));
181  if (gcd == 1) break;
182  }
183  if (gcd < 0) return IntegerValue(1); // Can happen with kint64min.
184  return IntegerValue(gcd);
185 }
186 
187 } // namespace
188 
189 void DivideByGCD(LinearConstraint* constraint) {
190  if (constraint->coeffs.empty()) return;
191  const IntegerValue gcd = ComputeGcd(constraint->coeffs);
192  if (gcd == 1) return;
193 
194  if (constraint->lb > kMinIntegerValue) {
195  constraint->lb = CeilRatio(constraint->lb, gcd);
196  }
197  if (constraint->ub < kMaxIntegerValue) {
198  constraint->ub = FloorRatio(constraint->ub, gcd);
199  }
200  for (IntegerValue& coeff : constraint->coeffs) coeff /= gcd;
201 }
202 
204  int new_size = 0;
205  const int size = constraint->vars.size();
206  for (int i = 0; i < size; ++i) {
207  if (constraint->coeffs[i] == 0) continue;
208  constraint->vars[new_size] = constraint->vars[i];
209  constraint->coeffs[new_size] = constraint->coeffs[i];
210  ++new_size;
211  }
212  constraint->vars.resize(new_size);
213  constraint->coeffs.resize(new_size);
214 }
215 
217  const int size = constraint->vars.size();
218  for (int i = 0; i < size; ++i) {
219  const IntegerValue coeff = constraint->coeffs[i];
220  if (coeff < 0) {
221  constraint->coeffs[i] = -coeff;
222  constraint->vars[i] = NegationOf(constraint->vars[i]);
223  }
224  }
225 }
226 
228  const int size = constraint->vars.size();
229  for (int i = 0; i < size; ++i) {
230  const IntegerVariable var = constraint->vars[i];
231  if (!VariableIsPositive(var)) {
232  constraint->coeffs[i] = -constraint->coeffs[i];
233  constraint->vars[i] = NegationOf(var);
234  }
235  }
236 }
237 
238 // TODO(user): it would be better if LinearConstraint natively supported
239 // term and not two separated vectors. Fix?
240 //
241 // TODO(user): This is really similar to CleanTermsAndFillConstraint(), maybe
242 // we should just make the later switch negative variable to positive ones to
243 // avoid an extra linear scan on each new cuts.
245  std::vector<std::pair<IntegerVariable, IntegerValue>> terms;
246 
247  const int size = ct->vars.size();
248  for (int i = 0; i < size; ++i) {
249  if (VariableIsPositive(ct->vars[i])) {
250  terms.push_back({ct->vars[i], ct->coeffs[i]});
251  } else {
252  terms.push_back({NegationOf(ct->vars[i]), -ct->coeffs[i]});
253  }
254  }
255  std::sort(terms.begin(), terms.end());
256 
257  ct->vars.clear();
258  ct->coeffs.clear();
259  for (const auto& term : terms) {
260  ct->vars.push_back(term.first);
261  ct->coeffs.push_back(term.second);
262  }
263 }
264 
266  absl::flat_hash_set<IntegerVariable> seen_variables;
267  const int size = ct.vars.size();
268  for (int i = 0; i < size; ++i) {
269  if (VariableIsPositive(ct.vars[i])) {
270  if (!seen_variables.insert(ct.vars[i]).second) return false;
271  } else {
272  if (!seen_variables.insert(NegationOf(ct.vars[i])).second) return false;
273  }
274  }
275  return true;
276 }
277 
279  LinearExpression canonical_expr;
280  canonical_expr.offset = expr.offset;
281  for (int i = 0; i < expr.vars.size(); ++i) {
282  if (expr.coeffs[i] < 0) {
283  canonical_expr.vars.push_back(NegationOf(expr.vars[i]));
284  canonical_expr.coeffs.push_back(-expr.coeffs[i]);
285  } else {
286  canonical_expr.vars.push_back(expr.vars[i]);
287  canonical_expr.coeffs.push_back(expr.coeffs[i]);
288  }
289  }
290  return canonical_expr;
291 }
292 
293 IntegerValue LinExprLowerBound(const LinearExpression& expr,
294  const IntegerTrail& integer_trail) {
295  IntegerValue lower_bound = expr.offset;
296  for (int i = 0; i < expr.vars.size(); ++i) {
297  DCHECK_GE(expr.coeffs[i], 0) << "The expression is not canonicalized";
298  lower_bound += expr.coeffs[i] * integer_trail.LowerBound(expr.vars[i]);
299  }
300  return lower_bound;
301 }
302 
303 IntegerValue LinExprUpperBound(const LinearExpression& expr,
304  const IntegerTrail& integer_trail) {
305  IntegerValue upper_bound = expr.offset;
306  for (int i = 0; i < expr.vars.size(); ++i) {
307  DCHECK_GE(expr.coeffs[i], 0) << "The expression is not canonicalized";
308  upper_bound += expr.coeffs[i] * integer_trail.UpperBound(expr.vars[i]);
309  }
310  return upper_bound;
311 }
312 
314  LinearExpression result;
315  result.vars = NegationOf(expr.vars);
316  result.coeffs = expr.coeffs;
317  result.offset = -expr.offset;
318  return result;
319 }
320 
322  LinearExpression result;
323  result.offset = expr.offset;
324  for (int i = 0; i < expr.vars.size(); ++i) {
325  if (VariableIsPositive(expr.vars[i])) {
326  result.vars.push_back(expr.vars[i]);
327  result.coeffs.push_back(expr.coeffs[i]);
328  } else {
329  result.vars.push_back(NegationOf(expr.vars[i]));
330  result.coeffs.push_back(-expr.coeffs[i]);
331  }
332  }
333  return result;
334 }
335 
336 IntegerValue GetCoefficient(const IntegerVariable var,
337  const LinearExpression& expr) {
338  for (int i = 0; i < expr.vars.size(); ++i) {
339  if (expr.vars[i] == var) {
340  return expr.coeffs[i];
341  } else if (expr.vars[i] == NegationOf(var)) {
342  return -expr.coeffs[i];
343  }
344  }
345  return IntegerValue(0);
346 }
347 
348 IntegerValue GetCoefficientOfPositiveVar(const IntegerVariable var,
349  const LinearExpression& expr) {
351  for (int i = 0; i < expr.vars.size(); ++i) {
352  if (expr.vars[i] == var) {
353  return expr.coeffs[i];
354  }
355  }
356  return IntegerValue(0);
357 }
358 
359 } // namespace sat
360 } // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK(condition)
Definition: base/logging.h:884
static int64 GCD64(int64 x, int64 y)
Definition: mathutil.h:107
const IntegerVariable GetLiteralView(Literal lit) const
Definition: integer.h:420
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff)
void AddTerm(IntegerVariable var, IntegerValue coeff)
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
IntType IntTypeAbs(IntType t)
Definition: integer.h:77
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
void RemoveZeroTerms(LinearConstraint *constraint)
LinearExpression PositiveVarExpr(const LinearExpression &expr)
double ScalarProduct(const LinearConstraint &constraint1, const LinearConstraint &constraint2)
const IntegerVariable kNoIntegerVariable(-1)
void MakeAllCoefficientsPositive(LinearConstraint *constraint)
LinearExpression CanonicalizeExpr(const LinearExpression &expr)
void CanonicalizeConstraint(LinearConstraint *ct)
bool NoDuplicateVariable(const LinearConstraint &ct)
double ComputeL2Norm(const LinearConstraint &constraint)
IntegerValue GetCoefficient(const IntegerVariable var, const LinearExpression &expr)
void MakeAllVariablesPositive(LinearConstraint *constraint)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
IntegerValue GetCoefficientOfPositiveVar(const IntegerVariable var, const LinearExpression &expr)
IntegerValue ComputeInfinityNorm(const LinearConstraint &constraint)
void CleanTermsAndFillConstraint(std::vector< std::pair< IntegerVariable, IntegerValue >> *terms, LinearConstraint *constraint)
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
bool VariableIsPositive(IntegerVariable i)
Definition: integer.h:130
void DivideByGCD(LinearConstraint *constraint)
double ComputeActivity(const LinearConstraint &constraint, const absl::StrongVector< IntegerVariable, double > &values)
double ToDouble(IntegerValue value)
Definition: integer.h:69
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::vector< IntegerVariable > vars