OR-Tools  8.1
implied_bounds.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 namespace operations_research {
17 namespace sat {
18 
19 // Just display some global statistics on destruction.
21  VLOG(1) << num_deductions_ << " enqueued deductions.";
22  VLOG(1) << bounds_.size() << " implied bounds stored.";
23  VLOG(1) << num_enqueued_in_var_to_bounds_
24  << " implied bounds with view stored.";
25 }
26 
28  if (!parameters_.use_implied_bounds()) return;
29  const IntegerVariable var = integer_literal.var;
30 
31  // Update our local level-zero bound.
32  if (var >= level_zero_lower_bounds_.size()) {
33  level_zero_lower_bounds_.resize(var.value() + 1, kMinIntegerValue);
34  new_level_zero_bounds_.Resize(var + 1);
35  }
36  level_zero_lower_bounds_[var] = std::max(
37  level_zero_lower_bounds_[var], integer_trail_->LevelZeroLowerBound(var));
38 
39  // Ignore any Add() with a bound worse than the level zero one.
40  // TODO(user): Check that this never happen? it shouldn't.
41  if (integer_literal.bound <= level_zero_lower_bounds_[var]) {
42  return;
43  }
44 
45  // We skip any IntegerLiteral refering to a variable with only two consecutive
46  // possible values. This is because, once shifted this will already be a
47  // variable in [0, 1] so we shouldn't gain much by substituing it.
48  if (integer_trail_->LevelZeroLowerBound(var) + 1 >=
49  integer_trail_->LevelZeroUpperBound(var)) {
50  return;
51  }
52 
53  // Add or update the current bound.
54  const auto key = std::make_pair(literal.Index(), var);
55  auto insert_result = bounds_.insert({key, integer_literal.bound});
56  if (!insert_result.second) {
57  if (insert_result.first->second < integer_literal.bound) {
58  insert_result.first->second = integer_literal.bound;
59  } else {
60  // No new info.
61  return;
62  }
63  }
64 
65  // Check if we have any deduction. Since at least one of (literal,
66  // literal.Negated()) must be true, we can take the min bound as valid at
67  // level zero.
68  //
69  // TODO(user): Like in probing, we can also create hole in the domain if there
70  // is some implied bounds for (literal.NegatedIndex, NegagtionOf(var)) that
71  // crosses integer_literal.bound.
72  const auto it = bounds_.find(std::make_pair(literal.NegatedIndex(), var));
73  if (it != bounds_.end()) {
74  if (it->second <= level_zero_lower_bounds_[var]) {
75  // The other bounds is worse than the new level-zero bound which can
76  // happen because of lazy update, so here we just remove it.
77  bounds_.erase(it);
78  } else {
79  const IntegerValue deduction =
80  std::min(integer_literal.bound, it->second);
81  DCHECK_GT(deduction, level_zero_lower_bounds_[var]);
82  DCHECK_GT(deduction, integer_trail_->LevelZeroLowerBound(var));
83 
84  // TODO(user): support Enqueueing level zero fact at a positive level.
85  // That is, do not loose the info on backtrack. This should be doable. It
86  // is also why we return a bool in case of conflict when pushing
87  // deduction.
88  ++num_deductions_;
89  level_zero_lower_bounds_[var] = deduction;
90  new_level_zero_bounds_.Set(var);
91 
92  VLOG(1) << "Deduction old: "
94  var, integer_trail_->LevelZeroLowerBound(var))
95  << " new: " << IntegerLiteral::GreaterOrEqual(var, deduction);
96 
97  // The entries that are equal to the min no longer need to be stored once
98  // the level zero bound is enqueued.
99  if (it->second == deduction) {
100  bounds_.erase(it);
101  }
102  if (integer_literal.bound == deduction) {
103  bounds_.erase(std::make_pair(literal.Index(), var));
104 
105  // No need to update var_to_bounds_ in this case.
106  return;
107  }
108  }
109  }
110 
111  // While the code above deal correctly with optionality, we cannot just
112  // register a literal => bound for an optional variable, because the equation
113  // might end up in the LP which do not handle them correctly.
114  //
115  // TODO(user): Maybe we can handle this case somehow, as long as every
116  // constraint using this bound is protected by the variable optional literal.
117  // Alternativelly we could disable optional variable when we are at
118  // linearization level 2.
119  if (integer_trail_->IsOptional(var)) return;
120 
121  // If we have a new implied bound and the literal has a view, add it to
122  // var_to_bounds_. Note that we might add more than one entry with the same
123  // literal_view, and we will later need to lazily clean the vector up.
124  if (integer_encoder_->GetLiteralView(literal) != kNoIntegerVariable) {
125  if (var_to_bounds_.size() <= var) {
126  var_to_bounds_.resize(var.value() + 1);
127  has_implied_bounds_.Resize(var + 1);
128  }
129  ++num_enqueued_in_var_to_bounds_;
130  has_implied_bounds_.Set(var);
131  var_to_bounds_[var].push_back({integer_encoder_->GetLiteralView(literal),
132  integer_literal.bound, true});
133  } else if (integer_encoder_->GetLiteralView(literal.Negated()) !=
135  if (var_to_bounds_.size() <= var) {
136  var_to_bounds_.resize(var.value() + 1);
137  has_implied_bounds_.Resize(var + 1);
138  }
139  ++num_enqueued_in_var_to_bounds_;
140  has_implied_bounds_.Set(var);
141  var_to_bounds_[var].push_back(
142  {integer_encoder_->GetLiteralView(literal.Negated()),
143  integer_literal.bound, false});
144  }
145 }
146 
147 const std::vector<ImpliedBoundEntry>& ImpliedBounds::GetImpliedBounds(
148  IntegerVariable var) {
149  if (var >= var_to_bounds_.size()) return empty_implied_bounds_;
150 
151  // Lazily remove obsolete entries from the vector.
152  //
153  // TODO(user): Check no duplicate and remove old entry if the enforcement
154  // is tighter.
155  int new_size = 0;
156  std::vector<ImpliedBoundEntry>& ref = var_to_bounds_[var];
157  const IntegerValue level_zero_lb = std::max(
158  level_zero_lower_bounds_[var], integer_trail_->LevelZeroLowerBound(var));
159  level_zero_lower_bounds_[var] = level_zero_lb;
160  for (const ImpliedBoundEntry& entry : ref) {
161  if (entry.lower_bound <= level_zero_lb) continue;
162  ref[new_size++] = entry;
163  }
164  ref.resize(new_size);
165 
166  return ref;
167 }
168 
170  if (!parameters_.use_implied_bounds()) return;
171 
172  CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 1);
173  tmp_integer_literals_.clear();
174  integer_trail_->AppendNewBounds(&tmp_integer_literals_);
175  for (const IntegerLiteral lit : tmp_integer_literals_) {
176  Add(first_decision, lit);
177  }
178 }
179 
181  CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
182  for (const IntegerVariable var :
183  new_level_zero_bounds_.PositionsSetAtLeastOnce()) {
184  if (!integer_trail_->Enqueue(
185  IntegerLiteral::GreaterOrEqual(var, level_zero_lower_bounds_[var]),
186  {}, {})) {
187  return false;
188  }
189  }
190  new_level_zero_bounds_.SparseClearAll();
191  return sat_solver_->FinishPropagation();
192 }
193 
194 } // namespace sat
195 } // namespace operations_research
var
IntVar * var
Definition: expr_array.cc:1858
min
int64 min
Definition: alldiff_cst.cc:138
operations_research::sat::IntegerTrail::AppendNewBounds
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
Definition: integer.cc:1699
VLOG
#define VLOG(verboselevel)
Definition: base/logging.h:978
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
max
int64 max
Definition: alldiff_cst.cc:139
absl::StrongVector::size
size_type size() const
Definition: strong_vector.h:147
operations_research::sat::IntegerTrail::LevelZeroUpperBound
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition: integer.h:1338
operations_research::sat::IntegerTrail::LevelZeroLowerBound
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1333
operations_research::sat::IntegerEncoder::GetLiteralView
const IntegerVariable GetLiteralView(Literal lit) const
Definition: integer.h:420
DCHECK_GT
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::IntegerLiteral::GreaterOrEqual
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1247
operations_research::SparseBitset::Set
void Set(IntegerType index)
Definition: bitset.h:805
operations_research::sat::IntegerLiteral::var
IntegerVariable var
Definition: integer.h:189
operations_research::sat::SatSolver::CurrentDecisionLevel
int CurrentDecisionLevel() const
Definition: sat_solver.h:361
operations_research::sat::IntegerTrail::Enqueue
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:989
operations_research::SparseBitset::SparseClearAll
void SparseClearAll()
Definition: bitset.h:772
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::SparseBitset::PositionsSetAtLeastOnce
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:815
operations_research::sat::IntegerLiteral::bound
IntegerValue bound
Definition: integer.h:190
operations_research::sat::IntegerLiteral
Definition: integer.h:153
implied_bounds.h
operations_research::sat::ImpliedBounds::EnqueueNewDeductions
bool EnqueueNewDeductions()
Definition: implied_bounds.cc:180
operations_research::sat::ImpliedBounds::Add
void Add(Literal literal, IntegerLiteral integer_literal)
Definition: implied_bounds.cc:27
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::SparseBitset::Resize
void Resize(IntegerType size)
Definition: bitset.h:791
operations_research::sat::kMinIntegerValue
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
operations_research::sat::ImpliedBounds::GetImpliedBounds
const std::vector< ImpliedBoundEntry > & GetImpliedBounds(IntegerVariable var)
Definition: implied_bounds.cc:147
operations_research::sat::ImpliedBounds::~ImpliedBounds
~ImpliedBounds()
Definition: implied_bounds.cc:20
operations_research::sat::SatSolver::FinishPropagation
bool FinishPropagation()
Definition: sat_solver.cc:521
absl::StrongVector::resize
void resize(size_type new_size)
Definition: strong_vector.h:150
literal
Literal literal
Definition: optimization.cc:84
operations_research::sat::IntegerTrail::IsOptional
bool IsOptional(IntegerVariable i) const
Definition: integer.h:615
operations_research::sat::ImpliedBounds::ProcessIntegerTrail
void ProcessIntegerTrail(Literal first_decision)
Definition: implied_bounds.cc:169
operations_research::sat::ImpliedBoundEntry
Definition: implied_bounds.h:39