OR-Tools  8.2
symmetry.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
23 : SatPropagator("SymmetryPropagator"),
24 stats_("SymmetryPropagator"),
25 num_propagations_(0),
26 num_conflicts_(0) {}
27
30 LOG(INFO) << stats_.StatString();
31 LOG(INFO) << "num propagations by symmetry: " << num_propagations_;
32 LOG(INFO) << "num conflicts by symmetry: " << num_conflicts_;
33 });
34}
35
37 std::unique_ptr<SparsePermutation> permutation) {
38 if (permutation->NumCycles() == 0) return;
39 SCOPED_TIME_STAT(&stats_);
41 if (permutation->Size() > images_.size()) {
42 images_.resize(permutation->Size());
43 }
44 for (int c = 0; c < permutation->NumCycles(); ++c) {
45 int e = permutation->LastElementInCycle(c);
46 for (const int image : permutation->Cycle(c)) {
47 DCHECK_GE(LiteralIndex(e), 0);
48 DCHECK_LE(LiteralIndex(e), images_.size());
49 const int permutation_index = permutations_.size();
50 images_[LiteralIndex(e)].push_back(
51 ImageInfo(permutation_index, Literal(LiteralIndex(image))));
52 e = image;
53 }
54 }
55 permutation_trails_.push_back(std::vector<AssignedLiteralInfo>());
56 permutation_trails_.back().reserve(permutation->Support().size());
57 permutations_.emplace_back(permutation.release());
58}
59
60bool SymmetryPropagator::PropagateNext(Trail* trail) {
61 SCOPED_TIME_STAT(&stats_);
62 const Literal true_literal = (*trail)[propagation_trail_index_];
63 if (true_literal.Index() < images_.size()) {
64 const std::vector<ImageInfo>& images = images_[true_literal.Index()];
65 for (int image_index = 0; image_index < images.size(); ++image_index) {
66 const int p_index = images[image_index].permutation_index;
67
68 // TODO(user): some optim ideas: no need to enqueue if a decision image is
69 // already assigned to false. But then the Untrail() is more involved.
70 std::vector<AssignedLiteralInfo>* p_trail =
71 &(permutation_trails_[p_index]);
72 if (Enqueue(*trail, true_literal, images[image_index].image, p_trail)) {
73 continue;
74 }
75
76 // We have a non-symmetric literal and its image is not already assigned
77 // to
78 // true.
79 const AssignedLiteralInfo& non_symmetric =
80 (*p_trail)[p_trail->back().first_non_symmetric_info_index_so_far];
81
82 // If the first non-symmetric literal is a decision, then we can't deduce
83 // anything. Otherwise, it is either a conflict or a propagation.
84 const BooleanVariable non_symmetric_var =
85 non_symmetric.literal.Variable();
86 const AssignmentInfo& assignment_info = trail->Info(non_symmetric_var);
87 if (trail->AssignmentType(non_symmetric_var) ==
89 continue;
90 }
91 if (trail->Assignment().LiteralIsFalse(non_symmetric.image)) {
92 // Conflict.
93 ++num_conflicts_;
94
95 // Set the conflict on the trail.
96 // Note that we need to fetch a reason for this.
97 std::vector<Literal>* conflict = trail->MutableConflict();
98 const absl::Span<const Literal> initial_reason =
99 trail->Reason(non_symmetric.literal.Variable());
100 Permute(p_index, initial_reason, conflict);
101 conflict->push_back(non_symmetric.image);
102 for (Literal literal : *conflict) {
104 }
105
106 // Backtrack over all the enqueues we just did.
107 for (; image_index >= 0; --image_index) {
108 permutation_trails_[images[image_index].permutation_index].pop_back();
109 }
110 return false;
111 } else {
112 // Propagation.
113 if (trail->Index() >= reasons_.size()) {
114 reasons_.resize(trail->Index() + 1);
115 }
116 reasons_[trail->Index()] = {assignment_info.trail_index, p_index};
117 trail->Enqueue(non_symmetric.image, propagator_id_);
118 ++num_propagations_;
119 }
120 }
121 }
123 return true;
124}
125
127 const int old_index = trail->Index();
128 while (trail->Index() == old_index && propagation_trail_index_ < old_index) {
129 if (!PropagateNext(trail)) return false;
130 }
131 return true;
132}
133
134void SymmetryPropagator::Untrail(const Trail& trail, int trail_index) {
135 SCOPED_TIME_STAT(&stats_);
136 while (propagation_trail_index_ > trail_index) {
138 const Literal true_literal = trail[propagation_trail_index_];
139 if (true_literal.Index() < images_.size()) {
140 for (ImageInfo& info : images_[true_literal.Index()]) {
141 permutation_trails_[info.permutation_index].pop_back();
142 }
143 }
144 }
145}
146
147absl::Span<const Literal> SymmetryPropagator::Reason(const Trail& trail,
148 int trail_index) const {
149 SCOPED_TIME_STAT(&stats_);
150 const ReasonInfo& reason_info = reasons_[trail_index];
151 std::vector<Literal>* reason = trail.GetEmptyVectorToStoreReason(trail_index);
152 Permute(reason_info.symmetry_index,
153 trail.Reason(trail[reason_info.source_trail_index].Variable()),
154 reason);
155 return *reason;
156}
157
158bool SymmetryPropagator::Enqueue(const Trail& trail, Literal literal,
159 Literal image,
160 std::vector<AssignedLiteralInfo>* p_trail) {
161 // Small optimization to get the trail index of literal.
162 const int literal_trail_index = propagation_trail_index_;
163 DCHECK_EQ(literal_trail_index, trail.Info(literal.Variable()).trail_index);
164
165 // Push the new AssignedLiteralInfo on the permutation trail. Note that we
166 // don't know yet its first_non_symmetric_info_index_so_far but we know that
167 // they are increasing, so we can restart by the one of the previous
168 // AssignedLiteralInfo.
169 p_trail->push_back(AssignedLiteralInfo(
170 literal, image,
171 p_trail->empty()
172 ? 0
173 : p_trail->back().first_non_symmetric_info_index_so_far));
174 int* index = &(p_trail->back().first_non_symmetric_info_index_so_far);
175
176 // Compute first_non_symmetric_info_index_so_far.
177 while (*index < p_trail->size() &&
178 trail.Assignment().LiteralIsTrue((*p_trail)[*index].image)) {
179 // This AssignedLiteralInfo is symmetric for the full solver assignment.
180 // We test if it is also symmetric for the assignment so far:
181 if (trail.Info((*p_trail)[*index].image.Variable()).trail_index >
182 literal_trail_index) {
183 // It isn't, so we can stop the function here. We will continue the loop
184 // when this function is called again with an higher trail_index.
185 return true;
186 }
187 ++(*index);
188 }
189 return *index == p_trail->size();
190}
191
192void SymmetryPropagator::Permute(int index, absl::Span<const Literal> input,
193 std::vector<Literal>* output) const {
194 SCOPED_TIME_STAT(&stats_);
195
196 // Initialize tmp_literal_mapping_ (resize it if needed).
197 DCHECK_GE(index, 0);
198 DCHECK_LT(index, permutations_.size());
199 const SparsePermutation& permutation = *(permutations_[index].get());
200 if (permutation.Size() > tmp_literal_mapping_.size()) {
201 tmp_literal_mapping_.resize(permutation.Size());
202 for (LiteralIndex i(0); i < tmp_literal_mapping_.size(); ++i) {
203 tmp_literal_mapping_[i] = Literal(i);
204 }
205 }
206 for (int c = 0; c < permutation.NumCycles(); ++c) {
207 int e = permutation.LastElementInCycle(c);
208 for (const int image : permutation.Cycle(c)) {
209 tmp_literal_mapping_[LiteralIndex(e)] = Literal(LiteralIndex(image));
210 e = image;
211 }
212 }
213
214 // Permute the input into the output.
215 output->clear();
216 for (const Literal literal : input) {
217 if (literal.Index() < tmp_literal_mapping_.size()) {
218 output->push_back(tmp_literal_mapping_[literal.Index()]);
219 } else {
220 output->push_back(literal);
221 }
222 }
223
224 // Clean up.
225 for (const int e : permutation.Support()) {
226 tmp_literal_mapping_[LiteralIndex(e)] = Literal(LiteralIndex(e));
227 }
228}
229
230} // namespace sat
231} // namespace operations_research
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
void resize(size_type new_size)
size_type size() const
void push_back(const value_type &x)
const std::vector< int > & Support() const
std::string StatString() const
Definition: stats.cc:71
LiteralIndex Index() const
Definition: sat_base.h:84
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: symmetry.cc:147
void AddSymmetry(std::unique_ptr< SparsePermutation > permutation)
Definition: symmetry.cc:36
void Permute(int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
Definition: symmetry.cc:192
void Untrail(const Trail &trail, int trail_index) final
Definition: symmetry.cc:134
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
int AssignmentType(BooleanVariable var) const
Definition: sat_base.h:572
absl::Span< const Literal > Reason(BooleanVariable var) const
Definition: sat_base.h:581
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
const int INFO
Definition: log_severity.h:31
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
Definition: stats.h:437
#define SCOPED_TIME_STAT(stats)
Definition: stats.h:438
static constexpr int kSearchDecision
Definition: sat_base.h:223