OR-Tools  8.2
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
16namespace operations_research {
17namespace 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
147const 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
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define VLOG(verboselevel)
Definition: base/logging.h:978
void resize(size_type new_size)
size_type size() const
void Set(IntegerType index)
Definition: bitset.h:803
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
void Resize(IntegerType size)
Definition: bitset.h:789
const std::vector< ImpliedBoundEntry > & GetImpliedBounds(IntegerVariable var)
void Add(Literal literal, IntegerLiteral integer_literal)
void ProcessIntegerTrail(Literal first_decision)
const IntegerVariable GetLiteralView(Literal lit) const
Definition: integer.h:420
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
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition: integer.h:1355
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1350
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
Definition: integer.cc:1728
bool IsOptional(IntegerVariable i) const
Definition: integer.h:622
IntVar * var
Definition: expr_array.cc:1858
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const IntegerVariable kNoIntegerVariable(-1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264