dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
dfs.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_DFS_H
6#define DEJAVU_DFS_H
7
8#include <random>
9#include <chrono>
10#include "refinement.h"
11#include "coloring.h"
12#include "graph.h"
13#include "trace.h"
14#include "groups.h"
15#include "ir.h"
16
17namespace dejavu {
18
25 namespace search_strategy {
26
27
28// static bool check_matched(coloring& c1, coloring& c2) {
29// markset test(c1.domain_size);
30// for(int i = 0; i < c1.domain_size; ) {
31// int col_sz = c1.ptn[i] + 1;
32// if(c2.ptn[i] + 1 != col_sz) {
33// return false;
34// }
35// if(col_sz == 1) {
36// i += col_sz;
37// continue;
38// }
39// for(int j = i; j < i + col_sz; ++j) {
40// test.set(c1.lab[j]);
41// }
42// for(int j = i; j < i + col_sz; ++j) {
43// if(!test.get(c2.lab[j])) {
44// return false;
45// }
46// }
47// test.reset();
48// i += col_sz;
49// }
50//
51// return true;
52// }
53
60 class dfs_ir {
61 int cost_snapshot = 0;
62 timed_print& ws_printer;
63 groups::automorphism_workspace& ws_automorphism;
64
65 public:
75 explicit dfs_ir(timed_print& printer, groups::automorphism_workspace& automorphism) :
76 ws_printer(printer), ws_automorphism(automorphism) {}
77
79 bool recurse=false) {
80 if(!recurse) {
81 const bool is_diffed_pre = state_right.update_diff_vertices_last_individualization(state_left);
82 if (!is_diffed_pre || state_right.get_diff_diverge()) return 2;
83 }
84
85 while (state_right.c->cells < g->v_size) {
86 // pick a color that prevents the "matching OPP"
87
88 // pick vertices that differ in the color
89 int ind_v_right, ind_v_left;
90 std::tie(ind_v_left, ind_v_right) = state_right.diff_pair(state_left);
91
92 const int col = state_left.c->vertex_to_col[ind_v_left];
93
94 dej_assert(col >= 0);
95 dej_assert(col < g->v_size);
96 const int col_sz_right = state_right.c->ptn[col] + 1;
97 const int col_sz_left = state_left.c->ptn[col] + 1;
98
99 dej_assert(col_sz_right > 1);
100 dej_assert(col_sz_left > 1);
101
102 if (col_sz_right < 2 || col_sz_left != col_sz_right) return 0;
103
104 dej_assert(ind_v_left >= -1);
105 dej_assert(ind_v_right >= -1);
106
107 dej_assert(state_left.c->vertex_to_col[ind_v_left] == col);
108 dej_assert(state_right.c->vertex_to_col[ind_v_right] == col);
109 dej_assert(state_left.c->vertex_to_col[ind_v_right] != col);
110
111 state_right.use_trace_early_out(false);
112 state_left.use_trace_early_out(false);
113 state_right.T->reset_trace_unequal();
114 state_left.T->reset_trace_unequal();
115
116 // individualize a vertex of base color
117 state_right.move_to_child(g, ind_v_right);
118 state_left.move_to_child(g, ind_v_left);
119
120 // invariant differs
121 if(state_right.T->get_hash() != state_left.T->get_hash()) return 0;
122
123 // can not perform diff udpates on this (AKA invariant should have differed, but is not
124 // guaranteed to differ always)
125 const bool is_diffed = state_right.update_diff_vertices_last_individualization(state_left);
126 if(state_left.get_diff_diverge()) return 0;
127
128 // no difference? check for automorphism now -- if it doesn't succeed there is no hope on this path
129 if(!is_diffed) {
130 ws_automorphism.reset();
131 state_right.singleton_automorphism(state_left, ws_automorphism);
132 const bool found_auto = state_right.certify(g, ws_automorphism);
133 return found_auto;
134 }
135
136 dej_assert(state_right.c->cells < g->v_size); // there can not be diff on a leaf
137 }
138
139 // unreachable
140 dej_assert(false);
141 return false;
142 }
143
145
146 int do_paired_dfs(dejavu_hook* hook, sgraph *g, ir::controller &state_left, ir::controller& state_right,
147 std::vector<std::pair<int, int>>& computed_orbits, bool prune = true) {
148 if(state_right.s_base_pos == 1) return do_simple_dfs(hook, g, state_right, computed_orbits, prune);
149
150 if(h_recent_cost_snapshot_limit < 0) return state_right.s_base_pos;
151 s_grp_sz.mantissa = 1.0;
152 s_grp_sz.exponent = 0;
153
154 // orbit algorithm structure
156 markset orbit_handled(g->v_size);
158
159 // automorphism workspace
160 ws_automorphism.reset();
161
162 // saucy strategy of paired states
163 state_left.link_compare(&state_right);
164
165 // we want to terminate if things become to costly, we save the current trace position to track cost
166 cost_snapshot = state_right.T->get_position();
167
168 // tell the controller we are performing DFS now
169 state_right.mode_compare_base();
170
171 int failed_first_level = -1;
172
173 // abort criteria
174 double recent_cost_snapshot = 0;
175 bool fail = false;
176 int trace_pos_reset = 0;
177
178 // loop that serves to optimize Tinhofer graphs
179 while ((recent_cost_snapshot < h_recent_cost_snapshot_limit || state_right.s_base_pos <= 1) &&
180 state_right.s_base_pos > 0 && !fail) {
181 // backtrack one level
182 state_right.move_to_parent();
183
184 // remember which color we are individualizing
185 const int col = (*state_right.compare_base)[state_right.s_base_pos].color;
186 const int base_vertex = (*state_right.compare_base_vertex)[state_right.s_base_pos]; // base vertex
187 const int col_sz = state_right.c->ptn[col] + 1;
188
189 if((state_right.s_base_pos & 0x00000FFF) == 0x00000FFD)
190 ws_printer.progress_current_method("dfs", "base_pos",
191 static_cast<double>(state_right.compare_base->size())
192 -state_right.s_base_pos, "cost_snapshot", recent_cost_snapshot);
193 dej_assert(col_sz >= 2);
195
196 int prune_cost_snapshot = 0; /*< if we prune, keep track of how costly it is */
197 orbit_handled.reset();
198
199 // iterate over current color class
200 for (int i = 0; i < col_sz; ++i) {
201 int ind_v = state_right.leaf_color.lab[col + i];
202 dej_assert(state_right.c->vertex_to_col[base_vertex] == state_right.c->vertex_to_col[ind_v]);
203
204 // only consider every orbit once
205 if(orbs.are_in_same_orbit(ind_v, base_vertex)) continue;
206 //if(!orbs.represents_orbit(ind_v)) continue;
207 if(!orbs.represents_orbit(ind_v)) ind_v = orbs.find_orbit(ind_v);
208 if(orbit_handled.get(ind_v)) continue;
209 orbit_handled.set(ind_v);
210
211
212 // track cost of this refinement for whatever is to come
213 const int cost_start = state_right.T->get_position();
214
215 // put the "left" state in the correct base position
216 while (state_left.s_base_pos > state_right.s_base_pos) state_left.move_to_parent();
217 state_left.T->set_position(state_right.T->get_position());
218 dej_assert(state_left.c->vertex_to_col[base_vertex] == state_left.c->vertex_to_col[ind_v]);
219 dej_assert(state_left.s_base_pos == state_right.s_base_pos);
220 dej_assert(state_left.T->get_position() == state_right.T->get_position());
221
222 // reset difference, since state_left and state_right are in the same node of the tree
223 // now -- so there is no difference
224 state_right.reset_diff();
225
226 // perform individualization-refinement in state_right
227 //TODO make a mode for this in the IR controller module
228 const int prev_base_pos = state_right.s_base_pos;
229 trace_pos_reset = state_right.T->get_position();
230 state_right.T->reset_trace_equal();
231 state_right.use_trace_early_out(true);
232 state_right.move_to_child(g, ind_v);
233
234 bool pruned = !state_right.T->trace_equal();
235 bool found_auto = false;
236
237 dej_assert(state_right.c->vertex_to_col[ind_v] ==
238 state_right.leaf_color.vertex_to_col[base_vertex]);
239
240 if(!pruned) {
241 // write singleton diff into automorphism...
242 const int wr_pos_st = state_right.base[state_right.base.size() - 1].singleton_pt;
243 const int wr_pos_end = (int) state_right.singletons.size();
244
245 ws_automorphism.reset();
246 // ... and then check whether this implies a (sparse) automorphism
247 ws_automorphism.write_singleton(state_right.compare_singletons,
248 &state_right.singletons, wr_pos_st,
249 wr_pos_end);
250 if(g->v_size != state_right.c->cells) ws_automorphism.cycle_completion(workspace);
251
252 found_auto = state_right.certify(g, ws_automorphism);
253
254 dej_assert(ws_automorphism.p()[base_vertex] == ind_v);
255 // if no luck with sparse automorphism, try more proper walk to leaf node
256 if (!found_auto) {
257 ws_automorphism.reset();
258
259 state_left.T->reset_trace_equal();
260 state_left.T->set_position(trace_pos_reset);
261 state_left.use_trace_early_out(true);
262 state_left.move_to_child(g, base_vertex); // need to move left to base vertex
263
264 dej_assert(state_left.T->trace_equal());
265 dej_assert(state_left.T->get_position() == state_right.T->get_position());
266
267 auto return_code = paired_recurse_to_equal_leaf(g, state_left, state_right);
268 found_auto = (return_code == 1);
269 pruned = (return_code == 2);
270 }
271 }
272
273 // track cost-based abort criterion
274 const int cost_end = state_right.T->get_position();
275 double cost_partial = (cost_end - cost_start) / (cost_snapshot*1.0);
276 recent_cost_snapshot = (cost_partial + recent_cost_snapshot * 3) / 4;
277 prune_cost_snapshot += pruned?(cost_end - cost_start):0;
278
279 // if we found automorphism, add to orbit and call hook
280 if (found_auto) {
281 dej_assert(ws_automorphism.nsupp() > 0);
282 dej_assert(ws_automorphism.p()[ind_v] == base_vertex ||
283 ws_automorphism.p()[base_vertex] == ind_v);
284 orbs.add_automorphism_to_orbit(ws_automorphism);
285 if(hook) (*hook)(g->v_size, ws_automorphism.p(), ws_automorphism.nsupp(),
286 ws_automorphism.supp());
287 }
288 ws_automorphism.reset();
289
290 // move state back up where we started in this iteration
291 while (prev_base_pos < state_right.s_base_pos) {
292 state_right.move_to_parent();
293 }
294 state_right.T->set_position(trace_pos_reset);
295
296 // if no automorphism could be determined we would have to backtrack -- so stop!
297
298 if ((!found_auto && !pruned) ||
299 ((4*prune_cost_snapshot > cost_snapshot) && (prev_base_pos > 0)) ||
300 (pruned && !prune)) {
301 fail = true;
302 if(failed_first_level == -1)
303 failed_first_level = state_right.s_base_pos;
304 break;
305 }
306 // if orbit size equals color size now, we are done on this DFS level
307 if (orbs.orbit_size(base_vertex) == col_sz) break;
308 }
309
310 // if we did not fail, accumulate size of current level to group size
311 if (!fail) {
312 computed_orbits.emplace_back((*state_right.compare_base_vertex)[state_right.s_base_pos],
313 orbs.orbit_size(base_vertex));
314 s_grp_sz.multiply(orbs.orbit_size(base_vertex));
315 }
316 }
317
318 // set reason for termination
319 s_termination = fail? r_fail : r_cost;
320
321 // if DFS failed on current level, we did not finish the current level -- has to be accounted for
322 return fail?failed_first_level + (fail):state_right.s_base_pos;
323 }
324
325 int do_simple_dfs(dejavu_hook* hook, sgraph *g, ir::controller& state_right,
326 std::vector<std::pair<int, int>>& computed_orbits, bool prune = true) {
327 if(h_recent_cost_snapshot_limit < 0) return state_right.s_base_pos;
328 s_grp_sz.mantissa = 1.0;
329 s_grp_sz.exponent = 0;
330
331 // orbit algorithm structure
333
334 // automorphism workspace
335 ws_automorphism.reset();
336
337 // we want to terminate if things become to costly, we save the current trace position to track cost
338 cost_snapshot = state_right.T->get_position();
339
340 // tell the controller we are performing DFS now
341 state_right.mode_compare_base();
342
343 int failed_first_level = -1;
344
345 // abort criteria
346 double recent_cost_snapshot = 0;
347 bool fail = false;
348 int trace_pos_reset = 0;
349
350 // loop that serves to optimize Tinhofer graphs
351 while ((recent_cost_snapshot < h_recent_cost_snapshot_limit || state_right.s_base_pos <= 1) &&
352 state_right.s_base_pos > 0 && !fail) {
353 // backtrack one level
354 state_right.move_to_parent();
355
356 if((state_right.s_base_pos & 0x00000FFF) == 0x00000FFD)
357 ws_printer.progress_current_method("dfs", "base_pos",
358 static_cast<double>(state_right.compare_base->size())
359 -state_right.s_base_pos, "cost_snapshot", recent_cost_snapshot);
360 // remember which color we are individualizing
361 const int col = (*state_right.compare_base)[state_right.s_base_pos].color;
362 const int col_sz = state_right.c->ptn[col] + 1;
363 const int base_vertex = (*state_right.compare_base_vertex)[state_right.s_base_pos]; // base vertex
364 dej_assert(col_sz >= 2);
365
366 int prune_cost_snapshot = 0; /*< if we prune, keep track of how costly it is */
367
368 // iterate over current color class
369 for (int i = 0; i < col_sz; ++i) {
370 int ind_v = state_right.leaf_color.lab[col + i];
371 dej_assert(state_right.c->vertex_to_col[base_vertex] == state_right.c->vertex_to_col[ind_v]);
372
373 // only consider every orbit once
374 if(orbs.are_in_same_orbit(ind_v, base_vertex)) continue;
375 if(!orbs.represents_orbit(ind_v)) continue;
376
377 // track cost of this refinement for whatever is to come
378 const int cost_start = state_right.T->get_position();
379
380 // perform individualization-refinement in state_right
381 const int prev_base_pos = state_right.s_base_pos;
382 trace_pos_reset = state_right.T->get_position();
383 state_right.T->reset_trace_equal();
384 state_right.use_trace_early_out(true);
385 state_right.move_to_child(g, ind_v);
386
387 bool pruned = !state_right.T->trace_equal();
388 bool found_auto = false;
389
390 dej_assert(state_right.c->vertex_to_col[ind_v] ==
391 state_right.leaf_color.vertex_to_col[base_vertex]);
392
393 if(!pruned) {
394 // write singleton diff into automorphism...
395 const int wr_pos_st = state_right.base[state_right.base.size() - 1].singleton_pt;
396 const int wr_pos_end = (int) state_right.singletons.size();
397
398 ws_automorphism.reset();
399 // ... and then check whether this implies a (sparse) automorphism
400 ws_automorphism.write_singleton(state_right.compare_singletons,
401 &state_right.singletons, wr_pos_st,
402 wr_pos_end);
403
404 found_auto = state_right.certify(g, ws_automorphism);
405
406 dej_assert(ws_automorphism.p()[base_vertex] == ind_v);
407 // if no luck with sparse automorphism, try more proper walk to leaf node
408 }
409
410 // track cost-based abort criterion
411 const int cost_end = state_right.T->get_position();
412 double cost_partial = (cost_end - cost_start) / (cost_snapshot*1.0);
413 recent_cost_snapshot = (cost_partial + recent_cost_snapshot * 3) / 4;
414 prune_cost_snapshot += pruned?(cost_end - cost_start):0;
415
416 // if we found automorphism, add to orbit and call hook
417 if (found_auto) {
418 dej_assert(ws_automorphism.nsupp() > 0);
419 dej_assert(ws_automorphism.p()[ind_v] == base_vertex ||
420 ws_automorphism.p()[base_vertex] == ind_v);
421 orbs.add_automorphism_to_orbit(ws_automorphism);
422 if(hook) (*hook)(g->v_size, ws_automorphism.p(), ws_automorphism.nsupp(),
423 ws_automorphism.supp());
424 }
425 ws_automorphism.reset();
426
427 // move state back up where we started in this iteration
428 while (prev_base_pos < state_right.s_base_pos) {
429 state_right.move_to_parent();
430 }
431 state_right.T->set_position(trace_pos_reset);
432
433 // if no automorphism could be determined we would have to backtrack -- so stop!
434
435 if ((!found_auto && !pruned) ||
436 ((4*prune_cost_snapshot > cost_snapshot) && (prev_base_pos > 0)) ||
437 (pruned && !prune)) {
438 fail = true;
439 if(failed_first_level == -1)
440 failed_first_level = state_right.s_base_pos;
441 break;
442 }
443 // if orbit size equals color size now, we are done on this DFS level
444 if (orbs.orbit_size(base_vertex) == col_sz) break;
445 }
446
447 // if we did not fail, accumulate size of current level to group size
448 if (!fail) {
449 computed_orbits.emplace_back((*state_right.compare_base_vertex)[state_right.s_base_pos],
450 orbs.orbit_size(base_vertex));
451 s_grp_sz.multiply(orbs.orbit_size(base_vertex));
452 }
453 }
454
455 // set reason for termination
456 s_termination = fail? r_fail : r_cost;
457
458 // if DFS failed on current level, we did not finish the current level -- has to be accounted for
459 return fail?failed_first_level + (fail):state_right.s_base_pos;
460 }
461 };
462 }
463}
464
465#endif //DEJAVU_DFS_H
Stores big numbers.
Definition: utility.h:138
long double mantissa
Definition: utility.h:140
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 reset()
Definition: ds.h:634
void set(int pos)
Definition: ds.h:616
Fixed-size integer array, 0-initialized.
Definition: ds.h:326
Workspace for sparse automorphisms.
Definition: groups.h:68
void cycle_completion(markset &scratch_set)
Definition: groups.h:439
dej_nodiscard int nsupp() const
Definition: groups.h:497
dej_nodiscard int * p() const
Definition: groups.h:483
dej_nodiscard int * supp() const
Definition: groups.h:490
void write_singleton(const std::vector< int > *singletons1, const std::vector< int > *singletons2, const int pos_start, const int pos_end)
Definition: groups.h:420
Orbit partition.
Definition: groups.h:507
bool are_in_same_orbit(const int v1, const int v2)
Definition: groups.h:586
int orbit_size(const int v)
Definition: groups.h:538
void initialize(int domain_size)
Definition: groups.h:638
dej_nodiscard bool represents_orbit(const int v) const
Definition: groups.h:550
int find_orbit(const int v)
Definition: groups.h:519
void add_automorphism_to_orbit(const int *p, const int nsupp, const int *supp)
Definition: groups.h:613
dej_nodiscard int get_position() const
Definition: trace.h:316
dej_nodiscard unsigned long get_hash() const
Definition: trace.h:257
void reset_trace_unequal()
Definition: trace.h:285
void set_position(int new_position)
Definition: trace.h:308
dej_nodiscard bool trace_equal() const
Definition: trace.h:272
void reset_trace_equal()
Definition: trace.h:279
Depth-first search without backtracking.
Definition: dfs.h:60
dfs_ir(timed_print &printer, groups::automorphism_workspace &automorphism)
Definition: dfs.h:75
double h_recent_cost_snapshot_limit
Definition: dfs.h:70
int do_paired_dfs(dejavu_hook *hook, sgraph *g, ir::controller &state_left, ir::controller &state_right, std::vector< std::pair< int, int > > &computed_orbits, bool prune=true)
Definition: dfs.h:146
termination_reason s_termination
Definition: dfs.h:67
int do_simple_dfs(dejavu_hook *hook, sgraph *g, ir::controller &state_right, std::vector< std::pair< int, int > > &computed_orbits, bool prune=true)
Definition: dfs.h:325
int paired_recurse_to_equal_leaf(sgraph *g, ir::controller &state_left, ir::controller &state_right, bool recurse=false)
Definition: dfs.h:78
Internal graph data structure.
Definition: graph.h:19
int v_size
Definition: graph.h:48
Prints information to the console.
Definition: utility.h:237
void progress_current_method(const std::string &print) const
Definition: utility.h:301
Definition: bfs.h:10
Controls movement in IR tree.
Definition: ir.h:130
std::vector< int > * compare_base_vertex
Definition: ir.h:141
std::vector< base_info > * compare_base
Definition: ir.h:142
std::vector< base_info > base
Definition: ir.h:139
void link_compare(controller *state)
Definition: ir.h:703
bool update_diff_vertices_last_individualization(const controller &other_state)
Definition: ir.h:611
coloring * c
Definition: ir.h:132
std::vector< int > singletons
Definition: ir.h:135
void mode_compare_base()
Definition: ir.h:442
void move_to_child(sgraph *g, int v)
Definition: ir.h:989
dej_nodiscard int get_diff_diverge() const
Definition: ir.h:597
void singleton_automorphism(controller &state, groups::automorphism_workspace &automorphism)
Definition: ir.h:584
void use_trace_early_out(bool trace_early_out)
Definition: ir.h:831
void move_to_parent()
Definition: ir.h:1057
std::vector< int > * compare_singletons
Definition: ir.h:136
std::pair< int, int > diff_pair(const controller &state)
Definition: ir.h:539
void reset_diff()
Definition: ir.h:566
bool certify(sgraph *g, groups::automorphism_workspace &automorphism)
Definition: ir.h:1123
bool there_is_difference_to_base_including_singles(int domain_size)
Definition: ir.h:513
coloring leaf_color
Definition: ir.h:144
#define dej_assert(expr)
Definition: utility.h:40
std::function< void(int, const int *, int, const int *)> dejavu_hook
Definition: utility.h:95