dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
dejavu.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_DEJAVU_H
6#define DEJAVU_DEJAVU_H
7
8#define DEJAVU_VERSION_MAJOR 2
9#define DEJAVU_VERSION_MINOR 0
10#define DEJAVU_VERSION_IS_PREVIEW true
11
12#include <utility>
13#include <string>
14
15#include "dfs.h"
16#include "bfs.h"
17#include "rand.h"
18#include "preprocess.h"
19#include "inprocess.h"
20#include "components.h"
21
22#if ((defined(_MSVC_LANG) && _MSVC_LANG < 201402L) || __cplusplus < 201402L)
23# error "dejavu requires to be compiled with C++ 2014 or newer"
24#endif
25
26// structures for testing
27#if defined(DEJDEBUG) && !defined(NDEBUG)
30#endif
31
32namespace dejavu {
33 #if defined(DEJDEBUG) && !defined(NDEBUG)
34 static inline void test_hook(int, const int *p, int nsupp, const int *supp) {
35 assert(test_r.certify_automorphism_sparse(&dej_test_graph, p, nsupp, supp));
36 }
37 #endif
38
42 namespace hooks {
43
45 public:
46 virtual dejavu_hook* get_hook() = 0;
47 virtual ~hook_interface() = default;
48 };
49
55 class multi_hook : public hook_interface {
56 private:
57 std::vector<dejavu_hook*> hooks;
58 dejavu_hook my_hook;
59 void hook_func(int n, const int *p, int nsupp, const int *supp) {
60 for(dejavu_hook* hook : hooks) {
61 (*hook)(n, p, nsupp, supp);
62 }
63 }
64 public:
65 void add_hook(dejavu_hook* hook) {
66 hooks.push_back(hook);
67 }
68
69 void clear() {
70 hooks.clear();
71 }
72
73 dej_nodiscard size_t size() const {
74 return hooks.size();
75 }
76
77 dejavu_hook* get_hook() override {
78 #ifndef dej_nolambda
79 my_hook = [this](auto && PH1, auto && PH2, auto && PH3, auto && PH4)
80 { return this->hook_func(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2),
81 std::forward<decltype(PH3)>(PH3), std::forward<decltype(PH4)>(PH4));
82 };
83 #else
84 my_hook = std::bind(&multi_hook::hook_func, this, std::placeholders::_1, std::placeholders::_2,
85 std::placeholders::_3, std::placeholders::_4);
86 #endif
87 return &my_hook;
88 }
89 };
90
97 private:
98 dejavu_hook my_hook;
99 std::ostream& my_ostream;
100 dejavu::ds::markset test_set;
101
102 void hook_func(int n, const int *p, int nsupp, const int *supp) {
103 test_set.initialize(n);
104 test_set.reset();
105 for(int i = 0; i < nsupp; ++i) {
106 const int v_from = supp[i];
107 if(test_set.get(v_from)) continue;
108 int v_next = p[v_from];
109 if(v_from == v_next) continue;
110 test_set.set(v_from);
111 my_ostream << "(" << v_from;
112 while(!test_set.get(v_next)) {
113 test_set.set(v_next);
114 my_ostream << " " << v_next;
115 v_next = p[v_next];
116 }
117 my_ostream << ")";
118 }
119 my_ostream << std::endl;
120 }
121 public:
122 explicit ostream_hook(std::ostream& ostream) : my_ostream(ostream) {}
123
124 dejavu_hook* get_hook() override {
125 #ifndef dej_nolambda
126 my_hook = [this](auto && PH1, auto && PH2, auto && PH3, auto && PH4)
127 { return this->hook_func(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2),
128 std::forward<decltype(PH3)>(PH3), std::forward<decltype(PH4)>(PH4));
129 };
130 #else
131 my_hook = std::bind(&ostream_hook::hook_func, this, std::placeholders::_1, std::placeholders::_2,
132 std::placeholders::_3, std::placeholders::_4);
133 #endif
134 return &my_hook;
135 }
136 };
137
149 private:
150 dejavu_hook my_hook;
151 dejavu_hook* my_call_hook = nullptr;
152 markset scratch_set;
153
154 sgraph my_g;
155
156 void hook_func(int n, const int *p, int nsupp, const int *supp) {
157 const bool certify = ir::certification::certify_automorphism_sparse(scratch_set, &my_g, p, nsupp, supp);
158 if(!certify) return;
159 (*my_call_hook)(n, p, nsupp, supp);
160 }
161 public:
163 initialize(*g.get_sgraph(), call_hook);
164 }
165
167 initialize(g, call_hook);
168 }
169
171
172 void initialize(sgraph& g, dejavu_hook* call_hook) {
173 my_g.copy_graph(&g);
174 my_call_hook = call_hook;
175 scratch_set.initialize(g.v_size);
176 }
177
178 dejavu_hook* get_hook() override {
179 #ifndef dej_nolambda
180 my_hook = [this](auto && PH1, auto && PH2, auto && PH3, auto && PH4)
181 { return this->hook_func(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2),
182 std::forward<decltype(PH3)>(PH3), std::forward<decltype(PH4)>(PH4));
183 };
184 #else
185 my_hook = std::bind(&strong_certification_hook::hook_func, this, std::placeholders::_1,
186 std::placeholders::_2, std::placeholders::_3, std::placeholders::_4);
187 #endif
188 return &my_hook;
189 }
190 };
191
198 private:
199 dejavu_hook my_hook;
200 groups::random_schreier& my_schreier;
201 void hook_func(int n, const int *p, int nsupp, const int *supp) {
202 my_schreier.sift(n, p, nsupp, supp);
203 }
204 public:
205 explicit schreier_hook(groups::random_schreier& schreier) : my_schreier(schreier) {}
206
207 dejavu_hook* get_hook() override {
208 #ifndef dej_nolambda
209 my_hook = [this](auto && PH1, auto && PH2, auto && PH3, auto && PH4)
210 { return this->hook_func(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2),
211 std::forward<decltype(PH3)>(PH3), std::forward<decltype(PH4)>(PH4));
212 };
213 #else
214 my_hook = std::bind(&schreier_hook::hook_func, this, std::placeholders::_1, std::placeholders::_2,
215 std::placeholders::_3, std::placeholders::_4);
216 #endif
217 return &my_hook;
218 }
219 };
220
226 class orbit_hook : public hook_interface {
227 private:
228 dejavu_hook my_hook;
229 groups::orbit& my_orbit;
230 void hook_func(int n, const int *p, int nsupp, const int *supp) {
231 my_orbit.add_automorphism_to_orbit(p, nsupp, supp);
232 }
233 public:
234 explicit orbit_hook(groups::orbit& save_orbit) : my_orbit(save_orbit) {}
235
236 dejavu_hook* get_hook() override {
237 #ifndef dej_nolambda
238 my_hook = [this](auto && PH1, auto && PH2, auto && PH3, auto && PH4)
239 { return this->hook_func(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2),
240 std::forward<decltype(PH3)>(PH3), std::forward<decltype(PH4)>(PH4));
241 };
242 #else
243 my_hook = std::bind(&orbit_hook::hook_func, this, std::placeholders::_1, std::placeholders::_2,
244 std::placeholders::_3, std::placeholders::_4);
245 #endif
246 return &my_hook;
247 }
248 };
249 }
250
257 class solver {
258 private:
259 int h_error_bound = 10;
262 bool h_random_use_true_random = false;
263 int h_random_seed = 0;
264 bool h_silent = false;
265 int h_bfs_memory_limit = 0x20000000;
266 bool h_decompose = true;
267 int h_base_max_diff = 5;
269 bool h_prefer_dfs = false;
270 bool h_destructive = true;
271 bool h_strong_certification = false;
273 //int h_limit_fail = 0; /**< limit for the amount of backtracking allowed */
274
275 // std::function<selector_hook>* h_user_selector = nullptr; /**< user-provided cell selector */
276 // std::function<selector_hook>* h_user_invariant = nullptr; /**< user-provided invariant to be applied during
277 // inprocessing */
278
279 bool s_deterministic_termination = true;
280 big_number s_grp_sz;
281 public:
288 void set_error_bound(int error_bound = 10) {
289 h_error_bound = error_bound;
290 }
291
298 int get_error_bound() const {
299 return h_error_bound;
300 }
301
308 void set_true_random(bool use_true_random = true) {
309 h_random_use_true_random = use_true_random;
310 }
311
318 void set_prefer_dfs(bool prefer_dfs = true) {
319 h_prefer_dfs = prefer_dfs;
320 }
321
328 void set_pseudo_random(bool use_pseudo_random = true) {
329 h_random_use_true_random = !use_pseudo_random;
330 }
331
336 void set_seed(int seed = 0) {
337 h_random_seed = seed;
338 }
339
345 void set_strong_certification(bool use_strong_certification = true) {
346 h_strong_certification = use_strong_certification;
347 }
348
354 void set_disallow_alteration(bool may_alter_graph = false) {
355 h_destructive = may_alter_graph;
356 }
357
363 void set_decompose(bool use_decompose = true) {
364 h_decompose = use_decompose;
365 }
366
372 std::random_device rd;
373 h_random_seed = static_cast<int>(rd());
374 }
375
381 void set_print(bool print=true) {
382 h_silent = !print;
383 }
384
390 return s_grp_sz;
391 }
392
398 return s_deterministic_termination;
399 }
400
410 void automorphisms(static_graph* g, dejavu_hook* hook = nullptr) {
411 automorphisms(g->get_sgraph(), g->get_coloring(), hook);
412 }
413
418 dejavu_hook hook_to_hook_ptr = std::move(hook);
419 automorphisms(g->get_sgraph(), g->get_coloring(), &hook_to_hook_ptr);
420 }
421
426 automorphisms(g->get_sgraph(), g->get_coloring(), hook.get_hook());
427 }
428
432 void automorphisms(sgraph* g, int* colmap = nullptr, dejavu_hook* hook = nullptr) {
433 enum termination_strategy { t_prep, t_inproc, t_dfs, t_bfs, t_det_schreier, t_rand_schreier };
434 termination_strategy s_term = t_prep;
435 s_grp_sz.set(1.0, 0);
436
437 // we want to print with a timer, so let's initialize a timed printer
438 timed_print m_printer;
439 m_printer.h_silent = h_silent;
440
441 // use strong certification?
442 hooks::strong_certification_hook certification_hook;
443 if(h_strong_certification) {
444 certification_hook.initialize(*g, hook);
445 hook = certification_hook.get_hook();
446 h_destructive = false;
447 }
448
449 // no vertex coloring provided? let's substitute a trivial vertex coloring
450 worklist colmap_substitute;
451 if (colmap == nullptr) {
452 colmap_substitute.resize(g->v_size);
453 colmap = colmap_substitute.get_array();
454 for (int i = 0; i < g->v_size; ++i) colmap[i] = 0;
455 } else if(!h_destructive) {
456 int* orig_colmap = colmap;
457 colmap_substitute.resize(g->v_size);
458 colmap = colmap_substitute.get_array();
459 for (int i = 0; i < g->v_size; ++i) colmap[i] = orig_colmap[i];
460 }
461
462 // not supposed to change the graph? swap it out...
463 sgraph graph_substitute;
464 if(!h_destructive) {
465 graph_substitute.copy_graph(g);
466 g = &graph_substitute;
467 }
468
469 // first, we try to preprocess the graph
470 preprocessor m_prep(&m_printer); /*< initializes the preprocessor */
471
472 // preprocess the graph
473 m_printer.print("preprocessing");
474 m_prep.reduce(g, colmap, hook); /*< reduces the graph */
475 s_grp_sz.multiply(m_prep.grp_sz); /*< add group size detected during preprocessing */
476
477 // early-out if preprocessor finished solving the graph
478 if(g->v_size <= 1) return;
479
480 // if the preprocessor changed the vertex set of the graph, we need to use reverse translation
482 hook = &dhook; /*< change hook to sassy hook */
483
484 // attempt to split into multiple quotient components than can be handled individually
485 ir::graph_decomposer m_decompose;
486 int s_num_components = 1;
487 if(h_decompose) {
488 // place to store the result of component computation
489 worklist vertex_to_component(g->v_size);
490 // compute the quotient components
491 s_num_components = ir::quotient_components(g, colmap, &vertex_to_component);
492 // make the decomposition according to the quotient components
493 m_decompose.decompose(g, colmap, vertex_to_component, s_num_components);
494 }
495
496 // run the solver for each of the components separately (tends to be just one component, though)
497 for(int i = 0; i < s_num_components; ++i) {
498 // if we have multiple components, we need to lift the symmetry back to the original graph
499 // we do so using the lifting routine of the preprocessor
500 if(s_num_components > 1) {
501 g = m_decompose.get_component(i); // graph of current component
502 colmap = m_decompose.get_colmap(i); // vertex coloring of current component
503 m_prep.inject_decomposer(&m_decompose, i); // set translation to current component
504 }
505
506 // print that we are solving now...
507 m_printer.h_silent = h_silent || (g->v_size <= 128 && i != 0);
508 if(!m_printer.h_silent)
509 PRINT("\r\nsolving_component " << i+1 << "/" << s_num_components << " (n=" << g->v_size << ")")
510 m_printer.print_header();
511 m_printer.timer_split();
512
513 // flag to denote which color refinement version is used
514 g->dense = !(g->e_size < g->v_size || g->e_size / g->v_size < g->v_size / (g->e_size / g->v_size));
515
516 // settings of heuristics
517 int h_budget = 1; /*< budget of current restart iteration */
518 int h_budget_inc_fact = 5; /*< factor used when increasing the budget */
519
520 // statistics used to steer heuristics
521 int s_restarts = -1; /*< number of restarts performed */
522 int s_inproc_success = 0; /*< how many times inprocessing succeeded */
523 int s_cost = 0; /*< cost induced so far by current restart iteration */
524 bool s_long_base = false; /*< flag for bases that are considered very long */
525 bool s_short_base = false; /*< flag for bases that are considered very short */
526 bool s_prunable = false; /*< does this graph seem to exhibit exploitable structure? */
527 double s_random_budget_bias = 1.0; /*< a bias for random search, whether we've gathered that the
528 * technique does not seem to work on this graph */
529
530 //bool s_few_cells = false;
531 bool h_used_shallow_inprocess = false;
532 bool h_used_shallow_inprocess_quadratic = false;
533 bool s_inprocessed = false; /*< flag which says that we've inprocessed the graph since last restart */
534 int s_consecutive_discard = 0; /*< count how many bases have been discarded in a row -- prevents edge
535 * case where all searchable bases became much larger due to BFS or other
536 * changes */
537 bool s_last_bfs_pruned = false;/*< keep track of whether last BFS calculation pruned some nodes */
538 bool s_any_bfs_pruned = false;
539 big_number s_last_tree_sz;
540
541 // some data we want to keep track of
542 std::vector<int> base_vertex; /*< current base_vertex of vertices */
543 std::vector<int> base_sizes; /*< current size of colors on base_vertex */
544
545 // local modules and workspace, to be used by other modules
546 ir::cell_selector_factory m_selectors; /*< cell selector creation */
547 ir::refinement m_refinement; /*< workspace for color refinement and other utilities */
548 groups::domain_compressor m_compress;/*< can compress a workspace of vertices to a subset of vertices */
549 groups::automorphism_workspace automorphism(g->v_size); /*< workspace to keep an automorphism */
550 groups::schreier_workspace schreierw(g->v_size); /*< workspace for Schreier-Sims */
551
552 // shared, global modules
553 ir::shared_tree sh_tree(g->v_size); /*< BFS levels, shared leaves, ... */
554 groups::compressed_schreier sh_schreier; /*< Schreier structure to sift automorphisms */
555 sh_schreier.set_error_bound(h_error_bound);
556
557 // randomness of the solver
558 random_source rng(h_random_use_true_random, h_random_seed);
559
560 // initialize modules for high-level search strategies
561 search_strategy::dfs_ir m_dfs(m_printer, automorphism); /*< depth-first search */
562 search_strategy::bfs_ir m_bfs(m_printer, automorphism); /*< breadth-first search */
563 search_strategy::random_ir m_rand(m_printer, schreierw, automorphism, rng); /*< randomized search */
564 search_strategy::inprocessor m_inprocess; /*< inprocessing */
565
566 // initialize a coloring using colors of preprocessed graph
567 coloring local_coloring;
568 coloring local_coloring_left;
569 g->initialize_coloring(&local_coloring, colmap);
570 const bool s_regular = local_coloring.cells == 1; /*< is this graph regular? */
571
572 // set up a local state for IR computations
573 ir::controller local_state(&m_refinement, &local_coloring); /*< controls movement in IR tree*/
574 ir::controller local_state_left(&m_refinement, &local_coloring_left);
575
576 // set deviation counter relative to graph size
577 local_state.set_increase_deviation(std::min(static_cast<int>(floor(3 * sqrt(g->v_size))), 128));
578 local_state.reserve(); // reserve some space
579
580 // save root state for random and BFS search, as well as restarts
581 ir::limited_save root_save;
582 local_state.save_reduced_state(root_save); /*< root of the IR tree */
583 int s_last_base_size = g->v_size + 1; /*< v_size + 1 is larger than any actual base_vertex*/
584 int dfs_level = -1; /*< level up to which depth-first search was performed */
585
586 // now that we are set up, let's start solving the graph
587 // loop for restarts
588 while (true) {
589 // "Dry land is not a myth, I've seen it!"
590 const bool s_hard = h_budget > 256; /* graph is "hard" (was 10000)*/
591 const bool s_easy = s_restarts == -1; /* graph is "easy" */
592
593 ++s_restarts; /*< increase the restart counter */
594 if (s_restarts > 0) {
595 // now, we manage the restart....
596 local_state.load_reduced_state(root_save); /*< start over from root */
597 m_printer.print_split();
598 const int s_inc_fac = (s_restarts >= 3)? h_budget_inc_fact : 2;/*< factor of budget increase */
599 if (s_inproc_success >= 3) {
600 s_random_budget_bias = 0.1; // do less random search (bfs seems to work well, since we are
601 // successfully inprocessing)
602 h_budget_inc_fact = 2;
603 }
604 if (s_inproc_success >= 6) s_random_budget_bias = 0.01; // do even less random search
605 if (s_inprocessed) h_budget = 1; /*< if we inprocessed, we hope that the graph is easy again */
606 h_budget *= s_inc_fac; /*< increase the budget */
607 s_cost = 0; /*< reset the cost */
608 }
609
610 // keep vertices which are save to individualize for in-processing
611 m_inprocess.inproc_can_individualize.clear();
612 m_inprocess.inproc_maybe_individualize.clear();
613
614 // find a selector, moves local_state to a leaf of the IR tree
615 auto style = static_cast<ir::cell_selector_factory::selector_style>(s_restarts % 4);
616 m_selectors.make_cell_selector(g, &local_state, &local_state_left, style, s_restarts, h_budget);
617 auto selector = m_selectors.get_selector_hook();
618 m_printer.timer_print("sel", local_state.s_base_pos, local_state.T->get_position());
619
620 // statistics of this base
621 const int base_size = local_state.s_base_pos; /*< base length */
622 const big_number s_tree_estimate = m_selectors.get_ir_size_estimate(); /*< size estimate of tree */
623 // determine whether base_vertex is "large", or "short"
624 s_long_base = base_size > sqrt(g->v_size); /*< a "long" base_vertex */
625 s_short_base = base_size <= 2; /*< a "short" base_vertex */
626 //s_few_cells = root_save.get_coloring()->cells <= 2; /*< "few" cells in initial */
627
628 // heuristics to determine whether we want to skip this base, i.e., is this obviously worse than
629 // what we've seen before, and is there no reason to look at it?
630 const bool s_too_long = base_size > h_base_max_diff * s_last_base_size && s_inproc_success <= 1;
631 const bool s_too_big = (s_inproc_success <= (s_regular + !s_prunable)) &&
632 (s_last_tree_sz < s_tree_estimate) &&
633 (s_restarts >= 2);
634
635 // immediately discard this base if deemed too unfavourable by the heuristics above, unless we are
636 // discarding too often
637 if ((s_too_big || s_too_long) && s_consecutive_discard < 3) {
638 m_printer.timer_print("skip", local_state.s_base_pos, s_last_base_size);
639 ++s_consecutive_discard;
640 continue;
641 }
642 s_consecutive_discard = 0; /*< reset counter since we are not discarding this one */
643 s_last_base_size = base_size; /*< also reset `s_last_base_size` to current `base_size` */
644 s_last_tree_sz = m_selectors.get_ir_size_estimate(); /*< ...same with the IR tree size estimate */
645 const bool s_last_base_eq = (base_vertex == local_state.base_vertex); /*< is this just the same
646 * base again? */
647
648 // make snapshot of trace and leaf, used by following search strategies
649 local_state.compare_to_this();
650 base_vertex = local_state.base_vertex; // we want to keep this for later
651 base_sizes.clear();
652 base_sizes.reserve(local_state.base.size());
653 for(auto& bi : local_state.base) base_sizes.push_back(bi.color_sz); // TODO clean up
654
655 const int s_trace_full_cost = local_state.T->get_position(); /*< total trace cost of this base */
656
657
658 // we first perform a depth-first search, starting from the computed leaf in local_state
659 m_dfs.h_recent_cost_snapshot_limit = s_long_base ? 0.33 : 0.25; // set up DFS heuristic
660 m_dfs.h_recent_cost_snapshot_limit = h_prefer_dfs ? 1.0 : m_dfs.h_recent_cost_snapshot_limit;
661 dfs_level = s_last_base_eq ? dfs_level : m_dfs.do_paired_dfs(hook, g, local_state_left, local_state,
662 m_inprocess.inproc_maybe_individualize,
663 base_size > 1 || s_restarts > 0);
664
665 m_printer.timer_print("dfs", std::to_string(base_size) + "-" + std::to_string(dfs_level),
666 "~" + std::to_string((int) m_dfs.s_grp_sz.mantissa) + "*10^" +
667 std::to_string(m_dfs.s_grp_sz.exponent));
668 s_prunable = s_prunable || (dfs_level < base_size - 5);
669 if (dfs_level == 0) {
670 // dfs finished the graph -- we are done!
671 s_term = t_dfs;
672 break;
673 }
674 const int s_dfs_potential_ind = m_inprocess.check_individualizations(root_save);
675
676 // next, we go into the random path + BFS algorithm, so we set up a Schreier structure and IR tree
677 // for the given base_vertex
678
679 // first, the Schreier structure
680 const bool can_keep_previous = (s_restarts >= 3) && !s_inprocessed; /*< do we want to try to keep
681 * previous automorphisms? */
682 // maybe we want to compress the Schreier structure
683 sh_schreier.h_min_compression_ratio = g->v_size > 1000000 ? 0.7 : 0.4; /*<if graph is large,
684 * compress aggressively */
685 m_compress.determine_compression_map(*root_save.get_coloring(), base_vertex, dfs_level);
686
687 // set up Schreier structure
688 const bool reset_prob = sh_schreier.reset(&m_compress, g->v_size, schreierw, base_vertex,
689 base_sizes, dfs_level, can_keep_previous,
690 m_inprocess.inproc_fixed_points);
691 if (reset_prob) sh_schreier.reset_probabilistic_criterion(); /*< need to reset probabilistic abort
692 * criterion after inprocessing */
693
694 // reset metrics of random search
695 m_rand.reset_statistics();
696
697 // here, we set up the shared IR tree, which contains computed BFS levels, stored leaves, as well as
698 // further gathered data for heuristics
699 sh_tree.reset(base_vertex, &root_save, can_keep_previous);
700 if (s_inprocessed) sh_tree.clear_leaves();
701
702 // we add the leaf of the base_vertex to the IR tree
703 search_strategy::random_ir::specific_walk(g, sh_tree, local_state, base_vertex);
704
705 s_last_bfs_pruned = false;
706 s_any_bfs_pruned = false;
707 int h_rand_fail_lim_total = 0;
708 int h_rand_fail_lim_now = 0;
709 double s_path_fail1_avg = 0;
710
711 // in the following, we will always decide between 3 different strategies: random paths, BFS, or
712 // inprocessing followed by a restart
713 enum decision {random_ir, bfs_ir, restart}; /*< this enum tracks the decision */
714 decision next_routine = random_ir; /*< here, we store the decision */
715 decision last_routine = random_ir; /*< here, we store the last decision */
716
717 // we perform these strategies in a loop, with the following abort criteria
718 bool do_a_restart = false; /*< we want to do a full restart */
719 bool finished_symmetries = false; /*< we found all the symmetries */
720
721 h_rand_fail_lim_now = 4; /*< how many failures are allowed during random leaf search */
722 last_routine = restart;
723
724 while (!do_a_restart && !finished_symmetries) {
725 // What do we do next? Random search, BFS, or a restart?
726 // here are our decision heuristics (AKA dark magic)
727
728 // first, we update our estimations / statistics
729 const int s_bfs_next_level_nodes =
731
732 const bool s_have_rand_estimate = (m_rand.s_paths >= 4); /*< for some estimations, we need a
733 * few random paths */
734 double s_trace_cost1_avg = s_trace_full_cost;
735
736 int s_random_path_trace_cost = s_trace_full_cost - sh_tree.get_current_level_tracepos();
737 if (s_have_rand_estimate) {
738 s_path_fail1_avg = (double) m_rand.s_paths_fail1 / (double) m_rand.s_paths;
739 s_trace_cost1_avg = (double) m_rand.s_trace_cost1 / (double) m_rand.s_paths;
740 }
741
742 // using this data, we now make a decision
743 next_routine = random_ir; /*< don't have an estimate? let's poke a bit with random! */
744 double score_rand, score_bfs;
745
746 if (s_have_rand_estimate) {
747 // if we have some data, we attempt to model how effective and costly random search
748 // and BFS is, to then make an informed decision of what to do next
749 const double reset_cost_rand = g->v_size;
750 const double reset_cost_bfs = std::min(s_trace_cost1_avg, (double) g->v_size);
751 double s_bfs_estimate = (s_trace_cost1_avg + reset_cost_bfs) * (s_bfs_next_level_nodes);
752 double s_rand_estimate = (s_random_path_trace_cost + reset_cost_rand) * h_rand_fail_lim_now;
753
754 // we do so by negatively scoring each method: higher score, worse technique
755 score_rand = s_rand_estimate * (1 - m_rand.s_rolling_success);
756 score_bfs = s_bfs_estimate * (0.1 + 1 - s_path_fail1_avg);
757
758 // we make some adjustments to try to model effect of techniques better
759 // increase BFS score if BFS does not prune nodes on the next level -- we want to be
760 // somewhat more reluctant to perform BFS in this case
761 if (s_path_fail1_avg < 0.01) score_bfs *= 2;
762
763 // we decrease the BFS score if we are beyond the first level, in the hope that this models
764 // the effect of trace deviation maps
765 if (sh_tree.get_finished_up_to() >= 1) score_bfs *= (1 - s_path_fail1_avg);
766
767 // we make a decision...
768 next_routine = (score_rand < score_bfs) ? random_ir : bfs_ir;
769
770 // if we do random_ir next, increase its budget
771 h_rand_fail_lim_now = next_routine==random_ir? 2*h_rand_fail_lim_now : h_rand_fail_lim_now;
772 }
773
774 // we override the above decisions in specific cases...
775 // first, we consider our limits: budget, memory limits, ...
776 if (next_routine == bfs_ir && s_bfs_next_level_nodes * (1 - s_path_fail1_avg) > 2 * h_budget)
777 next_routine = restart; /* best decision would be BFS, but it would exceed the budget a
778 * lot! */
779
780 // let's stick to the memory limits...
781 const long s_bfs_est_mem = (long) round(s_bfs_next_level_nodes * (1 - s_path_fail1_avg) *
782 g->v_size);
783 if (next_routine == bfs_ir && (s_bfs_est_mem > h_bfs_memory_limit)) next_routine = random_ir;
784
785 // let's stick to the budget...
786 if (s_cost > h_budget) next_routine = restart; /*< we exceeded our budget, restart */
787
788 // ...unless...
789 // silly case in which the base is so long, that an unnecessary restart has fairly high
790 // cost attached -- so if BFS can be successful, let's do that first...
791 if (next_routine == restart && 2 * base_size > s_bfs_next_level_nodes
792 && s_trace_cost1_avg < base_size && s_path_fail1_avg > 0.01) next_routine = bfs_ir;
793
794 // ... and if we are "almost done" with random search, we stretch the budget a bit
795 // here are some definitions for "almost done", because I can not come up with a single one
796 if (search_strategy::random_ir::h_almost_done(sh_schreier) && next_routine == restart)
797 next_routine = random_ir;
798 if (m_rand.s_rolling_success > 0.1 && s_cost <= h_budget * 4) next_routine = random_ir;
799 if (m_rand.s_rolling_success > 0.2 && s_cost <= h_budget * 6) next_routine = random_ir;
800 if (s_hard && m_rand.s_succeed >= 1 && s_cost <= m_rand.s_succeed * h_budget * 10 &&
801 next_routine == restart)
802 next_routine = random_ir;
803 if (dfs_level == sh_tree.get_finished_up_to() && s_any_bfs_pruned && s_cost <= h_budget * 20)
804 next_routine = random_ir;
805
806 // immediately inprocess if bfs was successful in pruning the first level -- we somewhat don't
807 // want to do too much bfs, since we have only very limited automorphism pruning capability
808 if (sh_tree.get_finished_up_to() == 1 && dfs_level > 1 && s_last_bfs_pruned)
809 next_routine = restart;
810 if (sh_tree.get_finished_up_to() > 1 && sh_tree.get_current_level_size() < base_sizes[0])
811 next_routine = restart;
812
813 // inprocess if depth-first search stopped because of failure, but we can inprocess a large
814 // number of automorphisms found by depth-first search
816 && s_dfs_potential_ind > 8 && s_dfs_potential_ind > base_size - dfs_level - 2)
817 next_routine = restart;
818
819 // now we've finally made up our mind of what to do next
820
821 // some printing...
822 if(last_routine == random_ir && next_routine != random_ir) {
823 m_printer.timer_print("random", sh_tree.stat_leaves(), m_rand.s_rolling_success);
824 if (sh_schreier.s_densegen() + sh_schreier.s_sparsegen() > 0) {
825 m_printer.timer_print("schreier", "s" + std::to_string(sh_schreier.s_sparsegen()) +
826 "/d" + std::to_string(sh_schreier.s_densegen()), "_");
827 }
828 }
829
830 // let's perform the next routine...
831 switch (next_routine) {
832 case random_ir: { // random leaf search
833 // look close means we do not abort random walks that deviate from trace on the first
834 // level
835 const bool h_look_close = ((m_rand.s_rolling_first_level_success > 0.5) &&
836 !s_short_base) || (s_have_rand_estimate &&
837 sh_tree.get_finished_up_to() == base_size - 1);
838 // we increase the random ir budget -- but we apply a "budget bias", which changes
839 // the proportion of time spent in random search versus bfs (but does not change the
840 // decision making)
841 h_rand_fail_lim_total +=
842 static_cast<int>(std::max(5.0, h_rand_fail_lim_now * s_random_budget_bias));
843 m_rand.use_look_close(h_look_close);
844 m_rand.h_sift_random = !s_easy;
845 m_rand.h_randomize_up_to = dfs_level;
846 if (sh_tree.get_finished_up_to() == 0 || (s_long_base && !s_any_bfs_pruned)) {
847 // random automorphisms, sampled from root of IR tree
848 m_rand.random_walks(g, hook, selector, sh_tree, sh_schreier, local_state,
849 local_state_left, h_rand_fail_lim_total);
850 } else {
851 // random automorphisms, sampled from current bfs level of ir tree
852 m_rand.random_walks_from_tree(g, hook, selector, sh_tree, sh_schreier,
853 local_state, local_state_left,
854 h_rand_fail_lim_total);
855 }
856 finished_symmetries = sh_schreier.any_abort_criterion();
857 s_term = sh_schreier.deterministic_abort_criterion()? t_det_schreier : t_rand_schreier;
858 s_cost += h_rand_fail_lim_now;
859
860 // TODO this code is duplicated, let's think about this again...
861 if(finished_symmetries) {
862 m_printer.timer_print("random", sh_tree.stat_leaves(), m_rand.s_rolling_success);
863 if (sh_schreier.s_densegen() + sh_schreier.s_sparsegen() > 0) {
864 m_printer.timer_print("schreier",
865 "s" + std::to_string(sh_schreier.s_sparsegen()) +
866 "/d" + std::to_string(sh_schreier.s_densegen()), "_");
867 }
868 }
869 }
870 break;
871 case bfs_ir: { // one level of breadth-first search
872 m_bfs.h_use_deviation_pruning = !((s_inproc_success >= 2) && s_path_fail1_avg > 0.1);
873 //m_bfs.h_use_deviation_pruning = false;
874 m_bfs.do_a_level(g, hook, sh_tree, local_state, selector);
875 m_printer.timer_print("bfs",
876 "0-" + std::to_string(sh_tree.get_finished_up_to()) + "(" +
877 std::to_string(s_bfs_next_level_nodes) + ")",
878 std::to_string(sh_tree.get_level_size(sh_tree.get_finished_up_to())));
879
880 // A bit of a mess here! Manage correct group size whenever BFS finishes the graph. Bit
881 // complicated because of the special code for `base_size == 2`, which can perform
882 // automorphism pruning. (The removed automorphisms must be accounted for when
883 // calculating the group size.)
884 if (sh_tree.get_finished_up_to() == base_size) {
885 finished_symmetries = true;
886 s_term = t_bfs;
887 if (base_size == 2) {
888 // case for the special code
889 m_inprocess.s_grp_sz.multiply(
890 (double) sh_tree.h_bfs_top_level_orbit.orbit_size(base_vertex[0]) *
891 sh_tree.h_bfs_automorphism_pw, 0);
892 } else if (base_size == 1) {
893 m_inprocess.s_grp_sz.multiply(
894 (double) sh_tree.h_bfs_top_level_orbit.orbit_size(base_vertex[0]), 0);
895 } else {
896 // base case which just multiplies the remaining elements of the level
897 m_inprocess.s_grp_sz.multiply(
898 (double) sh_tree.get_level_size(sh_tree.get_finished_up_to()), 0);
899 }
900 }
901
902 // if there are less remaining nodes than we expected, we pruned some nodes
903 s_last_bfs_pruned = sh_tree.get_current_level_size() < s_bfs_next_level_nodes;
904 s_any_bfs_pruned = s_any_bfs_pruned || s_last_bfs_pruned;
905 m_rand.reset_statistics();
906 s_cost += sh_tree.get_current_level_size();
907 }
908 break;
909 case restart: // do a restart
910 do_a_restart = true;
911 break;
912 }
913
914 last_routine = next_routine;
915 }
916
917 // Are we done or just restarting?
918 if (finished_symmetries) {
919 sh_schreier.compute_group_size(); // need to compute the group size now
920 break; // we are done
921 }
922
923 m_inprocess.set_splits_hint(m_rand.s_min_split_number);
924 // we are restarting -- so we try to inprocess using the gathered data
925
926 // decide whether we want to use shallow bfs invariants
927 const bool h_use_shallow_inprocess = !h_used_shallow_inprocess && s_inproc_success == 0 &&
928 s_path_fail1_avg > 0.1;
929 const bool h_use_shallow_inprocess_quadratic =
930 !h_used_shallow_inprocess_quadratic && s_inproc_success >= 1 + s_regular &&
931 s_prunable && 2*local_state.c->cells > sqrt(g->v_size) && s_hard;
932 h_used_shallow_inprocess = h_used_shallow_inprocess || h_use_shallow_inprocess;
933 h_used_shallow_inprocess_quadratic = h_used_shallow_inprocess_quadratic ||
934 h_use_shallow_inprocess_quadratic;
935
936 // inprocess
937 s_inprocessed = m_inprocess.inprocess(g, sh_tree, sh_schreier, local_state, root_save, h_budget,
938 s_any_bfs_pruned,
939 h_use_shallow_inprocess || h_use_shallow_inprocess_quadratic,
940 h_use_shallow_inprocess_quadratic, m_dfs.orbs);
941
942 // record whether inprocessing was successful in any way
943 s_inproc_success += s_inprocessed;
944 if(s_inprocessed) m_printer.timer_print("inprocess", local_state.c->cells, s_inproc_success);
945
946 // inprocessing might finish the graph, in which case we terminate
947 if (root_save.get_coloring()->cells == g->v_size) {
948 s_term = t_inproc;
949 break;
950 }
951 } // end of restart loop
952
953 // we are done with this component...
954 // ...did we solve it deterministically?
955 s_deterministic_termination = (s_term != t_rand_schreier) && s_deterministic_termination;
956
957 // let's add up the total group size from all the different modules.
958 s_grp_sz.multiply(m_inprocess.s_grp_sz);
959 if(s_term != t_inproc) s_grp_sz.multiply(m_dfs.s_grp_sz);
960
961 // if we finished with BFS, group size in Schreier is redundant since we also found them with BFS
962 if(s_term != t_bfs && s_term != t_inproc) s_grp_sz.multiply(sh_schreier.get_group_size());
963 } // end of loop for non-uniform components
964 m_printer.h_silent = h_silent;
965 m_printer.timer_print("done", s_deterministic_termination, s_term);
966 }
967 };
968}
969
970#endif //DEJAVU_DEJAVU_H
Stores big numbers.
Definition: utility.h:138
long double mantissa
Definition: utility.h:140
void set(long double set_mantissa, int set_exponent)
Definition: utility.h:155
void multiply(int number)
Definition: utility.h:165
Vertex coloring for a graph.
Definition: coloring.h:23
Set specialized for quick resets.
Definition: ds.h:546
bool get(int pos)
Definition: ds.h:605
void reset()
Definition: ds.h:634
void initialize(int size)
Definition: ds.h:588
void set(int pos)
Definition: ds.h:616
T * get_array() const
Definition: ds.h:280
void resize(const int size)
Definition: ds.h:248
Workspace for sparse automorphisms.
Definition: groups.h:68
Compressed Schreier structure.
Definition: groups.h:1976
bool reset(domain_compressor *new_compressor, int new_domain_size, schreier_workspace &w, std::vector< int > &new_base, std::vector< int > &new_base_sizes, const int stop, bool keep_old, std::vector< int > &global_fixed_points)
Definition: groups.h:2010
dej_nodiscard bool deterministic_abort_criterion() const
Definition: groups.h:2190
dej_nodiscard big_number get_group_size() const
Definition: groups.h:2210
dej_nodiscard bool any_abort_criterion() const
Definition: groups.h:2197
dej_nodiscard int s_densegen() const
Definition: groups.h:1998
void set_error_bound(int error_bound)
Definition: groups.h:2202
dej_nodiscard int s_sparsegen() const
Definition: groups.h:1991
Compresses vertex set to smaller window.
Definition: groups.h:1874
void determine_compression_map(coloring &c, std::vector< int > &base, int stop)
Definition: groups.h:1894
Orbit partition.
Definition: groups.h:507
int orbit_size(const int v)
Definition: groups.h:538
void add_automorphism_to_orbit(const int *p, const int nsupp, const int *supp)
Definition: groups.h:613
API for the dejavu Schreier structure.
Definition: groups.h:1643
bool sift(automorphism_workspace &automorphism, bool known_in_group=false)
Definition: groups.h:1832
Auxiliary workspace used for Schreier computations.
Definition: groups.h:825
virtual dejavu_hook * get_hook()=0
virtual ~hook_interface()=default
Calls several other hooks.
Definition: dejavu.h:55
void add_hook(dejavu_hook *hook)
Definition: dejavu.h:65
dej_nodiscard size_t size() const
Definition: dejavu.h:73
dejavu_hook * get_hook() override
Definition: dejavu.h:77
Hook to feed an orbit structure.
Definition: dejavu.h:226
orbit_hook(groups::orbit &save_orbit)
Definition: dejavu.h:234
dejavu_hook * get_hook() override
Definition: dejavu.h:236
Writes to an ostream.
Definition: dejavu.h:96
dejavu_hook * get_hook() override
Definition: dejavu.h:124
ostream_hook(std::ostream &ostream)
Definition: dejavu.h:122
Hook to feed a Schreier structure.
Definition: dejavu.h:197
schreier_hook(groups::random_schreier &schreier)
Definition: dejavu.h:205
dejavu_hook * get_hook() override
Definition: dejavu.h:207
Certification on the original graph.
Definition: dejavu.h:148
dejavu_hook * get_hook() override
Definition: dejavu.h:178
strong_certification_hook(static_graph &g, dejavu_hook *call_hook)
Definition: dejavu.h:162
strong_certification_hook(sgraph &g, dejavu_hook *call_hook)
Definition: dejavu.h:166
void initialize(sgraph &g, dejavu_hook *call_hook)
Definition: dejavu.h:172
Creates cell selectors.
Definition: ir.h:1140
big_number get_ir_size_estimate()
Definition: ir.h:1216
void make_cell_selector(sgraph *g, controller *state, controller *state_probe, const selector_style style, const int h_seed, const int h_budget)
Definition: ir.h:1229
std::function< type_selector_hook > * get_selector_hook()
Definition: ir.h:1207
static bool certify_automorphism_sparse(markset &scratch_set, const sgraph *g, const int *p, int supp, const int *supp_arr)
Definition: refinement.h:88
Decomposes graphs and manages decomposition information.
Definition: components.h:110
sgraph * get_component(int i)
Definition: components.h:246
void decompose(sgraph *g, int *colmap, ds::worklist &vertex_to_component, int new_num_components)
Definition: components.h:142
Reduced IR save state.
Definition: ir.h:47
coloring * get_coloring()
Definition: ir.h:69
Color refinement and related algorithms.
Definition: refinement.h:143
bool certify_automorphism_sparse(const sgraph *g, const int *p, int supp, const int *supp_arr)
Definition: refinement.h:379
IR tree structure.
Definition: ir.h:1982
int get_current_level_tracepos()
Definition: ir.h:2238
int get_current_level_size()
Definition: ir.h:2234
int stat_leaves() const
Definition: ir.h:2084
int get_level_size(int level)
Definition: ir.h:2242
int h_bfs_automorphism_pw
Definition: ir.h:1997
groups::orbit h_bfs_top_level_orbit
Definition: ir.h:1996
bool reset(std::vector< int > &new_base, ir::limited_save *root, bool keep_old)
Definition: ir.h:2088
dej_nodiscard int get_finished_up_to() const
Definition: ir.h:2222
void clear_leaves()
Definition: ir.h:2077
dej_nodiscard int get_position() const
Definition: trace.h:316
preprocessor for symmetry detection
Definition: preprocess.h:32
void inject_decomposer(dejavu::ir::graph_decomposer *new_decomposer, int component)
Definition: preprocess.h:125
void reduce(dejavu::static_graph *g, dejavu_hook *hook, std::vector< preop > *schedule=nullptr)
Definition: preprocess.h:3370
dejavu::big_number grp_sz
Definition: preprocess.h:98
static void _dejavu_hook(int n, const int *aut, int nsupp, const int *supp)
Definition: preprocess.h:3678
Random number generation.
Definition: utility.h:104
Breadth-first search.
Definition: bfs.h:16
void do_a_level(sgraph *g, dejavu_hook *hook, ir::shared_tree &ir_tree, ir::controller &local_state, std::function< ir::type_selector_hook > *selector)
Definition: bfs.h:34
static int next_level_estimate(ir::shared_tree &ir_tree, std::function< ir::type_selector_hook > *selector)
Definition: bfs.h:51
Depth-first search without backtracking.
Definition: dfs.h:60
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
Inprocessing for symmetry detection.
Definition: inprocess.h:22
std::vector< std::pair< int, int > > inproc_maybe_individualize
Definition: inprocess.h:89
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
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
int check_individualizations(ir::limited_save &root_save)
Definition: inprocess.h:242
IR search using random walks.
Definition: rand.h:26
static void specific_walk(sgraph *g, ir::shared_tree &ir_tree, ir::controller &local_state, std::vector< int > &base_vertex)
Definition: rand.h:199
static bool h_almost_done(groups::compressed_schreier &group)
Definition: rand.h:194
void random_walks_from_tree(sgraph *g, dejavu_hook *hook, std::function< ir::type_selector_hook > *selector, ir::shared_tree &ir_tree, groups::compressed_schreier &group, ir::controller &local_state, ir::controller &other_state, int fail_limit)
Definition: rand.h:392
void random_walks(sgraph *g, dejavu_hook *hook, std::function< ir::type_selector_hook > *selector, ir::shared_tree &ir_tree, groups::compressed_schreier &group, ir::controller &local_state, ir::controller &other_state, int fail_limit)
Definition: rand.h:224
void use_look_close(bool look_close=false)
Definition: rand.h:164
Internal graph data structure.
Definition: graph.h:19
void copy_graph(sgraph *g)
Definition: graph.h:243
int e_size
Definition: graph.h:49
void initialize_coloring(ds::coloring *c, int *vertex_to_col)
Definition: graph.h:61
int v_size
Definition: graph.h:48
bool dense
Definition: graph.h:51
The dejavu solver.
Definition: dejavu.h:257
dej_nodiscard big_number get_automorphism_group_size() const
Definition: dejavu.h:389
void set_pseudo_random(bool use_pseudo_random=true)
Definition: dejavu.h:328
dej_nodiscard bool get_deterministic_termination() const
Definition: dejavu.h:397
int get_error_bound() const
Definition: dejavu.h:298
void set_decompose(bool use_decompose=true)
Definition: dejavu.h:363
void automorphisms(static_graph *g, hooks::hook_interface &hook)
Definition: dejavu.h:425
void set_true_random(bool use_true_random=true)
Definition: dejavu.h:308
void automorphisms(sgraph *g, int *colmap=nullptr, dejavu_hook *hook=nullptr)
Definition: dejavu.h:432
void set_prefer_dfs(bool prefer_dfs=true)
Definition: dejavu.h:318
void automorphisms(static_graph *g, dejavu_hook hook)
Definition: dejavu.h:417
void set_seed(int seed=0)
Definition: dejavu.h:336
void set_strong_certification(bool use_strong_certification=true)
Definition: dejavu.h:345
void set_print(bool print=true)
Definition: dejavu.h:381
void set_disallow_alteration(bool may_alter_graph=false)
Definition: dejavu.h:354
void automorphisms(static_graph *g, dejavu_hook *hook=nullptr)
Definition: dejavu.h:410
void randomize_seed()
Definition: dejavu.h:371
void set_error_bound(int error_bound=10)
Definition: dejavu.h:288
Graph with static number of vertices and edges.
Definition: graph.h:292
int * get_coloring()
Definition: graph.h:433
dejavu::sgraph * get_sgraph()
Definition: graph.h:428
Prints information to the console.
Definition: utility.h:237
void timer_split()
Definition: utility.h:275
void print_split() const
Definition: utility.h:254
void print(const std::string &str) const
Definition: utility.h:259
void timer_print(const std::string &proc, const std::string &p1, const std::string &p2)
Definition: utility.h:264
void print_header() const
Definition: utility.h:249
dejavu::ir::refinement test_r
Definition: dejavu.cpp:13
dejavu::sgraph dej_test_graph
Definition: dejavu.cpp:14
Definition: bfs.h:10
Controls movement in IR tree.
Definition: ir.h:130
void compare_to_this()
Definition: ir.h:778
std::vector< base_info > base
Definition: ir.h:139
coloring * c
Definition: ir.h:132
void save_reduced_state(limited_save &state)
Definition: ir.h:883
void set_increase_deviation(int deviation_inc=48)
Definition: ir.h:854
void reserve()
Definition: ir.h:800
void load_reduced_state(limited_save &state)
Definition: ir.h:893
std::vector< int > base_vertex
Definition: ir.h:138
std::function< void(int, const int *, int, const int *)> dejavu_hook
Definition: utility.h:95
#define dej_nodiscard
Definition: utility.h:46
#define PRINT(str)
Definition: utility.h:35