20#include "absl/log/check.h"
21#include "absl/types/span.h"
33 stats_(
"SymmetryPropagator"),
40 LOG(INFO) <<
"num propagations by symmetry: " << num_propagations_;
41 LOG(INFO) <<
"num conflicts by symmetry: " << num_conflicts_;
46 std::unique_ptr<SparsePermutation> permutation) {
47 if (permutation->NumCycles() == 0)
return;
50 if (permutation->Size() > images_.size()) {
51 images_.
resize(permutation->Size());
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();
60 ImageInfo(permutation_index,
Literal(LiteralIndex(image))));
64 permutation_trails_.push_back(std::vector<AssignedLiteralInfo>());
65 permutation_trails_.back().reserve(permutation->Support().size());
66 permutations_.emplace_back(permutation.release());
69bool SymmetryPropagator::PropagateNext(
Trail* trail) {
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;
79 std::vector<AssignedLiteralInfo>* p_trail =
80 &(permutation_trails_[p_index]);
81 if (Enqueue(*trail, true_literal, images[image_index].image, p_trail)) {
88 const AssignedLiteralInfo& non_symmetric =
89 (*p_trail)[p_trail->back().first_non_symmetric_info_index_so_far];
93 const BooleanVariable non_symmetric_var =
94 non_symmetric.literal.Variable();
95 const AssignmentInfo& assignment_info = trail->
Info(non_symmetric_var);
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) {
116 for (; image_index >= 0; --image_index) {
117 permutation_trails_[images[image_index].permutation_index].pop_back();
122 if (trail->
Index() >= reasons_.size()) {
123 reasons_.resize(trail->
Index() + 1);
125 reasons_[trail->
Index()] = {assignment_info.trail_index, p_index};
136 const int old_index = trail->
Index();
138 if (!PropagateNext(trail))
return false;
148 if (true_literal.
Index() < images_.size()) {
149 for (ImageInfo& info : images_[true_literal.
Index()]) {
150 permutation_trails_[info.permutation_index].pop_back();
157 const Trail& trail,
int trail_index, int64_t )
const {
159 const ReasonInfo& reason_info = reasons_[trail_index];
161 Permute(reason_info.symmetry_index,
162 trail.
Reason(trail[reason_info.source_trail_index].Variable()),
169 std::vector<AssignedLiteralInfo>* p_trail) {
178 p_trail->push_back(AssignedLiteralInfo(
182 : p_trail->back().first_non_symmetric_info_index_so_far));
183 int*
index = &(p_trail->back().first_non_symmetric_info_index_so_far);
191 literal_trail_index) {
198 return *
index == p_trail->size();
202 std::vector<Literal>* output)
const {
207 DCHECK_LT(
index, permutations_.size());
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) {
215 for (
int c = 0; c < permutation.
NumCycles(); ++c) {
217 for (
const int image : permutation.
Cycle(c)) {
218 tmp_literal_mapping_[LiteralIndex(e)] =
Literal(LiteralIndex(image));
226 if (
literal.Index() < tmp_literal_mapping_.size()) {
227 output->push_back(tmp_literal_mapping_[
literal.Index()]);
234 for (
const int e : permutation.
Support()) {
235 tmp_literal_mapping_[LiteralIndex(e)] =
Literal(LiteralIndex(e));
const std::vector< int > & Support() const
Iterator Cycle(int i) const
int LastElementInCycle(int i) const
std::string StatString() const
LiteralIndex Index() const
Base class for all the SAT constraints.
int propagation_trail_index_
void AddSymmetry(std::unique_ptr< SparsePermutation > permutation)
void Untrail(const Trail &trail, int trail_index) final
bool Propagate(Trail *trail) final
absl::Span< const Literal > Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final
~SymmetryPropagator() override
void Permute(int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
std::vector< Literal > * MutableConflict()
int AssignmentType(BooleanVariable var) const
void Enqueue(Literal true_literal, int propagator_id)
absl::Span< const Literal > Reason(BooleanVariable var, int64_t conflict_id=-1) const
const AssignmentInfo & Info(BooleanVariable var) const
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
const VariablesAssignment & Assignment() const
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
void push_back(const value_type &val)
void resize(size_type new_size)
In SWIG mode, we don't want anything besides these top-level includes.
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)
int32_t trail_index
The index of this assignment in the trail.
static constexpr int kSearchDecision