24 stats_(
"SymmetryPropagator"),
31 LOG(
INFO) <<
"num propagations by symmetry: " << num_propagations_;
32 LOG(
INFO) <<
"num conflicts by symmetry: " << num_conflicts_;
37 std::unique_ptr<SparsePermutation> permutation) {
38 if (permutation->NumCycles() == 0)
return;
41 if (permutation->Size() > images_.
size()) {
42 images_.
resize(permutation->Size());
44 for (
int c = 0; c < permutation->NumCycles(); ++c) {
45 int e = permutation->LastElementInCycle(c);
46 for (
const int image : permutation->Cycle(c)) {
49 const int permutation_index = permutations_.size();
51 ImageInfo(permutation_index,
Literal(LiteralIndex(image))));
55 permutation_trails_.push_back(std::vector<AssignedLiteralInfo>());
56 permutation_trails_.back().reserve(permutation->Support().size());
57 permutations_.emplace_back(permutation.release());
60bool SymmetryPropagator::PropagateNext(
Trail* trail) {
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;
70 std::vector<AssignedLiteralInfo>* p_trail =
71 &(permutation_trails_[p_index]);
72 if (Enqueue(*trail, true_literal, images[image_index].image, p_trail)) {
79 const AssignedLiteralInfo& non_symmetric =
80 (*p_trail)[p_trail->back().first_non_symmetric_info_index_so_far];
84 const BooleanVariable non_symmetric_var =
85 non_symmetric.literal.Variable();
86 const AssignmentInfo& assignment_info = trail->
Info(non_symmetric_var);
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) {
107 for (; image_index >= 0; --image_index) {
108 permutation_trails_[images[image_index].permutation_index].pop_back();
113 if (trail->
Index() >= reasons_.size()) {
114 reasons_.resize(trail->
Index() + 1);
116 reasons_[trail->
Index()] = {assignment_info.trail_index, p_index};
127 const int old_index = trail->
Index();
129 if (!PropagateNext(trail))
return false;
139 if (true_literal.
Index() < images_.
size()) {
140 for (ImageInfo& info : images_[true_literal.
Index()]) {
141 permutation_trails_[info.permutation_index].pop_back();
148 int trail_index)
const {
150 const ReasonInfo& reason_info = reasons_[trail_index];
152 Permute(reason_info.symmetry_index,
153 trail.
Reason(trail[reason_info.source_trail_index].Variable()),
160 std::vector<AssignedLiteralInfo>* p_trail) {
169 p_trail->push_back(AssignedLiteralInfo(
173 : p_trail->back().first_non_symmetric_info_index_so_far));
174 int*
index = &(p_trail->back().first_non_symmetric_info_index_so_far);
177 while (*index < p_trail->size() &&
182 literal_trail_index) {
189 return *
index == p_trail->size();
193 std::vector<Literal>* output)
const {
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);
206 for (
int c = 0; c < permutation.
NumCycles(); ++c) {
208 for (
const int image : permutation.
Cycle(c)) {
209 tmp_literal_mapping_[LiteralIndex(e)] =
Literal(LiteralIndex(image));
217 if (
literal.Index() < tmp_literal_mapping_.size()) {
218 output->push_back(tmp_literal_mapping_[
literal.Index()]);
225 for (
const int e : permutation.
Support()) {
226 tmp_literal_mapping_[LiteralIndex(e)] =
Literal(LiteralIndex(e));
#define DCHECK_LE(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define DCHECK_EQ(val1, val2)
void resize(size_type new_size)
void push_back(const value_type &x)
int LastElementInCycle(int i) const
const std::vector< int > & Support() const
Iterator Cycle(int i) const
std::string StatString() const
LiteralIndex Index() const
int propagation_trail_index_
bool Propagate(Trail *trail) final
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
~SymmetryPropagator() override
void AddSymmetry(std::unique_ptr< SparsePermutation > permutation)
void Permute(int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
void Untrail(const Trail &trail, int trail_index) final
void Enqueue(Literal true_literal, int propagator_id)
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
const VariablesAssignment & Assignment() const
int AssignmentType(BooleanVariable var) const
absl::Span< const Literal > Reason(BooleanVariable var) const
std::vector< Literal > * MutableConflict()
const AssignmentInfo & Info(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)
static constexpr int kSearchDecision