dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
inprocess.h
Go to the documentation of this file.
1// Copyright 2024 Markus Anders
2// This file is part of dejavu 2.0.
3// See LICENSE for extended copyright information.
4
5#ifndef DEJAVU_INPROCESS_H
6#define DEJAVU_INPROCESS_H
7
8#include "dfs.h"
9#include "bfs.h"
10#include "rand.h"
11#include "components.h"
12
13namespace dejavu { namespace search_strategy {
14 // (need to nest namespaces due to C++ 14)
15
23 public:
24 // statistics
26 int h_splits_hint = INT32_MAX;
27
28 std::vector<std::pair<int, int>> inproc_can_individualize;
41 groups::orbit& orbit_partition,
42 int depth = 8, bool lower_depth = true) {
43 constexpr int test_frac = 100; // (1 / test_frac) elements used to find a better depth
44
45 local_state.use_reversible(true);
46 local_state.use_trace_early_out(lower_depth); // TODO bad for groups128, otherwise seems fine
47 local_state.use_increase_deviation(false);
48 local_state.use_split_limit(true, depth);
49
50 bool repeat = true;
51 int best_depth = depth;
52 while (repeat) {
53 repeat = false;
54 local_state.use_split_limit(true, depth);
55 for (int i = 0; i < g->v_size; ++i) {
56 if(!orbit_partition.represents_orbit(i)) continue;
57
58 local_state.T->set_hash(0);
59 local_state.reset_trace_equal();
60 const int col = local_state.c->vertex_to_col[i];
61 const int col_sz = local_state.c->ptn[col] + 1;
62 if (col_sz >= 2 && col_sz != orbit_partition.orbit_size(i)) {
63 local_state.move_to_child(g, i);
64 inv[i] = local_state.T->get_hash();
65 const int splits = local_state.get_number_of_splits();
66 local_state.move_to_parent();
67 if(test_frac * i < g->v_size && lower_depth && splits < best_depth &&
68 col == (*local_state.compare_base)[0].color) {
69 best_depth = splits;
70 }
71 if(test_frac * i >= g->v_size && lower_depth && best_depth < depth) {
72 depth = best_depth;
73 lower_depth = false;
74 repeat = true;
75 break;
76 }
77 } else {
78 inv[i] = 0;
79 }
80 }
81
82 for (int i = 0; i < g->v_size; ++i) inv[i] = inv[orbit_partition.find_orbit(i)];
83 }
84
85 local_state.use_trace_early_out(false);
86 local_state.use_increase_deviation(false);
87 local_state.use_split_limit(false);
88 }
89 std::vector<std::pair<int, int>> inproc_maybe_individualize;
91 std::vector<int> inproc_fixed_points;
92 std::vector<int> nodes;
93
95
96 void sort_nodes_map(std::vector<unsigned long>* map, int* colmap) {
97 struct comparator_map {
98 std::vector<unsigned long> *map;
99 int* colmap;
100
101 explicit comparator_map(std::vector<unsigned long> *m, int* vertex_to_col) {
102 this->map = m;
103 this->colmap = vertex_to_col;
104 }
105
106 bool operator()(const int &a, const int &b) const {
107 return (colmap[a] < colmap[b]) || ((colmap[a] == colmap[b]) && ((*map)[a] < (*map)[b]));
108 }
109 };
110 auto c = comparator_map(map, colmap);
111 std::sort(nodes.begin(), nodes.end(), c);
112 }
113
122 hash.allocate(g->v_size);
123
124 int num_of_hashs = 0;
125 for(int i = 0; i < g->v_size; ++i) nodes.push_back(i);
126 sort_nodes_map(inv.get_array(), local_state.c->vertex_to_col);
127 unsigned long last_inv = -1;
128 int last_col = local_state.c->vertex_to_col[0];
129 for(int i = 0; i < g->v_size; ++i) {
130 const int v = nodes[i];
131 const unsigned long v_inv = inv[v];
132 const int v_col = local_state.c->vertex_to_col[v];
133 if(last_col != v_col) {
134 last_col = v_col;
135 last_inv = v_inv;
136 ++num_of_hashs;
137 }
138 if(v_inv != last_inv) {
139 last_inv = v_inv;
140 ++num_of_hashs;
141 }
142 hash[v] = num_of_hashs;
143 }
144
145 g->initialize_coloring(local_state.c, hash.get_array());
146 }
147
148 void sort_nodes_map(unsigned long* map, int* colmap) {
149 struct comparator_map {
150 unsigned long *map;
151 int* colmap;
152
153 explicit comparator_map(unsigned long *m, int* vertex_to_col) {
154 this->map = m;
155 this->colmap = vertex_to_col;
156 }
157
158 bool operator()(const int &a, const int &b) const {
159 return (colmap[a] < colmap[b]) || ((colmap[a] == colmap[b]) && (map[a] < map[b]));
160 }
161 };
162 auto c = comparator_map(map, colmap);
163 std::sort(nodes.begin(), nodes.end(), c);
164 }
165
174 constexpr int col_sz_upper_bound = 16;
175 constexpr int fixed_split_limit = 8;
176
177 local_state.use_reversible(true);
178 local_state.use_trace_early_out(false);
179 local_state.use_increase_deviation(false);
180
181 markset original_colors(g->v_size);
182 for(int _col = 0; _col < g->v_size;) {
183 const int _col_sz = local_state.c->ptn[_col] + 1;
184 original_colors.set(_col);
185 _col += _col_sz;
186 }
187
188 std::vector<int> col_buffer;
189 col_buffer.reserve(col_sz_upper_bound);
190
191 // we write an invariant for every vertex
192 for(int i = 0; i < g->v_size; ++i) {
193 local_state.T->set_hash(0);
194 local_state.reset_trace_equal();
195 const int col = local_state.c->vertex_to_col[i];
196 const int col_sz = local_state.c->ptn[col] + 1;
197
198 // if vertex has non-trivial color, let's individualize
199 if(col_sz >= 2) {
200 // use split limiter
201 local_state.use_split_limit(true, fixed_split_limit);
202 local_state.move_to_child(g, i);
203 inv[i] = local_state.T->get_hash();
204 // write an invariant with one further level of bfs
205 for(int _col = 0; _col < g->v_size;) {
206 const int _col_sz = local_state.c->ptn[_col] + 1;
207 // only for small colors that were newly produced by the previous individualization
208 if (_col_sz >= 2 && _col_sz <= col_sz_upper_bound && !original_colors.get(_col)) {
209 // need to cache contents of color, since order changes through individualization
210 col_buffer.clear();
211 for (int jj = _col; jj < _col + _col_sz; ++jj) col_buffer.push_back(local_state.c->lab[jj]);
212 // now let's go through the color...
213 for (int j : col_buffer) {
214 local_state.use_split_limit(true, fixed_split_limit);
215 local_state.move_to_child(g, j);
216 inv[i] += local_state.T->get_hash();
217 local_state.move_to_parent();
218 }
219 }
220 _col += _col_sz;
221 }
222 local_state.move_to_parent();
223 } else {
224 inv[i] = 0;
225 }
226 }
227
228 local_state.use_trace_early_out(false);
229 local_state.use_increase_deviation(false);
230 local_state.use_split_limit(false);
231 }
232
237 void set_splits_hint(int splits_hint) {
238 h_splits_hint = splits_hint;
239 }
240
241
243
244 int success = 0;
245 for (auto &i: inproc_maybe_individualize) {
246 const int ind_v = i.first;
247 const int ind_col = root_save.get_coloring()->vertex_to_col[ind_v];
248 const int ind_col_sz = root_save.get_coloring()->ptn[ind_col] + 1;
249 const int orb_sz_det = i.second;
250 if(ind_col_sz > 1 && ind_col_sz == orb_sz_det) {
251 ++success;
252 }
253 }
254 return success;
255 }
256
270 ir::limited_save &root_save, int, bool use_bfs_inprocess,
271 bool use_shallow_inprocess, bool use_shallow_quadratic_inprocess, groups::orbit& orbit_partition) {
272 local_state.load_reduced_state(root_save);
273
274 const int cell_prev = root_save.get_coloring()->cells; /*< keep track how many cells we have initially*/
275 bool touched_coloring = false; /*< whether we change the root_save or not, i.e., whether we change
276 * anything */
277
278 // computes a shallow breadth-first invariant
279 if (use_shallow_inprocess && !(tree.get_finished_up_to() >= 1 && use_bfs_inprocess)) {
280 bool changed = false;
281 int its = 0;
282 int depth = std::max(std::min(h_splits_hint - 3, 16), 4);
283 //int depth = h_splits_hint;
284 do {
285 const int cell_last = local_state.c->cells;
287
288 nodes.reserve(g->v_size);
289 nodes.clear();
290
291 for (int i = 0; i < g->v_size; ++i) inv[i] = 0;
292 shallow_bfs_invariant(g, local_state, inv, orbit_partition, depth, !changed);
293 split_with_invariant(g, local_state, inv);
294
295 const int cell_after = local_state.c->cells;
296 changed = cell_after != cell_last;
297 if (changed) local_state.refine(g);
298 depth *= 2;
299 its += 1;
300 } while(changed && g->v_size != local_state.c->cells && its < 3);
301 }
302
303 // computes a shallow breadth-first invariant for 2 levels
304 if (use_shallow_quadratic_inprocess) {
306
307 nodes.reserve(g->v_size);
308 nodes.clear();
309
310 for(int i = 0; i < g->v_size; ++i) inv[i] = 0;
311 shallow_bfs_invariant2(g, local_state, inv);
312 split_with_invariant(g, local_state, inv);
313
314 const int cell_after = local_state.c->cells;
315 if (cell_after != cell_prev) {
316 local_state.refine(g);
317 }
318 }
319
320 // applies the computed breadth-first levels as a node invariant
321 if (tree.get_finished_up_to() >= 1 && use_bfs_inprocess) {
322 markset is_pruned(g->v_size);
323 tree.mark_first_level(is_pruned);
324 tree.make_node_invariant(); // "compresses" node invariant from all levels into first level
325 hash.allocate(g->v_size);
326
327 nodes.reserve(g->v_size);
328 nodes.clear();
329
330 int num_of_hashs = 0;
331
332 for(int i = 0; i < g->v_size; ++i) nodes.push_back(i);
333 sort_nodes_map(tree.get_node_invariant(), local_state.c->vertex_to_col);
334 unsigned long last_inv = (*tree.get_node_invariant())[0];
335 int last_col = local_state.c->vertex_to_col[0];
336 for(int i = 0; i < g->v_size; ++i) {
337 const int v = nodes[i];
338 const unsigned long v_inv = (*tree.get_node_invariant())[v];
339 const int v_col = local_state.c->vertex_to_col[v];
340 if(last_col != v_col) {
341 last_col = v_col;
342 last_inv = v_inv;
343 ++num_of_hashs;
344 }
345 if(v_inv != last_inv) {
346 last_inv = v_inv;
347 ++num_of_hashs;
348 }
349 hash[v] = num_of_hashs;
350 }
351
352 g->initialize_coloring(local_state.c, hash.get_array());
353 const int cell_after = local_state.c->cells;
354 if (cell_after != cell_prev) {
355 local_state.refine(g);
356 }
357 }
358
359 // performs individualizations if some of the initial cells of coloring coincide with their colors
361 if (!inproc_can_individualize.empty() || !inproc_maybe_individualize.empty()) {
362 int num_inds = 0;
363 for (auto &i: inproc_can_individualize) {
364 const int ind_v = i.first;
365 const int ind_col = local_state.c->vertex_to_col[ind_v];
366 dej_assert(i.second == local_state.c->ptn[ind_col] + 1);
367 s_grp_sz.multiply(local_state.c->ptn[ind_col] + 1);
368 local_state.move_to_child_no_trace(g, ind_v);
369 inproc_fixed_points.push_back(ind_v);
370 ++num_inds;
371 }
372 for (auto &i: inproc_maybe_individualize) {
373 const int ind_v = i.first;
374 const int ind_col = local_state.c->vertex_to_col[ind_v];
375 const int ind_col_sz = local_state.c->ptn[ind_col] + 1;
376 const int orb_sz_det = i.second;
377 if(ind_col_sz > 1 && ind_col_sz == orb_sz_det) {
378 s_grp_sz.multiply(ind_col_sz);
379 local_state.move_to_child_no_trace(g, ind_v);
380 inproc_fixed_points.push_back(ind_v);
381 ++num_inds;
382 }
383 }
384 if(num_inds > 0) orbit_partition.reset();
385 }
386
389
390 // did inprocessing succeed? if so, save the new state and report the change
391 if(cell_prev != local_state.c->cells) {
392 local_state.save_reduced_state(root_save);
393 touched_coloring = true;
394 }
395
396 return touched_coloring;
397 }
398 };
399} }
400
401#endif //DEJAVU_INPROCESS_H
Stores big numbers.
Definition: utility.h:138
void multiply(int number)
Definition: utility.h:165
Set specialized for quick resets.
Definition: ds.h:546
bool get(int pos)
Definition: ds.h:605
void set(int pos)
Definition: ds.h:616
Fixed-size array, uninitialized.
Definition: ds.h:90
T * get_array() const
Definition: ds.h:280
void allocate(int size)
Definition: ds.h:166
Compressed Schreier structure.
Definition: groups.h:1976
void determine_potential_individualization(std::vector< std::pair< int, int > > *save_to_individualize, coloring *root_coloring)
Definition: groups.h:2054
Orbit partition.
Definition: groups.h:507
int orbit_size(const int v)
Definition: groups.h:538
dej_nodiscard bool represents_orbit(const int v) const
Definition: groups.h:550
int find_orbit(const int v)
Definition: groups.h:519
Reduced IR save state.
Definition: ir.h:47
coloring * get_coloring()
Definition: ir.h:69
IR tree structure.
Definition: ir.h:1982
void make_node_invariant()
Definition: ir.h:2006
void mark_first_level(markset &marks)
Definition: ir.h:2158
std::vector< unsigned long > * get_node_invariant()
Definition: ir.h:2063
dej_nodiscard int get_finished_up_to() const
Definition: ir.h:2222
dej_nodiscard unsigned long get_hash() const
Definition: trace.h:257
void set_hash(unsigned long new_hash)
Definition: trace.h:265
Inprocessing for symmetry detection.
Definition: inprocess.h:22
void sort_nodes_map(std::vector< unsigned long > *map, int *colmap)
Definition: inprocess.h:96
void split_with_invariant(sgraph *g, ir::controller &local_state, worklist_t< unsigned long > &inv)
Definition: inprocess.h:121
std::vector< std::pair< int, int > > inproc_maybe_individualize
Definition: inprocess.h:89
static void shallow_bfs_invariant2(sgraph *g, ir::controller &local_state, worklist_t< unsigned long > &inv)
Definition: inprocess.h:173
std::vector< std::pair< int, int > > inproc_can_individualize
Definition: inprocess.h:28
void set_splits_hint(int splits_hint)
Definition: inprocess.h:237
std::vector< int > inproc_fixed_points
Definition: inprocess.h:91
void sort_nodes_map(unsigned long *map, int *colmap)
Definition: inprocess.h:148
bool inprocess(sgraph *g, ir::shared_tree &tree, groups::compressed_schreier &group, ir::controller &local_state, ir::limited_save &root_save, int, bool use_bfs_inprocess, bool use_shallow_inprocess, bool use_shallow_quadratic_inprocess, groups::orbit &orbit_partition)
Definition: inprocess.h:269
static void shallow_bfs_invariant(sgraph *g, ir::controller &local_state, worklist_t< unsigned long > &inv, groups::orbit &orbit_partition, int depth=8, bool lower_depth=true)
Definition: inprocess.h:40
int check_individualizations(ir::limited_save &root_save)
Definition: inprocess.h:242
Internal graph data structure.
Definition: graph.h:19
void initialize_coloring(ds::coloring *c, int *vertex_to_col)
Definition: graph.h:61
int v_size
Definition: graph.h:48
Definition: bfs.h:10
Controls movement in IR tree.
Definition: ir.h:130
std::vector< base_info > * compare_base
Definition: ir.h:142
void use_increase_deviation(bool deviation_inc_active)
Definition: ir.h:843
dej_nodiscard coloring * get_coloring() const
Definition: ir.h:925
coloring * c
Definition: ir.h:132
void save_reduced_state(limited_save &state)
Definition: ir.h:883
void move_to_child(sgraph *g, int v)
Definition: ir.h:989
void use_split_limit(bool use_split_limit, int limit=0)
Definition: ir.h:865
void use_reversible(const bool reversible)
Definition: ir.h:816
void use_trace_early_out(bool trace_early_out)
Definition: ir.h:831
void move_to_child_no_trace(sgraph *g, int v)
Definition: ir.h:1040
void load_reduced_state(limited_save &state)
Definition: ir.h:893
void reset_trace_equal()
Definition: ir.h:873
void move_to_parent()
Definition: ir.h:1057
int get_number_of_splits()
Definition: ir.h:415
void refine(sgraph *g)
Definition: ir.h:1050
#define dej_assert(expr)
Definition: utility.h:40