25 #include "absl/algorithm/container.h"
26 #include "absl/container/flat_hash_set.h"
27 #include "absl/flags/flag.h"
28 #include "absl/memory/memory.h"
29 #include "absl/status/status.h"
30 #include "absl/strings/str_format.h"
31 #include "absl/strings/str_join.h"
32 #include "absl/time/clock.h"
33 #include "absl/time/time.h"
41 ABSL_FLAG(
bool, minimize_permutation_support_size,
false,
42 "Tweak the algorithm to try and minimize the support size"
43 " of the generators produced. This may negatively impact the"
44 " performance, but works great on the sat_holeXXX benchmarks"
45 " to reduce the support size.");
53 std::vector<int> num_triangles(graph.num_nodes(), 0);
54 absl::flat_hash_set<std::pair<int, int>> arcs;
55 arcs.reserve(graph.num_arcs());
56 for (
int a = 0;
a < graph.num_arcs(); ++
a) {
57 arcs.insert({graph.Tail(
a), graph.Head(
a)});
59 for (
int node = 0; node < graph.num_nodes(); ++node) {
60 if (graph.OutDegree(node) > max_degree)
continue;
62 for (
int neigh1 : graph[node]) {
63 for (
int neigh2 : graph[node]) {
64 if (arcs.contains({neigh1, neigh2})) ++triangles;
67 num_triangles[node] = triangles;
72 void LocalBfs(const ::util::StaticGraph<int, int>& graph,
int source,
73 int stop_after_num_nodes, std::vector<int>* visited,
74 std::vector<int>* num_within_radius,
78 std::vector<bool>* tmp_mask) {
79 const int n = graph.num_nodes();
81 num_within_radius->clear();
82 num_within_radius->push_back(1);
83 DCHECK_EQ(tmp_mask->size(), n);
84 DCHECK(absl::c_find(*tmp_mask,
true) == tmp_mask->end());
85 visited->push_back(source);
86 (*tmp_mask)[source] =
true;
88 int next_distance_change = 1;
89 while (num_settled < visited->size()) {
90 const int from = (*visited)[num_settled++];
91 for (
const int child : graph[from]) {
92 if ((*tmp_mask)[child])
continue;
93 (*tmp_mask)[child] =
true;
94 visited->push_back(child);
96 if (num_settled == next_distance_change) {
98 num_within_radius->push_back(visited->size());
99 if (num_settled >= stop_after_num_nodes)
break;
100 next_distance_change = visited->size();
104 for (
const int node : *visited) (*tmp_mask)[node] =
false;
107 if (num_settled == visited->size()) {
108 DCHECK_GE(num_within_radius->size(), 2);
109 DCHECK_EQ(num_within_radius->back(),
110 (*num_within_radius)[num_within_radius->size() - 2]);
111 num_within_radius->pop_back();
117 void SwapFrontAndBack(std::vector<int>* v) {
122 bool PartitionsAreCompatibleAfterPartIndex(
const DynamicPartition& p1,
123 const DynamicPartition& p2,
125 const int num_parts = p1.NumParts();
126 if (p2.NumParts() != num_parts)
return false;
127 for (
int p = part_index; p < num_parts; ++p) {
128 if (p1.SizeOfPart(p) != p2.SizeOfPart(p) ||
129 p1.ParentOfPart(p) != p2.ParentOfPart(p)) {
144 template <
class List>
145 bool ListMapsToList(
const List& l1,
const List& l2,
146 const DynamicPermutation& permutation,
147 std::vector<bool>* tmp_node_mask) {
148 int num_elements_delta = 0;
150 for (
const int mapped_x : l2) {
151 ++num_elements_delta;
152 (*tmp_node_mask)[mapped_x] =
true;
154 for (
const int x : l1) {
155 --num_elements_delta;
156 const int mapped_x = permutation.ImageOf(x);
157 if (!(*tmp_node_mask)[mapped_x]) {
161 (*tmp_node_mask)[mapped_x] =
false;
163 if (num_elements_delta != 0) match =
false;
166 for (
const int x : l2) (*tmp_node_mask)[x] =
false;
174 tmp_dynamic_permutation_(NumNodes()),
175 tmp_node_mask_(NumNodes(), false),
176 tmp_degree_(NumNodes(), 0),
177 tmp_nodes_with_degree_(NumNodes() + 1) {
179 time_limit_ = &dummy_time_limit_;
180 tmp_partition_.
Reset(NumNodes());
187 reverse_adj_list_index_.assign(graph.
num_nodes() + 2, 0);
188 for (
const int node : graph.
AllNodes()) {
190 ++reverse_adj_list_index_[graph.
Head(
arc) + 2];
196 std::partial_sum(reverse_adj_list_index_.begin() + 2,
197 reverse_adj_list_index_.end(),
198 reverse_adj_list_index_.begin() + 2);
202 flattened_reverse_adj_lists_.assign(graph.
num_arcs(), -1);
203 for (
const int node : graph.
AllNodes()) {
205 flattened_reverse_adj_lists_[reverse_adj_list_index_[graph.
Head(
arc) +
214 for (
const int i : flattened_reverse_adj_lists_) DCHECK_NE(i, -1);
222 const int image = permutation.
ImageOf(base);
223 if (image == base)
continue;
224 if (!ListMapsToList(graph_[base], graph_[image], permutation,
229 if (!reverse_adj_list_index_.empty()) {
233 const int image = permutation.
ImageOf(base);
234 if (image == base)
continue;
235 if (!ListMapsToList(TailsOfIncomingArcsTo(base),
236 TailsOfIncomingArcsTo(image), permutation,
249 inline void IncrementCounterForNonSingletons(
const T&
nodes,
251 std::vector<int>* node_count,
252 std::vector<int>* nodes_seen,
253 int64_t* num_operations) {
254 *num_operations +=
nodes.end() -
nodes.begin();
255 for (
const int node :
nodes) {
257 const int count = ++(*node_count)[node];
258 if (count == 1) nodes_seen->push_back(node);
266 std::vector<int>& tmp_nodes_with_nonzero_degree = tmp_stack_;
275 int64_t num_operations = 0;
288 std::vector<bool> adjacency_directions(1,
true);
289 if (!reverse_adj_list_index_.empty()) {
290 adjacency_directions.push_back(
false);
292 for (
int part_index = first_unrefined_part_index;
295 for (
const bool outgoing_adjacency : adjacency_directions) {
298 if (outgoing_adjacency) {
300 IncrementCounterForNonSingletons(
301 graph_[node], *partition, &tmp_degree_,
302 &tmp_nodes_with_nonzero_degree, &num_operations);
306 IncrementCounterForNonSingletons(
307 TailsOfIncomingArcsTo(node), *partition, &tmp_degree_,
308 &tmp_nodes_with_nonzero_degree, &num_operations);
313 num_operations += 3 + tmp_nodes_with_nonzero_degree.size();
314 for (
const int node : tmp_nodes_with_nonzero_degree) {
315 const int degree = tmp_degree_[node];
316 tmp_degree_[node] = 0;
317 max_degree =
std::max(max_degree, degree);
318 tmp_nodes_with_degree_[degree].push_back(node);
320 tmp_nodes_with_nonzero_degree.clear();
323 for (
int degree = 1; degree <= max_degree; ++degree) {
326 num_operations += 1 + 3 * tmp_nodes_with_degree_[degree].size();
327 partition->
Refine(tmp_nodes_with_degree_[degree]);
328 tmp_nodes_with_degree_[degree].clear();
337 static_cast<double>(num_operations));
342 const int original_num_parts = partition->
NumParts();
343 partition->
Refine(std::vector<int>(1, node));
347 if (new_singletons !=
nullptr) {
348 new_singletons->clear();
349 for (
int p = original_num_parts; p < partition->
NumParts(); ++p) {
353 if (!tmp_node_mask_[parent] && parent < original_num_parts &&
355 tmp_node_mask_[parent] =
true;
363 for (
int p = original_num_parts; p < partition->
NumParts(); ++p) {
370 void MergeNodeEquivalenceClassesAccordingToPermutation(
373 for (
int c = 0; c < perm.
NumCycles(); ++c) {
376 for (
const int e : perm.
Cycle(c)) {
378 const int removed_representative =
380 if (sorted_representatives !=
nullptr && removed_representative != -1) {
381 sorted_representatives->
Remove(removed_representative);
401 void GetAllOtherRepresentativesInSamePartAs(
402 int representative_node,
const DynamicPartition& partition,
403 const DenseDoublyLinkedList& representatives_sorted_by_index_in_partition,
404 MergingPartition* node_equivalence_classes,
405 std::vector<int>* pruned_other_nodes) {
406 pruned_other_nodes->clear();
407 const int part_index = partition.PartOf(representative_node);
409 int repr = representative_node;
411 DCHECK_EQ(repr, node_equivalence_classes->GetRoot(repr));
412 repr = representatives_sorted_by_index_in_partition.Prev(repr);
413 if (repr < 0 || partition.PartOf(repr) != part_index)
break;
414 pruned_other_nodes->push_back(repr);
417 repr = representative_node;
419 DCHECK_EQ(repr, node_equivalence_classes->GetRoot(repr));
420 repr = representatives_sorted_by_index_in_partition.Next(repr);
421 if (repr < 0 || partition.PartOf(repr) != part_index)
break;
422 pruned_other_nodes->push_back(repr);
430 std::vector<int> expected_output;
431 for (
const int e : partition.ElementsInPart(part_index)) {
432 if (node_equivalence_classes->GetRoot(e) != representative_node) {
433 expected_output.push_back(e);
436 node_equivalence_classes->KeepOnlyOneNodePerPart(&expected_output);
437 for (
int& x : expected_output) x = node_equivalence_classes->GetRoot(x);
438 std::sort(expected_output.begin(), expected_output.end());
439 std::vector<int> sorted_output = *pruned_other_nodes;
440 std::sort(sorted_output.begin(), sorted_output.end());
441 DCHECK_EQ(absl::StrJoin(expected_output,
" "),
442 absl::StrJoin(sorted_output,
" "));
448 std::vector<int>* node_equivalence_classes_io,
449 std::vector<std::unique_ptr<SparsePermutation>>* generators,
450 std::vector<int>* factorized_automorphism_group_size,
456 factorized_automorphism_group_size->clear();
457 if (node_equivalence_classes_io->size() != NumNodes()) {
458 return absl::Status(absl::StatusCode::kInvalidArgument,
459 "Invalid 'node_equivalence_classes_io'.");
469 return absl::Status(absl::StatusCode::kDeadlineExceeded,
470 "During the initial refinement.");
472 VLOG(4) <<
"Base partition: "
476 std::vector<std::vector<int>> permutations_displacing_node(NumNodes());
477 std::vector<int> potential_root_image_nodes;
500 struct InvariantDiveState {
502 int num_parts_before_refinement;
504 InvariantDiveState(
int node,
int num_parts)
505 : invariant_node(node), num_parts_before_refinement(num_parts) {}
507 std::vector<InvariantDiveState> invariant_dive_stack;
514 for (
int invariant_node = 0; invariant_node < NumNodes(); ++invariant_node) {
518 invariant_dive_stack.push_back(
519 InvariantDiveState(invariant_node, base_partition.
NumParts()));
521 VLOG(4) <<
"Invariant dive: invariant node = " << invariant_node
522 <<
"; partition after: "
525 return absl::Status(absl::StatusCode::kDeadlineExceeded,
526 "During the invariant dive.");
537 while (!invariant_dive_stack.empty()) {
541 const int root_node = invariant_dive_stack.back().invariant_node;
542 const int base_num_parts =
543 invariant_dive_stack.back().num_parts_before_refinement;
544 invariant_dive_stack.pop_back();
547 VLOG(4) <<
"Backtracking invariant dive: root node = " << root_node
572 GetAllOtherRepresentativesInSamePartAs(
573 root_node, base_partition, representatives_sorted_by_index_in_partition,
574 &node_equivalence_classes, &potential_root_image_nodes);
575 DCHECK(!potential_root_image_nodes.empty());
576 IF_STATS_ENABLED(stats_.invariant_unroll_time.StopTimerAndAddElapsedTime());
580 while (!potential_root_image_nodes.empty()) {
582 VLOG(4) <<
"Potential (pruned) images of root node " << root_node
583 <<
" left: [" << absl::StrJoin(potential_root_image_nodes,
" ")
585 const int root_image_node = potential_root_image_nodes.back();
586 VLOG(4) <<
"Trying image of root node: " << root_image_node;
588 std::unique_ptr<SparsePermutation> permutation =
589 FindOneSuitablePermutation(root_node, root_image_node,
590 &base_partition, &image_partition,
591 *generators, permutations_displacing_node);
593 if (permutation !=
nullptr) {
598 MergeNodeEquivalenceClassesAccordingToPermutation(
599 *permutation, &node_equivalence_classes,
600 &representatives_sorted_by_index_in_partition);
605 SwapFrontAndBack(&potential_root_image_nodes);
607 &potential_root_image_nodes);
608 SwapFrontAndBack(&potential_root_image_nodes);
611 const int permutation_index =
static_cast<int>(generators->size());
612 for (
const int node : permutation->Support()) {
613 permutations_displacing_node[node].push_back(permutation_index);
618 generators->push_back(std::move(permutation));
621 potential_root_image_nodes.pop_back();
627 factorized_automorphism_group_size->push_back(
635 return absl::Status(absl::StatusCode::kDeadlineExceeded,
636 "Some automorphisms were found, but probably not all.");
638 return ::absl::OkStatus();
649 int part_index,
int* base_node,
int* image_node) {
663 if (absl::GetFlag(FLAGS_minimize_permutation_support_size)) {
665 for (
const int node : base_partition.
ElementsInPart(part_index)) {
666 if (image_partition.
PartOf(node) == part_index) {
667 *image_node = *base_node = node;
678 if (image_partition.
PartOf(*base_node) == part_index) {
679 *image_node = *base_node;
689 std::unique_ptr<SparsePermutation>
690 GraphSymmetryFinder::FindOneSuitablePermutation(
691 int root_node,
int root_image_node, DynamicPartition* base_partition,
692 DynamicPartition* image_partition,
693 const std::vector<std::unique_ptr<SparsePermutation>>&
694 generators_found_so_far,
695 const std::vector<std::vector<int>>& permutations_displacing_node) {
698 DCHECK_EQ(
"", tmp_dynamic_permutation_.
DebugString());
701 DCHECK(search_states_.empty());
704 std::vector<int> base_singletons;
705 std::vector<int> image_singletons;
708 int min_potential_mismatching_part_index;
709 std::vector<int> next_potential_image_nodes;
713 search_states_.emplace_back(
715 base_partition->NumParts(),
716 base_partition->NumParts());
718 search_states_.back().remaining_pruned_image_nodes.assign(1, root_image_node);
723 while (!search_states_.empty()) {
735 const SearchState& ss = search_states_.back();
736 const int image_node = ss.first_image_node >= 0
737 ? ss.first_image_node
738 : ss.remaining_pruned_image_nodes.back();
742 DCHECK_EQ(ss.num_parts_before_trying_to_map_base_node,
743 image_partition->NumParts());
752 VLOG(4) << ss.DebugString();
769 bool compatible =
true;
772 compatible = PartitionsAreCompatibleAfterPartIndex(
773 *base_partition, *image_partition,
774 ss.num_parts_before_trying_to_map_base_node);
775 u.AlsoUpdate(compatible ? &stats_.quick_compatibility_success_time
776 : &stats_.quick_compatibility_fail_time);
778 bool partitions_are_full_match =
false;
782 &stats_.dynamic_permutation_refinement_time);
783 tmp_dynamic_permutation_.
AddMappings(base_singletons, image_singletons);
786 min_potential_mismatching_part_index =
787 ss.min_potential_mismatching_part_index;
788 partitions_are_full_match = ConfirmFullMatchOrFindNextMappingDecision(
789 *base_partition, *image_partition, tmp_dynamic_permutation_,
790 &min_potential_mismatching_part_index, &next_base_node,
792 u.AlsoUpdate(partitions_are_full_match
793 ? &stats_.map_election_std_full_match_time
794 : &stats_.map_election_std_mapping_time);
796 if (compatible && partitions_are_full_match) {
797 DCHECK_EQ(min_potential_mismatching_part_index,
798 base_partition->NumParts());
804 bool is_automorphism =
true;
808 u.AlsoUpdate(is_automorphism ? &stats_.automorphism_test_success_time
809 : &stats_.automorphism_test_fail_time);
811 if (is_automorphism) {
815 std::unique_ptr<SparsePermutation> sparse_permutation(
817 VLOG(4) <<
"Automorphism found: " << sparse_permutation->DebugString();
818 const int base_num_parts =
819 search_states_[0].num_parts_before_trying_to_map_base_node;
820 base_partition->UndoRefineUntilNumPartsEqual(base_num_parts);
821 image_partition->UndoRefineUntilNumPartsEqual(base_num_parts);
822 tmp_dynamic_permutation_.
Reset();
823 search_states_.clear();
825 search_time_updater.AlsoUpdate(&stats_.search_time_success);
826 return sparse_permutation;
832 VLOG(4) <<
"Permutation candidate isn't a valid automorphism.";
833 if (base_partition->NumParts() == NumNodes()) {
844 int non_singleton_part = 0;
847 while (base_partition->SizeOfPart(non_singleton_part) == 1) {
848 ++non_singleton_part;
849 DCHECK_LT(non_singleton_part, base_partition->NumParts());
853 1e-9 *
static_cast<double>(non_singleton_part));
857 GetBestMapping(*base_partition, *image_partition, non_singleton_part,
858 &next_base_node, &next_image_node);
873 while (!search_states_.empty()) {
874 SearchState*
const last_ss = &search_states_.back();
875 image_partition->UndoRefineUntilNumPartsEqual(
876 last_ss->num_parts_before_trying_to_map_base_node);
877 if (last_ss->first_image_node >= 0) {
890 const int part = image_partition->PartOf(last_ss->first_image_node);
891 last_ss->remaining_pruned_image_nodes.reserve(
892 image_partition->SizeOfPart(part));
893 last_ss->remaining_pruned_image_nodes.push_back(
894 last_ss->first_image_node);
895 for (
const int e : image_partition->ElementsInPart(part)) {
896 if (e != last_ss->first_image_node) {
897 last_ss->remaining_pruned_image_nodes.push_back(e);
902 PruneOrbitsUnderPermutationsCompatibleWithPartition(
903 *image_partition, generators_found_so_far,
904 permutations_displacing_node[last_ss->first_image_node],
905 &last_ss->remaining_pruned_image_nodes);
907 SwapFrontAndBack(&last_ss->remaining_pruned_image_nodes);
908 DCHECK_EQ(last_ss->remaining_pruned_image_nodes.back(),
909 last_ss->first_image_node);
910 last_ss->first_image_node = -1;
912 last_ss->remaining_pruned_image_nodes.pop_back();
913 if (!last_ss->remaining_pruned_image_nodes.empty())
break;
915 VLOG(4) <<
"Backtracking one level up.";
916 base_partition->UndoRefineUntilNumPartsEqual(
917 last_ss->num_parts_before_trying_to_map_base_node);
922 search_states_.pop_back();
931 VLOG(4) <<
" Deepening the search.";
932 search_states_.emplace_back(
933 next_base_node, next_image_node,
934 base_partition->NumParts(),
935 min_potential_mismatching_part_index);
943 search_time_updater.AlsoUpdate(&stats_.search_time_fail);
948 GraphSymmetryFinder::TailsOfIncomingArcsTo(
int node)
const {
950 flattened_reverse_adj_lists_.begin() + reverse_adj_list_index_[node],
951 flattened_reverse_adj_lists_.begin() + reverse_adj_list_index_[node + 1]);
954 void GraphSymmetryFinder::PruneOrbitsUnderPermutationsCompatibleWithPartition(
955 const DynamicPartition& partition,
956 const std::vector<std::unique_ptr<SparsePermutation>>& permutations,
957 const std::vector<int>& permutation_indices, std::vector<int>*
nodes) {
958 VLOG(4) <<
" Pruning [" << absl::StrJoin(*
nodes,
", ") <<
"]";
965 if (
nodes->size() <= 1)
return;
970 std::vector<int>& tmp_nodes_on_support =
972 DCHECK(tmp_nodes_on_support.empty());
976 for (
const int p : permutation_indices) {
977 const SparsePermutation& permutation = *permutations[p];
980 bool compatible =
true;
981 for (
int c = 0; c < permutation.NumCycles(); ++c) {
982 const SparsePermutation::Iterator cycle = permutation.Cycle(c);
984 partition.SizeOfPart(partition.PartOf(*cycle.begin()))) {
989 if (!compatible)
continue;
992 for (
int c = 0; c < permutation.NumCycles(); ++c) {
994 for (
const int node : permutation.Cycle(c)) {
995 if (partition.PartOf(node) != part) {
1000 part = partition.PartOf(node);
1004 if (!compatible)
continue;
1007 MergeNodeEquivalenceClassesAccordingToPermutation(permutation,
1008 &tmp_partition_,
nullptr);
1009 for (
const int node : permutation.Support()) {
1010 if (!tmp_node_mask_[node]) {
1011 tmp_node_mask_[node] =
true;
1012 tmp_nodes_on_support.push_back(node);
1021 for (
const int node : tmp_nodes_on_support) {
1022 tmp_node_mask_[node] =
false;
1025 tmp_nodes_on_support.clear();
1026 VLOG(4) <<
" Pruned: [" << absl::StrJoin(*
nodes,
", ") <<
"]";
1029 bool GraphSymmetryFinder::ConfirmFullMatchOrFindNextMappingDecision(
1030 const DynamicPartition& base_partition,
1031 const DynamicPartition& image_partition,
1032 const DynamicPermutation& current_permutation_candidate,
1033 int* min_potential_mismatching_part_index_io,
int* next_base_node,
1034 int* next_image_node)
const {
1035 *next_base_node = -1;
1036 *next_image_node = -1;
1040 if (!absl::GetFlag(FLAGS_minimize_permutation_support_size)) {
1044 for (
const int loose_node : current_permutation_candidate.LooseEnds()) {
1045 DCHECK_GT(base_partition.ElementsInSamePartAs(loose_node).size(), 1);
1046 *next_base_node = loose_node;
1047 const int root = current_permutation_candidate.RootOf(loose_node);
1048 DCHECK_NE(root, loose_node);
1049 if (image_partition.PartOf(root) == base_partition.PartOf(loose_node)) {
1052 *next_image_node = root;
1056 if (*next_base_node != -1) {
1061 .ElementsInPart(base_partition.PartOf(*next_base_node))
1077 const int initial_min_potential_mismatching_part_index =
1078 *min_potential_mismatching_part_index_io;
1079 for (; *min_potential_mismatching_part_index_io < base_partition.NumParts();
1080 ++*min_potential_mismatching_part_index_io) {
1081 const int p = *min_potential_mismatching_part_index_io;
1082 if (base_partition.SizeOfPart(p) != 1 &&
1083 base_partition.FprintOfPart(p) != image_partition.FprintOfPart(p)) {
1084 GetBestMapping(base_partition, image_partition, p, next_base_node,
1089 const int parent = base_partition.ParentOfPart(p);
1090 if (parent < initial_min_potential_mismatching_part_index &&
1091 base_partition.SizeOfPart(parent) != 1 &&
1092 base_partition.FprintOfPart(parent) !=
1093 image_partition.FprintOfPart(parent)) {
1094 GetBestMapping(base_partition, image_partition, parent, next_base_node,
1103 for (
int p = 0; p < base_partition.NumParts(); ++p) {
1104 if (base_partition.SizeOfPart(p) != 1) {
1105 CHECK_EQ(base_partition.FprintOfPart(p),
1106 image_partition.FprintOfPart(p));
1113 std::string GraphSymmetryFinder::SearchState::DebugString()
const {
1114 return absl::StrFormat(
1115 "SearchState{ base_node=%d, first_image_node=%d,"
1116 " remaining_pruned_image_nodes=[%s],"
1117 " num_parts_before_trying_to_map_base_node=%d }",
1118 base_node, first_image_node,
1119 absl::StrJoin(remaining_pruned_image_nodes,
" "),
1120 num_parts_before_trying_to_map_base_node);
IterablePart ElementsInPart(int i) const
void Refine(const std::vector< int > &distinguished_subset)
const std::vector< int > & ElementsInHierarchicalOrder() const
int SizeOfPart(int part) const
void UndoRefineUntilNumPartsEqual(int original_num_parts)
IterablePart ElementsInSamePartAs(int i) const
int PartOf(int element) const
int ParentOfPart(int part) const
std::string DebugString(DebugStringSorting sorting) const
const int NumParts() const
std::unique_ptr< SparsePermutation > CreateSparsePermutation() const
std::string DebugString() const
const std::vector< int > & AllMappingsSrc() const
void UndoLastMappings(std::vector< int > *undone_mapping_src)
void AddMappings(const std::vector< int > &src, const std::vector< int > &dst)
void RecursivelyRefinePartitionByAdjacency(int first_unrefined_part_index, DynamicPartition *partition)
bool IsGraphAutomorphism(const DynamicPermutation &permutation) const
void DistinguishNodeInPartition(int node, DynamicPartition *partition, std::vector< int > *new_singletons_or_null)
absl::Status FindSymmetries(std::vector< int > *node_equivalence_classes_io, std::vector< std::unique_ptr< SparsePermutation > > *generators, std::vector< int > *factorized_automorphism_group_size, TimeLimit *time_limit=nullptr)
GraphSymmetryFinder(const Graph &graph, bool is_undirected)
int NumNodesInSamePartAs(int node)
void Reset(int num_nodes)
int MergePartsOf(int node1, int node2)
int FillEquivalenceClasses(std::vector< int > *node_equivalence_classes)
void KeepOnlyOneNodePerPart(std::vector< int > *nodes)
Iterator Cycle(int i) const
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
ArcIndexType num_arcs() const
NodeIndexType num_nodes() const
IntegerRange< NodeIndex > AllNodes() const
NodeIndexType Head(ArcIndexType arc) const
BeginEndWrapper< OutgoingArcIterator > OutgoingArcs(NodeIndexType node) const
ModelSharedTimeLimit * time_limit
ABSL_FLAG(bool, minimize_permutation_support_size, false, "Tweak the algorithm to try and minimize the support size" " of the generators produced. This may negatively impact the" " performance, but works great on the sat_holeXXX benchmarks" " to reduce the support size.")
void swap(IdMap< K, V > &a, IdMap< K, V > &b)
Collection of objects used to extend the Constraint Solver library.
std::vector< int > CountTriangles(const ::util::StaticGraph< int, int > &graph, int max_degree)
DisabledScopedTimeDistributionUpdater ScopedTimeDistributionUpdater
void LocalBfs(const ::util::StaticGraph< int, int > &graph, int source, int stop_after_num_nodes, std::vector< int > *visited, std::vector< int > *num_within_radius, std::vector< bool > *tmp_mask)
bool GraphIsSymmetric(const Graph &graph)
#define IF_STATS_ENABLED(instructions)
std::vector< int >::const_iterator begin() const
#define VLOG(verboselevel)