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 
14 #include "ortools/sat/symmetry.h"
15 
16 #include "ortools/base/int_type.h"
17 #include "ortools/base/logging.h"
18 
19 namespace operations_research {
20 namespace 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 
60 bool 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 
134 void 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 
147 absl::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 
158 bool 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 
192 void 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
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
int AssignmentType(BooleanVariable var) const
Definition: sat_base.h:572
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
absl::Span< const Literal > Reason(BooleanVariable var) const
Definition: sat_base.h:581
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
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