OR-Tools  8.2
presolve_util.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
18
19namespace operations_research {
20namespace sat {
21
22void DomainDeductions::AddDeduction(int literal_ref, int var, Domain domain) {
23 CHECK_GE(var, 0);
24 const Index index = IndexFromLiteral(literal_ref);
25 if (index >= something_changed_.size()) {
26 something_changed_.Resize(index + 1);
27 enforcement_to_vars_.resize(index.value() + 1);
28 }
29 if (var >= tmp_num_occurrences_.size()) {
30 tmp_num_occurrences_.resize(var + 1, 0);
31 }
32 const auto insert = deductions_.insert({{index, var}, domain});
33 if (insert.second) {
34 // New element.
35 something_changed_.Set(index);
36 enforcement_to_vars_[index].push_back(var);
37 } else {
38 // Existing element.
39 const Domain& old_domain = insert.first->second;
40 if (!old_domain.IsIncludedIn(domain)) {
41 insert.first->second = domain.IntersectionWith(old_domain);
42 something_changed_.Set(index);
43 }
44 }
45}
46
47std::vector<std::pair<int, Domain>> DomainDeductions::ProcessClause(
48 absl::Span<const int> clause) {
49 std::vector<std::pair<int, Domain>> result;
50
51 // We only need to process this clause if something changed since last time.
52 bool abort = true;
53 for (const int ref : clause) {
54 const Index index = IndexFromLiteral(ref);
55 if (index >= something_changed_.size()) return result;
56 if (something_changed_[index]) {
57 abort = false;
58 }
59 }
60 if (abort) return result;
61
62 // Count for each variable, how many times it appears in the deductions lists.
63 std::vector<int> to_process;
64 std::vector<int> to_clean;
65 for (const int ref : clause) {
66 const Index index = IndexFromLiteral(ref);
67 for (const int var : enforcement_to_vars_[index]) {
68 if (tmp_num_occurrences_[var] == 0) {
69 to_clean.push_back(var);
70 }
71 tmp_num_occurrences_[var]++;
72 if (tmp_num_occurrences_[var] == clause.size()) {
73 to_process.push_back(var);
74 }
75 }
76 }
77
78 // Clear the counts.
79 for (const int var : to_clean) {
80 tmp_num_occurrences_[var] = 0;
81 }
82
83 // Compute the domain unions.
84 std::vector<Domain> domains(to_process.size());
85 for (const int ref : clause) {
86 const Index index = IndexFromLiteral(ref);
87 for (int i = 0; i < to_process.size(); ++i) {
88 domains[i] = domains[i].UnionWith(
89 gtl::FindOrDieNoPrint(deductions_, {index, to_process[i]}));
90 }
91 }
92
93 for (int i = 0; i < to_process.size(); ++i) {
94 result.push_back({to_process[i], std::move(domains[i])});
95 }
96 return result;
97}
98
99namespace {
100// Helper method for variable substitution. Returns the coefficient of 'var' in
101// 'proto' and copies other terms in 'terms'.
102template <typename ProtoWithVarsAndCoeffs>
103int64 GetVarCoeffAndCopyOtherTerms(const int var,
104 const ProtoWithVarsAndCoeffs& proto,
105 std::vector<std::pair<int, int64>>* terms) {
106 bool found = false;
107 int64 var_coeff = 0;
108 const int size = proto.vars().size();
109 for (int i = 0; i < size; ++i) {
110 int ref = proto.vars(i);
111 int64 coeff = proto.coeffs(i);
112 if (!RefIsPositive(ref)) {
113 ref = NegatedRef(ref);
114 coeff = -coeff;
115 }
116
117 if (ref == var) {
118 CHECK(!found);
119 found = true;
120 var_coeff = coeff;
121 continue;
122 } else {
123 terms->push_back({ref, coeff});
124 }
125 }
126 CHECK(found);
127 return var_coeff;
128}
129
130// Helper method for variable substituion. Sorts and merges the terms in 'terms'
131// and adds them to 'proto'.
132template <typename ProtoWithVarsAndCoeffs>
133void SortAndMergeTerms(std::vector<std::pair<int, int64>>* terms,
134 ProtoWithVarsAndCoeffs* proto) {
135 proto->clear_vars();
136 proto->clear_coeffs();
137 std::sort(terms->begin(), terms->end());
138 int current_var = 0;
139 int64 current_coeff = 0;
140 for (const auto entry : *terms) {
141 CHECK(RefIsPositive(entry.first));
142 if (entry.first == current_var) {
143 current_coeff += entry.second;
144 } else {
145 if (current_coeff != 0) {
146 proto->add_vars(current_var);
147 proto->add_coeffs(current_coeff);
148 }
149 current_var = entry.first;
150 current_coeff = entry.second;
151 }
152 }
153 if (current_coeff != 0) {
154 proto->add_vars(current_var);
155 proto->add_coeffs(current_coeff);
156 }
157}
158
159// Adds all the terms from the var definition constraint with given var
160// coefficient.
161void AddTermsFromVarDefinition(const int var, const int64 var_coeff,
162 const ConstraintProto& definition,
163 std::vector<std::pair<int, int64>>* terms) {
164 const int definition_size = definition.linear().vars().size();
165 for (int i = 0; i < definition_size; ++i) {
166 int ref = definition.linear().vars(i);
167 int64 coeff = definition.linear().coeffs(i);
168 if (!RefIsPositive(ref)) {
169 ref = NegatedRef(ref);
170 coeff = -coeff;
171 }
172
173 if (ref == var) {
174 continue;
175 } else {
176 terms->push_back({ref, -coeff * var_coeff});
177 }
178 }
179}
180} // namespace
181
182void SubstituteVariable(int var, int64 var_coeff_in_definition,
183 const ConstraintProto& definition,
184 ConstraintProto* ct) {
186 CHECK_EQ(std::abs(var_coeff_in_definition), 1);
187
188 // Copy all the terms (except the one refering to var).
189 std::vector<std::pair<int, int64>> terms;
190 int64 var_coeff = GetVarCoeffAndCopyOtherTerms(var, ct->linear(), &terms);
191
192 if (var_coeff_in_definition < 0) var_coeff *= -1;
193
194 AddTermsFromVarDefinition(var, var_coeff, definition, &terms);
195
196 // The substitution is correct only if we don't loose information here.
197 // But for a constant definition rhs that is always the case.
198 bool exact = false;
199 Domain offset = ReadDomainFromProto(definition.linear());
200 offset = offset.MultiplicationBy(-var_coeff, &exact);
201 CHECK(exact);
202
203 const Domain rhs = ReadDomainFromProto(ct->linear());
204 FillDomainInProto(rhs.AdditionWith(offset), ct->mutable_linear());
205
206 SortAndMergeTerms(&terms, ct->mutable_linear());
207}
208
209} // namespace sat
210} // namespace operations_research
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
void resize(size_type new_size)
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
bool IsIncludedIn(const Domain &domain) const
Returns true iff D is included in the given domain.
Domain MultiplicationBy(int64 coeff, bool *exact=nullptr) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e * coeff}.
Domain AdditionWith(const Domain &domain) const
Returns {x ∈ Int64, ∃ a ∈ D, ∃ b ∈ domain, x = a + b}.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
IntegerType size() const
Definition: bitset.h:769
void Set(IntegerType index)
Definition: bitset.h:803
void Resize(IntegerType size)
Definition: bitset.h:789
std::vector< std::pair< int, Domain > > ProcessClause(absl::Span< const int > clause)
void AddDeduction(int literal_ref, int var, Domain domain)
CpModelProto proto
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
const Collection::value_type::second_type & FindOrDieNoPrint(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:186
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void SubstituteVariable(int var, int64 var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
bool RefIsPositive(int ref)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int index
Definition: pack.cc:508