Google OR-Tools v9.11
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
symmetry.cc
Go to the documentation of this file.
1// Copyright 2010-2024 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#include <cstdint>
17#include <memory>
18#include <vector>
19
20#include "absl/log/check.h"
21#include "absl/types/span.h"
25#include "ortools/util/stats.h"
27
28namespace operations_research {
29namespace sat {
30
32 : SatPropagator("SymmetryPropagator"),
33 stats_("SymmetryPropagator"),
34 num_propagations_(0),
35 num_conflicts_(0) {}
36
39 LOG(INFO) << stats_.StatString();
40 LOG(INFO) << "num propagations by symmetry: " << num_propagations_;
41 LOG(INFO) << "num conflicts by symmetry: " << num_conflicts_;
42 });
43}
44
46 std::unique_ptr<SparsePermutation> permutation) {
47 if (permutation->NumCycles() == 0) return;
48 SCOPED_TIME_STAT(&stats_);
49 DCHECK_EQ(propagation_trail_index_, 0);
50 if (permutation->Size() > images_.size()) {
51 images_.resize(permutation->Size());
52 }
53 for (int c = 0; c < permutation->NumCycles(); ++c) {
54 int e = permutation->LastElementInCycle(c);
55 for (const int image : permutation->Cycle(c)) {
56 DCHECK_GE(LiteralIndex(e), 0);
57 DCHECK_LE(LiteralIndex(e), images_.size());
58 const int permutation_index = permutations_.size();
59 images_[LiteralIndex(e)].push_back(
60 ImageInfo(permutation_index, Literal(LiteralIndex(image))));
61 e = image;
62 }
63 }
64 permutation_trails_.push_back(std::vector<AssignedLiteralInfo>());
65 permutation_trails_.back().reserve(permutation->Support().size());
66 permutations_.emplace_back(permutation.release());
67}
68
69bool SymmetryPropagator::PropagateNext(Trail* trail) {
70 SCOPED_TIME_STAT(&stats_);
71 const Literal true_literal = (*trail)[propagation_trail_index_];
72 if (true_literal.Index() < images_.size()) {
73 const std::vector<ImageInfo>& images = images_[true_literal.Index()];
74 for (int image_index = 0; image_index < images.size(); ++image_index) {
75 const int p_index = images[image_index].permutation_index;
76
77 // TODO(user): some optim ideas: no need to enqueue if a decision image is
78 // already assigned to false. But then the Untrail() is more involved.
79 std::vector<AssignedLiteralInfo>* p_trail =
80 &(permutation_trails_[p_index]);
81 if (Enqueue(*trail, true_literal, images[image_index].image, p_trail)) {
82 continue;
83 }
84
85 // We have a non-symmetric literal and its image is not already assigned
86 // to
87 // true.
88 const AssignedLiteralInfo& non_symmetric =
89 (*p_trail)[p_trail->back().first_non_symmetric_info_index_so_far];
90
91 // If the first non-symmetric literal is a decision, then we can't deduce
92 // anything. Otherwise, it is either a conflict or a propagation.
93 const BooleanVariable non_symmetric_var =
94 non_symmetric.literal.Variable();
95 const AssignmentInfo& assignment_info = trail->Info(non_symmetric_var);
96 if (trail->AssignmentType(non_symmetric_var) ==
98 continue;
99 }
100 if (trail->Assignment().LiteralIsFalse(non_symmetric.image)) {
101 // Conflict.
102 ++num_conflicts_;
103
104 // Set the conflict on the trail.
105 // Note that we need to fetch a reason for this.
106 std::vector<Literal>* conflict = trail->MutableConflict();
107 const absl::Span<const Literal> initial_reason =
108 trail->Reason(non_symmetric.literal.Variable());
109 Permute(p_index, initial_reason, conflict);
110 conflict->push_back(non_symmetric.image);
111 for (Literal literal : *conflict) {
112 DCHECK(trail->Assignment().LiteralIsFalse(literal)) << literal;
113 }
114
115 // Backtrack over all the enqueues we just did.
116 for (; image_index >= 0; --image_index) {
117 permutation_trails_[images[image_index].permutation_index].pop_back();
118 }
119 return false;
120 } else {
121 // Propagation.
122 if (trail->Index() >= reasons_.size()) {
123 reasons_.resize(trail->Index() + 1);
124 }
125 reasons_[trail->Index()] = {assignment_info.trail_index, p_index};
126 trail->Enqueue(non_symmetric.image, propagator_id_);
127 ++num_propagations_;
128 }
129 }
130 }
132 return true;
133}
134
136 const int old_index = trail->Index();
137 while (trail->Index() == old_index && propagation_trail_index_ < old_index) {
138 if (!PropagateNext(trail)) return false;
139 }
140 return true;
141}
142
143void SymmetryPropagator::Untrail(const Trail& trail, int trail_index) {
144 SCOPED_TIME_STAT(&stats_);
145 while (propagation_trail_index_ > trail_index) {
147 const Literal true_literal = trail[propagation_trail_index_];
148 if (true_literal.Index() < images_.size()) {
149 for (ImageInfo& info : images_[true_literal.Index()]) {
150 permutation_trails_[info.permutation_index].pop_back();
151 }
152 }
153 }
154}
155
156absl::Span<const Literal> SymmetryPropagator::Reason(
157 const Trail& trail, int trail_index, int64_t /*conflict_id*/) const {
158 SCOPED_TIME_STAT(&stats_);
159 const ReasonInfo& reason_info = reasons_[trail_index];
160 std::vector<Literal>* reason = trail.GetEmptyVectorToStoreReason(trail_index);
161 Permute(reason_info.symmetry_index,
162 trail.Reason(trail[reason_info.source_trail_index].Variable()),
163 reason);
164 return *reason;
165}
166
167bool SymmetryPropagator::Enqueue(const Trail& trail, Literal literal,
168 Literal image,
169 std::vector<AssignedLiteralInfo>* p_trail) {
170 // Small optimization to get the trail index of literal.
171 const int literal_trail_index = propagation_trail_index_;
172 DCHECK_EQ(literal_trail_index, trail.Info(literal.Variable()).trail_index);
173
174 // Push the new AssignedLiteralInfo on the permutation trail. Note that we
175 // don't know yet its first_non_symmetric_info_index_so_far but we know that
176 // they are increasing, so we can restart by the one of the previous
177 // AssignedLiteralInfo.
178 p_trail->push_back(AssignedLiteralInfo(
179 literal, image,
180 p_trail->empty()
181 ? 0
182 : p_trail->back().first_non_symmetric_info_index_so_far));
183 int* index = &(p_trail->back().first_non_symmetric_info_index_so_far);
184
185 // Compute first_non_symmetric_info_index_so_far.
186 while (*index < p_trail->size() &&
187 trail.Assignment().LiteralIsTrue((*p_trail)[*index].image)) {
188 // This AssignedLiteralInfo is symmetric for the full solver assignment.
189 // We test if it is also symmetric for the assignment so far:
190 if (trail.Info((*p_trail)[*index].image.Variable()).trail_index >
191 literal_trail_index) {
192 // It isn't, so we can stop the function here. We will continue the loop
193 // when this function is called again with an higher trail_index.
194 return true;
195 }
196 ++(*index);
197 }
198 return *index == p_trail->size();
199}
200
201void SymmetryPropagator::Permute(int index, absl::Span<const Literal> input,
202 std::vector<Literal>* output) const {
203 SCOPED_TIME_STAT(&stats_);
204
205 // Initialize tmp_literal_mapping_ (resize it if needed).
206 DCHECK_GE(index, 0);
207 DCHECK_LT(index, permutations_.size());
208 const SparsePermutation& permutation = *(permutations_[index].get());
209 if (permutation.Size() > tmp_literal_mapping_.size()) {
210 tmp_literal_mapping_.resize(permutation.Size());
211 for (LiteralIndex i(0); i < tmp_literal_mapping_.size(); ++i) {
212 tmp_literal_mapping_[i] = Literal(i);
213 }
214 }
215 for (int c = 0; c < permutation.NumCycles(); ++c) {
216 int e = permutation.LastElementInCycle(c);
217 for (const int image : permutation.Cycle(c)) {
218 tmp_literal_mapping_[LiteralIndex(e)] = Literal(LiteralIndex(image));
219 e = image;
220 }
221 }
222
223 // Permute the input into the output.
224 output->clear();
225 for (const Literal literal : input) {
226 if (literal.Index() < tmp_literal_mapping_.size()) {
227 output->push_back(tmp_literal_mapping_[literal.Index()]);
228 } else {
229 output->push_back(literal);
230 }
231 }
232
233 // Clean up.
234 for (const int e : permutation.Support()) {
235 tmp_literal_mapping_[LiteralIndex(e)] = Literal(LiteralIndex(e));
236 }
237}
238
239} // namespace sat
240} // namespace operations_research
IntegerValue size
const std::vector< int > & Support() const
std::string StatString() const
Definition stats.cc:77
LiteralIndex Index() const
Definition sat_base.h:91
Base class for all the SAT constraints.
Definition sat_base.h:533
void AddSymmetry(std::unique_ptr< SparsePermutation > permutation)
Definition symmetry.cc:45
void Untrail(const Trail &trail, int trail_index) final
Definition symmetry.cc:143
absl::Span< const Literal > Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final
Definition symmetry.cc:156
void Permute(int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
Definition symmetry.cc:201
std::vector< Literal > * MutableConflict()
Definition sat_base.h:433
int AssignmentType(BooleanVariable var) const
Definition sat_base.h:671
void Enqueue(Literal true_literal, int propagator_id)
Definition sat_base.h:317
absl::Span< const Literal > Reason(BooleanVariable var, int64_t conflict_id=-1) const
Definition sat_base.h:680
const AssignmentInfo & Info(BooleanVariable var) const
Definition sat_base.h:463
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition sat_base.h:393
const VariablesAssignment & Assignment() const
Definition sat_base.h:462
bool LiteralIsFalse(Literal literal) const
Definition sat_base.h:185
bool LiteralIsTrue(Literal literal) const
Definition sat_base.h:188
void push_back(const value_type &val)
void resize(size_type new_size)
int literal
int index
In SWIG mode, we don't want anything besides these top-level includes.
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
Definition stats.h:417
#define SCOPED_TIME_STAT(stats)
Definition stats.h:418
int32_t trail_index
The index of this assignment in the trail.
Definition sat_base.h:263