20 #include "absl/memory/memory.h"
21 #include "absl/status/status.h"
22 #include "absl/strings/str_format.h"
23 #include "absl/strings/str_join.h"
24 #include "absl/time/clock.h"
25 #include "absl/time/time.h"
35 "Tweak the algorithm to try and minimize the support size"
36 " of the generators produced. This may negatively impact the"
37 " performance, but works great on the sat_holeXXX benchmarks"
38 " to reduce the support size.");
46 void SwapFrontAndBack(std::vector<int>* v) {
48 std::swap((*v)[0], v->back());
51 bool PartitionsAreCompatibleAfterPartIndex(
const DynamicPartition& p1,
52 const DynamicPartition& p2,
54 const int num_parts = p1.NumParts();
55 if (p2.NumParts() != num_parts)
return false;
56 for (
int p = part_index; p < num_parts; ++p) {
57 if (p1.SizeOfPart(p) != p2.SizeOfPart(p) ||
58 p1.ParentOfPart(p) != p2.ParentOfPart(p)) {
74 bool ListMapsToList(
const List& l1,
const List& l2,
75 const DynamicPermutation& permutation,
76 std::vector<bool>* tmp_node_mask) {
77 int num_elements_delta = 0;
79 for (
const int mapped_x : l2) {
81 (*tmp_node_mask)[mapped_x] =
true;
83 for (
const int x : l1) {
85 const int mapped_x = permutation.ImageOf(x);
86 if (!(*tmp_node_mask)[mapped_x]) {
90 (*tmp_node_mask)[mapped_x] =
false;
92 if (num_elements_delta != 0) match =
false;
95 for (
const int x : l2) (*tmp_node_mask)[x] =
false;
103 tmp_dynamic_permutation_(NumNodes()),
104 tmp_node_mask_(NumNodes(), false),
105 tmp_degree_(NumNodes(), 0),
106 tmp_nodes_with_degree_(NumNodes() + 1) {
109 tmp_partition_.
Reset(NumNodes());
116 reverse_adj_list_index_.assign(graph.
num_nodes() + 2, 0);
117 for (
const int node : graph.
AllNodes()) {
119 ++reverse_adj_list_index_[graph.
Head(arc) + 2];
125 std::partial_sum(reverse_adj_list_index_.begin() + 2,
126 reverse_adj_list_index_.end(),
127 reverse_adj_list_index_.begin() + 2);
131 flattened_reverse_adj_lists_.assign(graph.
num_arcs(), -1);
132 for (
const int node : graph.
AllNodes()) {
134 flattened_reverse_adj_lists_[reverse_adj_list_index_[graph.
Head(arc) +
143 for (
const int i : flattened_reverse_adj_lists_) DCHECK_NE(i, -1);
151 const int image = permutation.
ImageOf(base);
152 if (image == base)
continue;
153 if (!ListMapsToList(graph_[base], graph_[image], permutation,
158 if (!reverse_adj_list_index_.empty()) {
162 const int image = permutation.
ImageOf(base);
163 if (image == base)
continue;
164 if (!ListMapsToList(TailsOfIncomingArcsTo(base),
165 TailsOfIncomingArcsTo(image), permutation,
178 inline void IncrementCounterForNonSingletons(
const T& nodes,
180 std::vector<int>* node_count,
181 std::vector<int>* nodes_seen) {
182 for (
const int node : nodes) {
184 const int count = ++(*node_count)[node];
185 if (count == 1) nodes_seen->push_back(node);
193 std::vector<int>& tmp_nodes_with_nonzero_degree = tmp_stack_;
206 std::vector<bool> adjacency_directions(1,
true);
207 if (!reverse_adj_list_index_.empty()) {
208 adjacency_directions.push_back(
false);
210 for (
int part_index = first_unrefined_part_index;
213 for (
const bool outgoing_adjacency : adjacency_directions) {
216 if (outgoing_adjacency) {
218 IncrementCounterForNonSingletons(graph_[node], *partition,
220 &tmp_nodes_with_nonzero_degree);
224 IncrementCounterForNonSingletons(TailsOfIncomingArcsTo(node),
225 *partition, &tmp_degree_,
226 &tmp_nodes_with_nonzero_degree);
231 for (
const int node : tmp_nodes_with_nonzero_degree) {
232 const int degree = tmp_degree_[node];
233 tmp_degree_[node] = 0;
234 max_degree =
std::max(max_degree, degree);
235 tmp_nodes_with_degree_[degree].push_back(node);
237 tmp_nodes_with_nonzero_degree.clear();
240 for (
int degree = 1; degree <= max_degree; ++degree) {
241 partition->
Refine(tmp_nodes_with_degree_[degree]);
242 tmp_nodes_with_degree_[degree].clear();
250 const int original_num_parts = partition->
NumParts();
251 partition->
Refine(std::vector<int>(1, node));
255 if (new_singletons !=
nullptr) {
256 new_singletons->clear();
257 for (
int p = original_num_parts; p < partition->
NumParts(); ++p) {
261 if (!tmp_node_mask_[parent] && parent < original_num_parts &&
263 tmp_node_mask_[parent] =
true;
271 for (
int p = original_num_parts; p < partition->
NumParts(); ++p) {
278 void MergeNodeEquivalenceClassesAccordingToPermutation(
281 for (
int c = 0; c < perm.
NumCycles(); ++c) {
284 for (
const int e : perm.
Cycle(c)) {
286 const int removed_representative =
288 if (sorted_representatives !=
nullptr && removed_representative != -1) {
289 sorted_representatives->
Remove(removed_representative);
309 void GetAllOtherRepresentativesInSamePartAs(
310 int representative_node,
const DynamicPartition& partition,
311 const DenseDoublyLinkedList& representatives_sorted_by_index_in_partition,
312 MergingPartition* node_equivalence_classes,
313 std::vector<int>* pruned_other_nodes) {
314 pruned_other_nodes->clear();
315 const int part_index = partition.PartOf(representative_node);
317 int repr = representative_node;
319 DCHECK_EQ(repr, node_equivalence_classes->GetRoot(repr));
320 repr = representatives_sorted_by_index_in_partition.Prev(repr);
321 if (repr < 0 || partition.PartOf(repr) != part_index)
break;
322 pruned_other_nodes->push_back(repr);
325 repr = representative_node;
327 DCHECK_EQ(repr, node_equivalence_classes->GetRoot(repr));
328 repr = representatives_sorted_by_index_in_partition.Next(repr);
329 if (repr < 0 || partition.PartOf(repr) != part_index)
break;
330 pruned_other_nodes->push_back(repr);
338 std::vector<int> expected_output;
339 for (
const int e : partition.ElementsInPart(part_index)) {
340 if (node_equivalence_classes->GetRoot(e) != representative_node) {
341 expected_output.push_back(e);
344 node_equivalence_classes->KeepOnlyOneNodePerPart(&expected_output);
345 for (
int& x : expected_output) x = node_equivalence_classes->GetRoot(x);
346 std::sort(expected_output.begin(), expected_output.end());
347 std::vector<int> sorted_output = *pruned_other_nodes;
348 std::sort(sorted_output.begin(), sorted_output.end());
349 DCHECK_EQ(absl::StrJoin(expected_output,
" "),
350 absl::StrJoin(sorted_output,
" "));
356 double time_limit_seconds, std::vector<int>* node_equivalence_classes_io,
357 std::vector<std::unique_ptr<SparsePermutation>>* generators,
358 std::vector<int>* factorized_automorphism_group_size) {
360 time_limit_ = absl::make_unique<TimeLimit>(time_limit_seconds);
363 factorized_automorphism_group_size->clear();
364 if (node_equivalence_classes_io->size() != NumNodes()) {
365 return absl::Status(absl::StatusCode::kInvalidArgument,
366 "Invalid 'node_equivalence_classes_io'.");
375 if (time_limit_->LimitReached()) {
376 return absl::Status(absl::StatusCode::kDeadlineExceeded,
377 "During the initial refinement.");
379 VLOG(4) <<
"Base partition: "
383 std::vector<std::vector<int>> permutations_displacing_node(NumNodes());
384 std::vector<int> potential_root_image_nodes;
407 struct InvariantDiveState {
409 int num_parts_before_refinement;
411 InvariantDiveState(
int node,
int num_parts)
412 : invariant_node(node), num_parts_before_refinement(num_parts) {}
414 std::vector<InvariantDiveState> invariant_dive_stack;
421 for (
int invariant_node = 0; invariant_node < NumNodes(); ++invariant_node) {
425 invariant_dive_stack.push_back(
426 InvariantDiveState(invariant_node, base_partition.
NumParts()));
428 VLOG(4) <<
"Invariant dive: invariant node = " << invariant_node
429 <<
"; partition after: "
431 if (time_limit_->LimitReached()) {
432 return absl::Status(absl::StatusCode::kDeadlineExceeded,
433 "During the invariant dive.");
444 while (!invariant_dive_stack.empty()) {
445 if (time_limit_->LimitReached())
break;
448 const int root_node = invariant_dive_stack.back().invariant_node;
449 const int base_num_parts =
450 invariant_dive_stack.back().num_parts_before_refinement;
451 invariant_dive_stack.pop_back();
454 VLOG(4) <<
"Backtracking invariant dive: root node = " << root_node
479 GetAllOtherRepresentativesInSamePartAs(
480 root_node, base_partition, representatives_sorted_by_index_in_partition,
481 &node_equivalence_classes, &potential_root_image_nodes);
482 DCHECK(!potential_root_image_nodes.empty());
483 IF_STATS_ENABLED(stats_.invariant_unroll_time.StopTimerAndAddElapsedTime());
487 while (!potential_root_image_nodes.empty()) {
488 if (time_limit_->LimitReached())
break;
489 VLOG(4) <<
"Potential (pruned) images of root node " << root_node
490 <<
" left: [" << absl::StrJoin(potential_root_image_nodes,
" ")
492 const int root_image_node = potential_root_image_nodes.back();
493 VLOG(4) <<
"Trying image of root node: " << root_image_node;
495 std::unique_ptr<SparsePermutation> permutation =
496 FindOneSuitablePermutation(root_node, root_image_node,
497 &base_partition, &image_partition,
498 *generators, permutations_displacing_node);
500 if (permutation !=
nullptr) {
505 MergeNodeEquivalenceClassesAccordingToPermutation(
506 *permutation, &node_equivalence_classes,
507 &representatives_sorted_by_index_in_partition);
512 SwapFrontAndBack(&potential_root_image_nodes);
514 &potential_root_image_nodes);
515 SwapFrontAndBack(&potential_root_image_nodes);
518 const int permutation_index =
static_cast<int>(generators->size());
519 for (
const int node : permutation->Support()) {
520 permutations_displacing_node[node].push_back(permutation_index);
525 generators->push_back(std::move(permutation));
528 potential_root_image_nodes.pop_back();
534 factorized_automorphism_group_size->push_back(
541 if (time_limit_->LimitReached()) {
542 return absl::Status(absl::StatusCode::kDeadlineExceeded,
543 "Some automorphisms were found, but probably not all.");
545 return ::absl::OkStatus();
556 int part_index,
int* base_node,
int* image_node) {
570 if (FLAGS_minimize_permutation_support_size) {
572 for (
const int node : base_partition.
ElementsInPart(part_index)) {
573 if (image_partition.
PartOf(node) == part_index) {
574 *image_node = *base_node = node;
585 if (image_partition.
PartOf(*base_node) == part_index) {
586 *image_node = *base_node;
596 std::unique_ptr<SparsePermutation>
597 GraphSymmetryFinder::FindOneSuitablePermutation(
598 int root_node,
int root_image_node, DynamicPartition* base_partition,
599 DynamicPartition* image_partition,
600 const std::vector<std::unique_ptr<SparsePermutation>>&
601 generators_found_so_far,
602 const std::vector<std::vector<int>>& permutations_displacing_node) {
605 DCHECK_EQ(
"", tmp_dynamic_permutation_.
DebugString());
608 DCHECK(search_states_.empty());
611 std::vector<int> base_singletons;
612 std::vector<int> image_singletons;
615 int min_potential_mismatching_part_index;
616 std::vector<int> next_potential_image_nodes;
620 search_states_.emplace_back(
622 base_partition->NumParts(),
623 base_partition->NumParts());
625 search_states_.back().remaining_pruned_image_nodes.assign(1, root_image_node);
630 while (!search_states_.empty()) {
631 if (time_limit_->LimitReached())
return nullptr;
642 const SearchState& ss = search_states_.back();
643 const int image_node = ss.first_image_node >= 0
644 ? ss.first_image_node
645 : ss.remaining_pruned_image_nodes.back();
649 DCHECK_EQ(ss.num_parts_before_trying_to_map_base_node,
650 image_partition->NumParts());
659 VLOG(4) << ss.DebugString();
676 bool compatible =
true;
679 compatible = PartitionsAreCompatibleAfterPartIndex(
680 *base_partition, *image_partition,
681 ss.num_parts_before_trying_to_map_base_node);
682 u.AlsoUpdate(compatible ? &stats_.quick_compatibility_success_time
683 : &stats_.quick_compatibility_fail_time);
685 bool partitions_are_full_match =
false;
689 &stats_.dynamic_permutation_refinement_time);
690 tmp_dynamic_permutation_.
AddMappings(base_singletons, image_singletons);
693 min_potential_mismatching_part_index =
694 ss.min_potential_mismatching_part_index;
695 partitions_are_full_match = ConfirmFullMatchOrFindNextMappingDecision(
696 *base_partition, *image_partition, tmp_dynamic_permutation_,
697 &min_potential_mismatching_part_index, &next_base_node,
699 u.AlsoUpdate(partitions_are_full_match
700 ? &stats_.map_election_std_full_match_time
701 : &stats_.map_election_std_mapping_time);
703 if (compatible && partitions_are_full_match) {
704 DCHECK_EQ(min_potential_mismatching_part_index,
705 base_partition->NumParts());
711 bool is_automorphism =
true;
715 u.AlsoUpdate(is_automorphism ? &stats_.automorphism_test_success_time
716 : &stats_.automorphism_test_fail_time);
718 if (is_automorphism) {
722 std::unique_ptr<SparsePermutation> sparse_permutation(
724 VLOG(4) <<
"Automorphism found: " << sparse_permutation->DebugString();
725 const int base_num_parts =
726 search_states_[0].num_parts_before_trying_to_map_base_node;
727 base_partition->UndoRefineUntilNumPartsEqual(base_num_parts);
728 image_partition->UndoRefineUntilNumPartsEqual(base_num_parts);
729 tmp_dynamic_permutation_.
Reset();
730 search_states_.clear();
732 search_time_updater.AlsoUpdate(&stats_.search_time_success);
733 return sparse_permutation;
739 VLOG(4) <<
"Permutation candidate isn't a valid automorphism.";
740 if (base_partition->NumParts() == NumNodes()) {
749 int non_singleton_part = 0;
752 while (base_partition->SizeOfPart(non_singleton_part) == 1) {
753 ++non_singleton_part;
754 DCHECK_LT(non_singleton_part, base_partition->NumParts());
759 GetBestMapping(*base_partition, *image_partition, non_singleton_part,
760 &next_base_node, &next_image_node);
775 while (!search_states_.empty()) {
776 SearchState*
const last_ss = &search_states_.back();
777 image_partition->UndoRefineUntilNumPartsEqual(
778 last_ss->num_parts_before_trying_to_map_base_node);
779 if (last_ss->first_image_node >= 0) {
792 const int part = image_partition->PartOf(last_ss->first_image_node);
793 last_ss->remaining_pruned_image_nodes.reserve(
794 image_partition->SizeOfPart(part));
795 last_ss->remaining_pruned_image_nodes.push_back(
796 last_ss->first_image_node);
797 for (
const int e : image_partition->ElementsInPart(part)) {
798 if (e != last_ss->first_image_node) {
799 last_ss->remaining_pruned_image_nodes.push_back(e);
804 PruneOrbitsUnderPermutationsCompatibleWithPartition(
805 *image_partition, generators_found_so_far,
806 permutations_displacing_node[last_ss->first_image_node],
807 &last_ss->remaining_pruned_image_nodes);
809 SwapFrontAndBack(&last_ss->remaining_pruned_image_nodes);
810 DCHECK_EQ(last_ss->remaining_pruned_image_nodes.back(),
811 last_ss->first_image_node);
812 last_ss->first_image_node = -1;
814 last_ss->remaining_pruned_image_nodes.pop_back();
815 if (!last_ss->remaining_pruned_image_nodes.empty())
break;
817 VLOG(4) <<
"Backtracking one level up.";
818 base_partition->UndoRefineUntilNumPartsEqual(
819 last_ss->num_parts_before_trying_to_map_base_node);
824 search_states_.pop_back();
833 VLOG(4) <<
" Deepening the search.";
834 search_states_.emplace_back(
835 next_base_node, next_image_node,
836 base_partition->NumParts(),
837 min_potential_mismatching_part_index);
845 search_time_updater.AlsoUpdate(&stats_.search_time_fail);
850 GraphSymmetryFinder::TailsOfIncomingArcsTo(
int node)
const {
852 flattened_reverse_adj_lists_.begin() + reverse_adj_list_index_[node],
853 flattened_reverse_adj_lists_.begin() + reverse_adj_list_index_[node + 1]);
856 void GraphSymmetryFinder::PruneOrbitsUnderPermutationsCompatibleWithPartition(
857 const DynamicPartition& partition,
858 const std::vector<std::unique_ptr<SparsePermutation>>& permutations,
859 const std::vector<int>& permutation_indices, std::vector<int>* nodes) {
860 VLOG(4) <<
" Pruning [" << absl::StrJoin(*nodes,
", ") <<
"]";
867 if (nodes->size() <= 1)
return;
872 std::vector<int>& tmp_nodes_on_support =
874 DCHECK(tmp_nodes_on_support.empty());
878 for (
const int p : permutation_indices) {
879 const SparsePermutation& permutation = *permutations[p];
882 bool compatible =
true;
883 for (
int c = 0; c < permutation.NumCycles(); ++c) {
884 const SparsePermutation::Iterator cycle = permutation.Cycle(c);
886 partition.SizeOfPart(partition.PartOf(*cycle.begin()))) {
891 if (!compatible)
continue;
894 for (
int c = 0; c < permutation.NumCycles(); ++c) {
896 for (
const int node : permutation.Cycle(c)) {
897 if (partition.PartOf(node) != part) {
902 part = partition.PartOf(node);
906 if (!compatible)
continue;
909 MergeNodeEquivalenceClassesAccordingToPermutation(permutation,
910 &tmp_partition_,
nullptr);
911 for (
const int node : permutation.Support()) {
912 if (!tmp_node_mask_[node]) {
913 tmp_node_mask_[node] =
true;
914 tmp_nodes_on_support.push_back(node);
923 for (
const int node : tmp_nodes_on_support) {
924 tmp_node_mask_[node] =
false;
927 tmp_nodes_on_support.clear();
928 VLOG(4) <<
" Pruned: [" << absl::StrJoin(*nodes,
", ") <<
"]";
931 bool GraphSymmetryFinder::ConfirmFullMatchOrFindNextMappingDecision(
932 const DynamicPartition& base_partition,
933 const DynamicPartition& image_partition,
934 const DynamicPermutation& current_permutation_candidate,
935 int* min_potential_mismatching_part_index_io,
int* next_base_node,
936 int* next_image_node)
const {
937 *next_base_node = -1;
938 *next_image_node = -1;
942 if (!FLAGS_minimize_permutation_support_size) {
946 for (
const int loose_node : current_permutation_candidate.LooseEnds()) {
947 DCHECK_GT(base_partition.ElementsInSamePartAs(loose_node).size(), 1);
948 *next_base_node = loose_node;
949 const int root = current_permutation_candidate.RootOf(loose_node);
950 DCHECK_NE(root, loose_node);
951 if (image_partition.PartOf(root) == base_partition.PartOf(loose_node)) {
954 *next_image_node = root;
958 if (*next_base_node != -1) {
963 .ElementsInPart(base_partition.PartOf(*next_base_node))
979 const int initial_min_potential_mismatching_part_index =
980 *min_potential_mismatching_part_index_io;
981 for (; *min_potential_mismatching_part_index_io < base_partition.NumParts();
982 ++*min_potential_mismatching_part_index_io) {
983 const int p = *min_potential_mismatching_part_index_io;
984 if (base_partition.SizeOfPart(p) != 1 &&
985 base_partition.FprintOfPart(p) != image_partition.FprintOfPart(p)) {
986 GetBestMapping(base_partition, image_partition, p, next_base_node,
991 const int parent = base_partition.ParentOfPart(p);
992 if (parent < initial_min_potential_mismatching_part_index &&
993 base_partition.SizeOfPart(parent) != 1 &&
994 base_partition.FprintOfPart(parent) !=
995 image_partition.FprintOfPart(parent)) {
996 GetBestMapping(base_partition, image_partition, parent, next_base_node,
1005 for (
int p = 0; p < base_partition.NumParts(); ++p) {
1006 if (base_partition.SizeOfPart(p) != 1) {
1007 CHECK_EQ(base_partition.FprintOfPart(p),
1008 image_partition.FprintOfPart(p));
1015 std::string GraphSymmetryFinder::SearchState::DebugString()
const {
1016 return absl::StrFormat(
1017 "SearchState{ base_node=%d, first_image_node=%d,"
1018 " remaining_pruned_image_nodes=[%s],"
1019 " num_parts_before_trying_to_map_base_node=%d }",
1020 base_node, first_image_node,
1021 absl::StrJoin(remaining_pruned_image_nodes,
" "),
1022 num_parts_before_trying_to_map_base_node);