dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
refinement.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_REFINEMENT_H
6#define DEJAVU_REFINEMENT_H
7
8#include "ds.h"
9#include "coloring.h"
10#include "graph.h"
11#include "utility.h"
12
13namespace dejavu {
14
15 using namespace ds;
16
17 namespace ir {
18
25 private:
26 static bool bijection_check(markset& scratch_set, int n, const int *p) {
27 scratch_set.reset();
28 bool comp = true;
29 for(int i = 0; i < n && comp; ++i) {
30 const int v = p[i];
31 comp = !scratch_set.get(v);
32 scratch_set.set(v);
33 }
34 return comp;
35 }
36
37 static bool cycle_check(markset& scratch_set, const int *p, int supp, const int *supp_arr) {
38 scratch_set.reset();
39 bool comp = true;
40 for(int i = 0; i < supp && comp; ++i) {
41 const int v = supp_arr[i];
42 if(scratch_set.get(v)) continue;
43 int v_next = p[v];
44 while(v_next != v && comp) {
45 comp = !scratch_set.get(v_next);
46 scratch_set.set(v_next);
47 v_next = p[v_next];
48 }
49 }
50 return comp;
51 }
52
53 public:
54 // certify an automorphism on a graph
55 static bool certify_automorphism(markset& scratch_set, sgraph *g, const int *p) {
56 if(!bijection_check(scratch_set, g->v_size, p)) return false;
57
58 for (int i = 0; i < g->v_size; ++i) {
59 const int image_i = p[i];
60 if (image_i == i) continue;
61
62 scratch_set.reset();
63 // automorphism must preserve neighbours
64 int found = 0;
65 const int start_pt = g->v[i];
66 const int end_pt = g->v[i] + g->d[i];
67 for (int j = start_pt; j < end_pt; ++j) {
68 const int vertex_j = g->e[j];
69 const int image_j = p[vertex_j];
70 scratch_set.set(image_j);
71 found += 1;
72 }
73 const int image_start_pt = g->v[image_i];
74 const int image_end_pt = g->v[image_i] + g->d[image_i];
75 for (int j = image_start_pt; j < image_end_pt; ++j) {
76 const int vertex_j = g->e[j];
77 if (!scratch_set.get(vertex_j)) return false;
78 scratch_set.unset(vertex_j);
79 found -= 1;
80 }
81 if (found != 0) return false;
82 }
83
84 return true;
85 }
86
87 // certify an automorphism on a graph, sparse
88 static bool certify_automorphism_sparse(markset& scratch_set, const sgraph *g, const int *p, int supp,
89 const int *supp_arr) {
90 int i, found;
91 if(!cycle_check(scratch_set, p, supp, supp_arr)) return false;
92
93 for (int f = 0; f < supp; ++f) {
94 i = supp_arr[f];
95 const int image_i = p[i];
96 scratch_set.reset();
97 // automorphism must preserve neighbours
98 found = 0;
99 const int start_pt = g->v[i];
100 const int end_pt = g->v[i] + g->d[i];
101 for (int j = start_pt; j < end_pt; ++j) {
102 const int vertex_j = g->e[j];
103 const int image_j = p[vertex_j];
104 scratch_set.set(image_j);
105 found += 1;
106 }
107 const int image_start_pt = g->v[image_i];
108 const int image_end_pt = g->v[image_i] + g->d[image_i];
109 for (int j = image_start_pt; j < image_end_pt; ++j) {
110 const int vertex_j = g->e[j];
111 if (!scratch_set.get(vertex_j)) {
112 scratch_set.reset();
113 return false;
114 }
115 found -= 1;
116 }
117 if (found != 0) {
118 scratch_set.reset();
119 return false;
120 }
121 }
122 scratch_set.reset();
123 return true;
124 }
125 };
126
127
128 // return whether to continue color refinement
129 // bool split_color_hook(int color_initial, int new_color, int new_color_sz);
130 typedef bool type_split_color_hook(const int, const int, const int);
131
132 // return whether to continue splitting the respective cell, or skip it
133 // bool worklist_color_hook(int color, int color_sz);
134 typedef bool type_worklist_color_hook(const int, const int);
135
144 bool g_early_out = false;
145 const std::function<type_split_color_hook>* g_split_hook;
146
147 public:
161 void refine_coloring(sgraph *g, coloring *c, int init_color = -1, int color_limit = -1,
162 const std::function<type_split_color_hook>* split_hook = nullptr,
163 const std::function<type_worklist_color_hook>* worklist_hook = nullptr) {
164 assure_initialized(g);
165 cell_todo.reset(queue_pointer);
166
167 if (init_color < 0) {
168 // initialize queue with all classes (except for largest one)
169 for (int i = 0; i < c->domain_size;) {
170 cell_todo.add_cell(queue_pointer, i);
171 const int col_sz = c->ptn[i];
172 i += col_sz + 1;
173 }
174 } else {
175 dej_assert(c->vertex_to_col[c->lab[init_color]] == init_color);
176 cell_todo.add_cell(queue_pointer, init_color);
177 }
178
179 g_early_out = false;
180 g_split_hook = split_hook;
181
182 while (!cell_todo.empty()) {
183 const int next_color_class = cell_todo.next_cell(queue_pointer, c);
184 const int next_color_class_sz = c->ptn[next_color_class] + 1;
185
186 if (worklist_hook && !(*worklist_hook)(next_color_class, next_color_class_sz)) continue;
187
188 // this scheme is reverse-engineered from the color refinement in Traces by Adolfo Piperno
189 // we choose a separate algorithm depending on the size and density of the graph and/or color class
190 const int test_deg = g->d[c->lab[next_color_class]];
191 const bool very_dense = test_deg > (g->v_size / (next_color_class_sz + 1));
192 //const bool cell_dense = test_deg > (c->cells);
193
194 if (next_color_class_sz == 1 && !(g->dense && very_dense)) { // singleton
195 refine_color_class_singleton(g, c, next_color_class);
196 } else if (g->dense) {
197 if (very_dense) { // dense-dense
198 refine_color_class_dense_dense(g, c, next_color_class,next_color_class_sz);
199 } //else if(cell_dense) { // dense-cell
200 //refine_color_class_dense_cell(g, c, next_color_class, next_color_class_sz);
201 //}
202 else { // dense-sparse
203 refine_color_class_dense(g, c, next_color_class, next_color_class_sz);
204 }
205 } else { // sparse
206 refine_color_class_sparse(g, c, next_color_class, next_color_class_sz);
207 }
208
209 // early out possible?
210 if (g_early_out || c->cells == g->v_size || c->cells == color_limit) {
211 cell_todo.reset(queue_pointer);
212 break;
213 }
214 }
215 }
216 private:
217 void report_split_color_class(coloring* c, const int old_class, const int new_class, const int new_class_sz,
218 const bool is_largest) {
219 c->cells += (old_class != new_class);
220 dej_assert(c->ptn[new_class] + 1 == new_class_sz);
221
222 if ((g_split_hook != nullptr) && !(*g_split_hook)(old_class, new_class, new_class_sz)) {
223 g_early_out = true;
224 }
225
226 if (!is_largest && old_class != new_class) {
227 cell_todo.add_cell(queue_pointer, new_class);
228 } else if(is_largest) {
229 // since old color class is skipped above, this should be safe
230 int i = queue_pointer.get(old_class);
231 if (i >= 0) cell_todo.replace_cell(queue_pointer, old_class, new_class);
232 if(old_class != new_class) cell_todo.add_cell(queue_pointer, old_class);
233 }
234 }
235
236 public:
244 static int
245 individualize_vertex(coloring *c, int v, const std::function<type_split_color_hook> &split_hook = nullptr) {
246 const int color = c->vertex_to_col[v];
247 const int pos = c->vertex_to_lab[v];
248
249 int color_class_size = c->ptn[color];
250
251 dej_assert(color_class_size > 0);
252
253 const int vertex_at_pos = c->lab[color + color_class_size];
254 c->lab[pos] = vertex_at_pos;
255 c->vertex_to_lab[vertex_at_pos] = pos;
256
257 c->lab[color + color_class_size] = v;
258 c->vertex_to_lab[v] = color + color_class_size;
259 c->vertex_to_col[v] = color + color_class_size;
260
261 c->ptn[color] -= 1;
262 c->ptn[color + color_class_size] = 0;
263 c->ptn[color + color_class_size - 1] = 0;
264 c->cells += 1;
265
266 if (split_hook) {
267 split_hook(color, color + color_class_size, 1);
268 split_hook(color, color, c->ptn[color] + 1);
269 }
270
271 return color + color_class_size;
272 }
273
284 void refine_coloring_first(sgraph *g, coloring *c, int init_color_class = -1) {
285 assure_initialized(g);
286 singleton_hint.reset();
287
288 cell_todo.reset(queue_pointer);
289
290 if (init_color_class < 0) {
291 for (int i = 0; i < c->domain_size;) {
292 cell_todo.add_cell(queue_pointer, i);
293 const int col_sz = c->ptn[i];
294 if (col_sz == 0) {
295 singleton_hint.push_back(i);
296 }
297 i += col_sz + 1;
298 }
299 } else {
300 cell_todo.add_cell(queue_pointer, init_color_class);
301 }
302
303 while (!cell_todo.empty()) {
304 const int next_color_class = cell_todo.next_cell(queue_pointer, c, singleton_hint);
305 const int next_color_class_sz = c->ptn[next_color_class] + 1;
306 const bool very_dense = (g->d[c->lab[next_color_class]] > (g->v_size / (next_color_class_sz + 1)));
307
308 if (next_color_class_sz == 1 && !(g->dense && very_dense)) {
309 // singleton
310 refine_color_class_singleton_first(g, c, next_color_class);
311 } else if (g->dense) {
312 if (very_dense) { // dense-dense
313 refine_color_class_dense_dense_first(g, c, next_color_class, next_color_class_sz);
314 } else { // dense-sparse
315 refine_color_class_dense_first(g, c, next_color_class, next_color_class_sz);
316 }
317 } else { // sparse
318 refine_color_class_sparse_first(g, c, next_color_class, next_color_class_sz);
319 }
320
321 if (c->cells == g->v_size) {
322 cell_todo.reset(queue_pointer);
323 return;
324 }
325 }
326 }
327
328 private:
329 void report_split_color_class_first(coloring* c, int old_class, int new_class, int new_class_sz,
330 bool is_largest) {
331 c->cells += (old_class != new_class);
332 dej_assert(c->ptn[new_class] + 1 == new_class_sz);
333
334 if (!is_largest && old_class != new_class) {
335 cell_todo.add_cell(queue_pointer, new_class);
336 if (new_class_sz == 1) singleton_hint.push_back(new_class);
337 } else if(is_largest) {
338 // since old color class is skipped above, this should be safe
339 int i = queue_pointer.get(old_class);
340 if (i >= 0) {
341 cell_todo.replace_cell(queue_pointer, old_class, new_class);
342 if(new_class_sz == 1) singleton_hint.push_back(new_class);
343 }
344 if(old_class != new_class) {
345 cell_todo.add_cell(queue_pointer, old_class);
346 if(c->ptn[old_class] + 1 == 1) singleton_hint.push_back(old_class);
347 }
348 }
349 }
350
351 public:
362 bool certify_automorphism(sgraph *g, const int *p) {
363 assure_initialized(g);
364 return certification::certify_automorphism(scratch_set, g, p);
365 }
366
379 bool certify_automorphism_sparse(const sgraph *g, const int *p, int supp, const int *supp_arr) {
380 assure_initialized(g);
381 return certification::certify_automorphism_sparse(scratch_set, g, p, supp, supp_arr);
382 }
383
384 private:
385 // worklist implementation for color refinement
386 class cell_worklist {
387 public:
388 void initialize(int _domain_size) {
389 arr = new int[_domain_size];
390 arr_sz = _domain_size;
391 init = true;
392 cur_pos = 0;
393 }
394
395 ~cell_worklist() {
396 delete[] arr;
397 }
398
399 int add_cell(work_set_int& _queue_pointer, int col) {
400 dej_assert(init);
401 dej_assert(cur_pos >= 0 && cur_pos < arr_sz - 1);
402 _queue_pointer.set(col, cur_pos);
403 arr[cur_pos] = col;
404 cur_pos++;
405 return 0;
406 }
407
408 int next_cell(work_set_int& _queue_pointer, coloring *c) {
409 // look at first 12 positions and pick the (first) smallest cell within these entries
410 int sm_j = cur_pos - 1; /*< AKA "smallest j" */
411 for (int j = cur_pos - 1; j >= 0 && ((cur_pos - j) <= 12); --j) {
412 if (c->ptn[arr[j]] < c->ptn[arr[sm_j]]) {
413 sm_j = j;
414 if (c->ptn[arr[sm_j]] == 0)
415 break;
416 }
417 }
418
419 // swap sm_j and j
420 const int sm_col = arr[sm_j];
421 arr[sm_j] = arr[cur_pos - 1];
422 _queue_pointer.set(arr[sm_j], sm_j);
423
424 cur_pos--;
425 _queue_pointer.set(sm_col, -1);
426 return sm_col;
427 }
428
429 int next_cell(work_set_int& _queue_pointer, coloring *c, worklist_t<int>& _singleton_hint) {
430 // use singleton_hint
431 int sm_j = -1; /*< AKA "smallest j" */
432 while (!_singleton_hint.empty() && sm_j == -1) {
433 const int next_hint = _singleton_hint.pop_back();
434 sm_j = _queue_pointer.get(next_hint);
435 }
436
437 // look at first 12 positions and pick the (first) smallest cell within these entries
438 if (sm_j == -1) {
439 sm_j = cur_pos - 1;
440 for (int j = cur_pos - 1; j >= 0 && ((cur_pos - j) <= 12); --j) {
441 const int size_sm_j = c->ptn[arr[sm_j]];
442 const bool smaller = (c->ptn[arr[j]] < size_sm_j);
443 sm_j = smaller ? j : sm_j;
444 if (size_sm_j - smaller <= 0) break;
445 }
446 }
447
448 // swap sm_j and j
449 const int sm_col = arr[sm_j];
450 arr[sm_j] = arr[cur_pos - 1];
451 _queue_pointer.set(arr[sm_j], sm_j);
452
453 cur_pos--;
454 _queue_pointer.set(sm_col, -1);
455 return sm_col;
456 }
457
458 void replace_cell(work_set_int& _queue_pointer, int col_old, int col) {
459 const int pos = _queue_pointer.get(col_old);
460 arr[pos] = col;
461 dej_assert(_queue_pointer.get(col_old) != -1);
462 _queue_pointer.set(col_old, -1);
463 _queue_pointer.set(col, pos);
464 }
465
466 void reset(work_set_int& _queue_pointer) {
467 while (cur_pos > 0) {
468 cur_pos--;
469 _queue_pointer.set(arr[cur_pos], -1);
470 }
471 }
472
473 dej_nodiscard bool empty() const {
474 return (cur_pos == 0);
475 }
476
477 dej_nodiscard int size() const {
478 return cur_pos;
479 }
480
481 private:
482 int *arr = nullptr;
483 int arr_sz = -1;
484 int cur_pos = -1;
485 bool init = false;
486 };
487
488 int domain_size = -1;
489
490 // worklist of color refinement algorithm
491 work_set_int queue_pointer;
492 cell_worklist cell_todo;
493 worklist_t<int> singleton_hint;
494
495 // helper data structures for color refinement
496 markset scratch_set;
497 worklist_t<int> vertex_worklist;
498 workset_t<int> color_vertices_considered; // todo should use different datastructure, with n space not 2n
499 workset_t<int> neighbours;
500 workset_t<int> neighbour_sizes;
501 worklist_t<int> old_color_classes;
502 workspace scratch;
503
504 void assure_initialized(const sgraph *g) {
505 if (g->v_size > domain_size) {
506 const int n = g->v_size;
507
508 vertex_worklist.allocate(n * 2);
509 singleton_hint.allocate(n);
510 old_color_classes.allocate(n);
511 neighbours.initialize(n);
512 neighbour_sizes.initialize(n);
513 queue_pointer.initialize(n);
514 color_vertices_considered.initialize(n);
515 scratch.resize(n);
516 scratch_set.initialize(n);
517 cell_todo.initialize(n * 2);
518 domain_size = n;
519 }
520 }
521
522 void refine_color_class_sparse(sgraph *g, coloring *c, int color_class,
523 int class_size) {
524 // for all vertices of the color class...
525 int i, j, cc, end_cc, largest_color_class_size, acc;
526 int *vertex_to_lab = c->vertex_to_lab;
527 int *lab = c->lab;
528 int *ptn = c->ptn;
529 int *vertex_to_col = c->vertex_to_col;
530
531 cc = color_class; // iterate over color class
532
533 old_color_classes.reset();
534 neighbours.reset();
535 color_vertices_considered.reset();
536
537 end_cc = color_class + class_size;
538 while (cc < end_cc) { // increment value of neighbours of vc by 1
539 const int vc = lab[cc];
540 const int pe = g->v[vc];
541 const int end_i = pe + g->d[vc];
542 for (i = pe; i < end_i; i++) {
543 const int v = g->e[i];
544 const int col = vertex_to_col[v];
545 if (ptn[col] == 0) {
546 continue;
547 }
548 neighbours.inc_nr(v);
549 if (neighbours.get(v) == 0) {
550 color_vertices_considered.inc_nr(col);
551 dej_assert(col + color_vertices_considered.get(col) < g->v_size);
552 scratch[col + color_vertices_considered.get(col)] = v; // hit vertices
553 if (color_vertices_considered.get(col) == 0) {
554 old_color_classes.push_back(col);
555 }
556 }
557 }
558 cc += 1;
559 }
560
561 // remove color classes from list if they don't split
562 for(j = 0; j < old_color_classes.size(); ++j) {
563 const int _col = old_color_classes[j];
564 const int _col_sz = ptn[_col] + 1;
565 const int vcount = color_vertices_considered.get(_col) + 1;
566
567 if(vcount == _col_sz) {
568 const int v_first = scratch[_col];
569 const int index_first = neighbours.get(v_first) + 1;
570 bool splits = false;
571
572 for (i = 1; i < vcount; ++i) {
573 const int v = scratch[_col + i];
574 const int index = neighbours.get(v) + 1;
575 splits = index != index_first;
576 if(splits) break;
577 }
578
579 if(splits) continue;
580
581 i = 0;
582 while (i < vcount) {
583 const int v = scratch[_col + i];
584 neighbours.set(v, -1);
585 ++i;
586 }
587
588 color_vertices_considered.set(_col, -1);
589
590 old_color_classes[j] = old_color_classes[old_color_classes.size() - 1];
591 old_color_classes.pop_back();
592 continue;
593 }
594 }
595
596 // sort split color classes
597 old_color_classes.sort();
598
599 // now split the color classes according to neighbour count
600 while (!old_color_classes.empty()) {
601 const int _col = old_color_classes.pop_back();
602 const int _col_sz = ptn[_col] + 1;
603 const int vcount = color_vertices_considered.get(_col) + 1;
604 neighbour_sizes.reset();
605 vertex_worklist.reset();
606
607 for (i = 0; i < vcount; ++i) {
608 const int v = scratch[_col + i];
609 const int index = neighbours.get(v) + 1;
610 if (neighbour_sizes.inc(index) == 0) vertex_worklist.push_back(index);
611 }
612
613 if(vcount == _col_sz && vertex_worklist.cur_pos == 1) {
614 vertex_worklist.reset();
615 j = 0;
616 while (j < vcount) {
617 const int v = scratch[_col + j];
618 neighbours.set(v, -1);
619 ++j;
620 }
621 color_vertices_considered.set(_col, -1);
622 continue;
623 }
624
625 vertex_worklist.sort();
626
627 // enrich neighbour_sizes to accumulative counting array
628 acc = 0;
629 while (!vertex_worklist.empty()) {
630 const int k = vertex_worklist.pop_back();
631 const int val = neighbour_sizes.get(k) + 1;
632 if (val >= 1) {
633 neighbour_sizes.set(k, val + acc);
634 acc += val;
635 const int _ncol = _col + _col_sz - (neighbour_sizes.get(k));
636 if (_ncol != _col)
637 ptn[_ncol] = -1;
638 }
639 }
640
641
642 vertex_worklist.reset();
643 j = 0;
644 color_vertices_considered.set(_col, -1);
645
646 // determine colors and rearrange vertices
647 while (j < vcount) {
648 const int v = scratch[_col + j];
649 ++j;
650 if ((neighbours.get(v) == -1))
651 continue;
652 const int v_new_color = _col + _col_sz - neighbour_sizes.get(neighbours.get(v) + 1);
653 neighbours.set(v, -1);
654 if (v_new_color == _col)
655 continue;
656
657 const int lab_pt = v_new_color + ptn[v_new_color] + 1;
658 ptn[v_new_color] += 1;
659 ptn[_col] -= (_col != v_new_color);
660
661 const int vertex_old_pos = vertex_to_lab[v];
662 const int vertex_at_pos = lab[lab_pt];
663 lab[vertex_old_pos] = vertex_at_pos;
664 vertex_to_lab[vertex_at_pos] = vertex_old_pos;
665 lab[lab_pt] = v;
666 vertex_to_col[v] = v_new_color;
667 vertex_to_lab[v] = lab_pt;
668 }
669
670 // add new colors to worklist
671 largest_color_class_size = -1;
672 int largest_color_class = -1;
673 for (i = _col; i < _col + _col_sz;) {
674 dej_assert(i >= 0 && i < c->domain_size);
675 dej_assert(c->ptn[i] + 1 > 0);
676 const bool new_largest = largest_color_class_size < (ptn[i] + 1);
677 largest_color_class_size = new_largest? (ptn[i] + 1) : largest_color_class_size;
678 largest_color_class = new_largest? i : largest_color_class;
679 i += ptn[i] + 1;
680 }
681 dej_assert(largest_color_class >= _col);
682 dej_assert(largest_color_class < _col + _col_sz);
683
684 for (i = _col; i < _col + _col_sz;) {
685 const int i_sz = ptn[i] + 1;
686 const bool is_largest = i == largest_color_class;
687 report_split_color_class(c, _col, i, i_sz, is_largest);
688 i += i_sz;
689 }
690 }
691
692 neighbour_sizes.reset();
693 vertex_worklist.reset();
694 }
695
696 void refine_color_class_dense(sgraph *g, coloring *c, int color_class, int class_size) {
697 int i, cc, acc, largest_color_class_size, pos;
698 cc = color_class; // iterate over color class
699
700 neighbours.reset();
701 scratch_set.reset();
702 old_color_classes.reset();
703 vertex_worklist.reset();
704
705 const int end_cc = color_class + class_size;
706
707 // for all vertices of the color class...
708 while (cc < end_cc) { // increment value of neighbours of vc by 1
709 const int vc = c->lab[cc];
710 const int pe = g->v[vc];
711 const int end_i = pe + g->d[vc];
712 for (i = pe; i < end_i; i++) {
713 const int v = g->e[i];
714 const int col = c->vertex_to_col[v];
715 if (c->ptn[col] > 0) {
716 neighbours.inc(v); // want to use reset variant?
717 if (!scratch_set.get(col)) {
718 scratch_set.set(col);
719 old_color_classes.push_back(col);
720 }
721 }
722 }
723 cc += 1;
724 }
725
726 // remove color classes from list if they don't split
727 for(int j = 0; j < old_color_classes.size(); ++j) {
728 const int _col = old_color_classes[j];
729 const int _col_sz = c->ptn[_col] + 1;
730
731 const int v_first = c->lab[_col];
732 const int index_first = neighbours.get(v_first);
733 bool splits = false;
734
735 for (i = 1; i < _col_sz && !splits; ++i) {
736 const int v = c->lab[_col + i];
737 const int index = neighbours.get(v);
738 splits = index != index_first;
739 }
740
741 if(splits) continue;
742
743 old_color_classes[j] = old_color_classes[old_color_classes.size() - 1];
744 old_color_classes.pop_back();
745 }
746
747 old_color_classes.sort();
748
749 // for every cell to be split...
750 while (!old_color_classes.empty()) {
751 const int col = old_color_classes.pop_back();
752 const int col_sz = c->ptn[col] + 1;
753 if (col_sz == 1) continue;
754
755 neighbour_sizes.reset();
756 vertex_worklist.reset();
757
758 const int first_index = neighbours.get(c->lab[col]) + 1;
759 vertex_worklist.push_back(first_index);
760 int total = 0;
761 for (i = col; i < col + col_sz; ++i) {
762 const int v = c->lab[i];
763 int index = neighbours.get(v) + 1;
764 if (index == first_index) continue;
765 total += 1;
766 if (neighbour_sizes.inc(index) == 0)
767 vertex_worklist.push_back(index);
768 }
769
770 neighbour_sizes.inc(first_index);
771 neighbour_sizes.set(first_index, col_sz - total - 1);
772
773 if (vertex_worklist.cur_pos == 1) continue;
774
775 //if(vertex_worklist.cur_pos < 8)
776 vertex_worklist.sort();
777 //else bucket_sort(vertex_worklist, scratch_set, vertex_worklist.max());
778
779 // enrich neighbour_sizes to accumulative counting array
780 acc = 0;
781 while (!vertex_worklist.empty()) {
782 const int j = vertex_worklist.pop_back();
783 const int val = neighbour_sizes.get(j) + 1;
784 if (val >= 1) {
785 neighbour_sizes.set(j, val + acc);
786 acc += val;
787 const int _col = col + col_sz - (neighbour_sizes.get(j));
788 c->ptn[_col] = -1; // this is val - 1, actually...
789 }
790 }
791
792 vertex_worklist.reset();
793
794 // copy cell for rearranging
795 memcpy(scratch.get_array(), c->lab + col, col_sz * sizeof(int));
796 pos = col_sz;
797
798 // determine colors and rearrange
799 // split color classes according to count in counting array
800 while (pos > 0) {
801 const int v = scratch[--pos];
802 const int v_new_color = col + col_sz - (neighbour_sizes.get(neighbours.get(v) + 1));
803 // i could immediately determine size of v_new_color here and write invariant before rearrange?
804 dej_assert(v_new_color >= col);
805 dej_assert(v_new_color < col + col_sz);
806
807 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
808 c->vertex_to_col[v] = v_new_color;
809 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
810 c->ptn[v_new_color] += 1;
811 }
812
813 largest_color_class_size = -1;
814 int largest_color_class = 0;
815 // determine largest class to throw away
816 for (i = col; i < col + col_sz;) {
817 dej_assert(i >= 0 && i < c->domain_size);
818 dej_assert(c->ptn[i] + 1 > 0);
819 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
820 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
821 largest_color_class = new_largest? i : largest_color_class;
822 if (i != 0) c->ptn[i - 1] = 0;
823 i += c->ptn[i] + 1;
824 }
825 dej_assert(largest_color_class >= col);
826 dej_assert(largest_color_class < col + col_sz);
827
828 // report splits
829 for (i = col; i < col + col_sz;) {
830 const int i_sz = c->ptn[i] + 1;
831 report_split_color_class(c, col, i, i_sz, i == largest_color_class);
832 i += i_sz;
833 }
834 }
835
836 neighbours.reset();
837 }
838
839 void refine_color_class_dense_cell(sgraph *g, coloring *c, int color_class, int class_size) {
840 int i, cc, acc, largest_color_class_size, pos;
841 cc = color_class; // iterate over color class
842
843 //neighbours.reset_hard();
844 neighbours.reset();
845 scratch_set.reset();
846 old_color_classes.reset();
847 vertex_worklist.reset();
848
849 const int end_cc = color_class + class_size;
850
851 // for all vertices of the color class...
852 while (cc < end_cc) { // increment value of neighbours of vc by 1
853 const int vc = c->lab[cc];
854 const int pe = g->v[vc];
855 const int end_i = pe + g->d[vc];
856 for (i = pe; i < end_i; i++) {
857 const int v = g->e[i];
858 const int col = c->vertex_to_col[v];
859 neighbours.inc(v);
860 scratch_set.set(col);
861 }
862 cc += 1;
863 }
864
865 // for every cell to be split...
866 for(int _col = 0; _col < g->v_size;) {
867 const int col_sz = c->ptn[_col] + 1;
868 const int col = _col;
869 _col += col_sz;
870 if (col_sz == 1 || !scratch_set.get(col)) continue;
871
872 neighbour_sizes.reset();
873 vertex_worklist.reset();
874
875 const int first_index = neighbours.get(c->lab[col]) + 1;
876 vertex_worklist.push_back(first_index);
877 int total = 0;
878 for (i = col; i < col + col_sz; ++i) {
879 const int v = c->lab[i];
880 int index = neighbours.get(v) + 1;
881 if (index == first_index) continue;
882 total += 1;
883 if (neighbour_sizes.inc(index) == 0)
884 vertex_worklist.push_back(index);
885 }
886
887 neighbour_sizes.inc(first_index);
888 neighbour_sizes.set(first_index, col_sz - total - 1);
889
890 if (vertex_worklist.cur_pos == 1) continue;
891
892 vertex_worklist.sort();
893 // enrich neighbour_sizes to accumulative counting array
894 acc = 0;
895 while (!vertex_worklist.empty()) {
896 const int j = vertex_worklist.pop_back();
897 const int val = neighbour_sizes.get(j) + 1;
898 if (val >= 1) {
899 neighbour_sizes.set(j, val + acc);
900 acc += val;
901 const int rcol = col + col_sz - (neighbour_sizes.get(j));
902 c->ptn[rcol] = -1; // this is val - 1, actually...
903 }
904 }
905
906 // copy cell for rearranging
907 memcpy(scratch.get_array(), c->lab + col, col_sz * sizeof(int));
908 //vertex_worklist.cur_pos = col_sz;
909 pos = col_sz;
910
911 // determine colors and rearrange
912 // split color classes according to count in counting array
913 while (pos > 0) {
914 const int v = scratch[--pos];
915 const int v_new_color = col + col_sz - (neighbour_sizes.get(neighbours.get(v) + 1));
916 // i could immediately determine size of v_new_color here and write invariant before rearrange?
917 dej_assert(v_new_color >= col);
918 dej_assert(v_new_color < col + col_sz);
919
920 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
921 c->vertex_to_col[v] = v_new_color;
922 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
923 c->ptn[v_new_color] += 1;
924 }
925
926 largest_color_class_size = -1;
927 int largest_color_class = 0;
928 // determine largest class to throw away
929 for (i = col; i < col + col_sz;) {
930 dej_assert(i >= 0 && i < c->domain_size);
931 dej_assert(c->ptn[i] + 1 > 0);
932 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
933 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
934 largest_color_class = new_largest? i : largest_color_class;
935 if (i != 0) c->ptn[i - 1] = 0;
936 i += c->ptn[i] + 1;
937 }
938 dej_assert(largest_color_class >= col);
939 dej_assert(largest_color_class < col + col_sz);
940
941 // report splits
942 for (i = col; i < col + col_sz;) {
943 const int i_sz = c->ptn[i] + 1;
944 report_split_color_class(c, col, i, i_sz, i == largest_color_class);
945 i += i_sz;
946 }
947 }
948
949 neighbours.reset();
950 }
951
952 void refine_color_class_dense_dense(sgraph *g, coloring *c, int color_class, int class_size) {
953 int i, j, acc, cc, largest_color_class_size;
954 int deg = -1;
955 cc = color_class; // iterate over color class
956
957 neighbours.reset();
958
959 const int end_cc = color_class + class_size;
960 while (cc < end_cc) { // increment value of neighbours of vc by 1
961 const int vc = c->lab[cc];
962 const int pe = g->v[vc];
963 deg = g->d[vc];
964 const int end_i = pe + deg - (deg==g->v_size-1?deg:0); // special code for universal vertices
965
966 for (i = pe; i < end_i; i++) {
967 const int v = g->e[i];
968 neighbours.inc_nr(v);
969 }
970 cc += 1;
971 }
972
973 if(class_size == 1 && deg == g->v_size-1) return; // special code for universal singletons
974
975 // in dense-dense we dont sort, instead we just iterate over all cells (which are already sorted)
976 // for every cell...
977 for (j = 0; j < g->v_size;) {
978 const int col = j;
979 const int col_sz = c->ptn[col] + 1;
980 j += col_sz;
981 if (col_sz == 1) continue;
982
983 neighbour_sizes.reset();
984 vertex_worklist.reset();
985
986 const int first_index = neighbours.get(c->lab[col]) + 1;
987 vertex_worklist.push_back(first_index);
988 int total = 0;
989 for (i = col; i < col + col_sz; ++i) {
990 const int v = c->lab[i];
991 const int index = neighbours.get(v) + 1;
992 if (index == first_index) continue;
993 total += 1;
994 if (neighbour_sizes.inc(index) == 0)
995 vertex_worklist.push_back(index);
996 }
997
998 neighbour_sizes.inc(first_index);
999 neighbour_sizes.set(first_index, col_sz - total - 1);
1000
1001 if (vertex_worklist.cur_pos == 1) continue; // no split
1002
1003 vertex_worklist.sort();
1004 // enrich neighbour_sizes to accumulative counting array
1005 acc = 0;
1006 while (!vertex_worklist.empty()) {
1007 const int k = vertex_worklist.pop_back();
1008 const int val = neighbour_sizes.get(k) + 1;
1009 if (val >= 1) {
1010 neighbour_sizes.set(k, val + acc);
1011 acc += val;
1012 const int _col = col + col_sz - (neighbour_sizes.get(k));
1013 c->ptn[_col] = -1; // this is val - 1, actually...
1014 }
1015 }
1016
1017 vertex_worklist.reset();
1018
1019 // copy cell for rearranging
1020 memcpy(vertex_worklist.get_array(), c->lab + col, col_sz * sizeof(int));
1021 vertex_worklist.cur_pos = col_sz;
1022
1023 // determine colors and rearrange
1024 // split color classes according to count in counting array
1025 while (!vertex_worklist.empty()) {
1026 const int v = vertex_worklist.pop_back();
1027 //for(i = 0; i < col_sz; ++i) {
1028 //const int v = vertex_worklist[i];
1029 const int v_new_color = col + col_sz - (neighbour_sizes.get(neighbours.get(v) + 1));
1030 // i could immediately determine size of v_new_color here and write invariant before rearrange?
1031 dej_assert(v_new_color >= col);
1032 dej_assert(v_new_color < col + col_sz);
1033
1034 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
1035 c->vertex_to_col[v] = v_new_color;
1036 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
1037 c->ptn[v_new_color] += 1;
1038 }
1039
1040 largest_color_class_size = -1;
1041 int largest_color_class = 0;
1042
1043 // determine largest class to throw away and finish
1044 for (i = col; i < col + col_sz;) {
1045 dej_assert(i >= 0 && i < c->domain_size);
1046 dej_assert(c->ptn[i] + 1 > 0);
1047 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
1048 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
1049 largest_color_class = new_largest? i : largest_color_class;
1050 if (i != 0) c->ptn[i - 1] = 0;
1051 i += c->ptn[i] + 1;
1052 }
1053 dej_assert(largest_color_class >= col);
1054 dej_assert(largest_color_class < col + col_sz);
1055
1056 // report splits
1057 for (i = col; i < col + col_sz;) {
1058 const int i_sz = c->ptn[i] + 1;
1059 report_split_color_class(c, col, i, i_sz, i == largest_color_class);
1060 i += i_sz;
1061 }
1062 }
1063
1064 neighbours.reset_hard();
1065 }
1066
1067 void refine_color_class_singleton(sgraph *g, coloring *c, int color_class) {
1068 int i, cc, deg1_write_pos, deg1_read_pos;
1069 cc = color_class; // iterate over color class
1070
1071 neighbours.reset();
1072 vertex_worklist.reset();
1073 old_color_classes.reset();
1074
1075 const int vc = c->lab[cc];
1076 const int pe = g->v[vc];
1077 const int deg= g->d[vc];
1078 const int end_i = pe + deg;
1079
1080 for (i = pe; i < end_i; i++) {
1081 const int v = g->e[i];
1082 const int col = c->vertex_to_col[v];
1083
1084 // singletons can not be split, so let's just ignore them
1085 if (c->ptn[col] == 0) continue;
1086
1087 if(neighbours.get(col) == -1) {
1088 old_color_classes.push_back(col);
1089 // neighbours acts as the write position for degree 1 vertices of col in the scratchpad
1090 neighbours.set(col, col);
1091 }
1092 // write vertex to scratchpad for later use
1093 scratch[neighbours.get(col)] = v;
1094 neighbours.inc_nr(col); // we reset neighbours later, use old_color_classes for reset
1095 }
1096
1097 /*
1098 // remove color classes from list if they don't split
1099 const int pre_size = old_color_classes.size();
1100 for(int j = 0; j < old_color_classes.size();) {
1101 const int deg0_col = old_color_classes[j];
1102 const int deg1_col_sz = neighbours.get(deg0_col) - deg0_col;
1103 const int deg0_col_sz = (c->ptn[deg0_col] + 1) - deg1_col_sz;
1104 const int deg1_col = deg0_col + deg0_col_sz;
1105
1106 if (deg0_col == deg1_col) {
1107 neighbours.set(deg1_col, -1);
1108 old_color_classes[j] = old_color_classes[old_color_classes.size() - 1];
1109 old_color_classes.pop_back();
1110 continue;
1111 }
1112
1113 ++j;
1114 }*/
1115
1116 old_color_classes.sort();
1117
1118 for(int j = 0; j < old_color_classes.cur_pos; ++j) {
1119 const int deg0_col = old_color_classes[j];
1120 const int deg1_col_sz = neighbours.get(deg0_col) - deg0_col;
1121 const int deg0_col_sz = (c->ptn[deg0_col] + 1) - deg1_col_sz;
1122 const int deg1_col = deg0_col + deg0_col_sz;
1123
1124 dej_assert(c->vertex_to_col[c->lab[deg0_col]] == deg0_col);
1125
1126 // no split? done...
1127 if (deg0_col == deg1_col) {
1128 neighbours.set(deg1_col, -1);
1129 dej_assert(c->vertex_to_col[c->lab[deg0_col]] == deg0_col);
1130 continue;
1131 }
1132
1133 dej_assert(deg0_col_sz + deg1_col_sz - 1 == c->ptn[deg0_col]);
1134
1135 // set ptn
1136 c->ptn[deg0_col] = deg0_col_sz - 1;
1137 c->ptn[deg1_col] = deg1_col_sz - 1;
1138 c->ptn[deg1_col - 1] = 0;
1139
1140 deg1_write_pos = deg1_col;
1141 deg1_read_pos = neighbours.get(deg0_col) - 1;
1142
1143 //c->vertex_to_col[c->lab[deg1_col]] = deg1_col;
1144
1145 // rearrange vertices of deg1 to the back of deg0 color
1146 dej_assert(deg1_read_pos >= deg0_col);
1147
1148 while (deg1_read_pos >= deg0_col) {
1149 const int v = scratch[deg1_read_pos];
1150 const int vertex_at_pos = c->lab[deg1_write_pos];
1151 const int lab_pos = c->vertex_to_lab[v];
1152
1153 c->lab[deg1_write_pos] = v;
1154 c->vertex_to_lab[v] = deg1_write_pos;
1155 c->vertex_to_col[v] = deg1_col;
1156
1157 c->lab[lab_pos] = vertex_at_pos;
1158 c->vertex_to_lab[vertex_at_pos] = lab_pos;
1159
1160 deg1_write_pos++;
1161 deg1_read_pos--;
1162 }
1163
1164 dej_assert(c->vertex_to_col[c->lab[deg0_col]] == deg0_col);
1165 dej_assert(c->vertex_to_col[c->lab[deg1_col]] == deg1_col);
1166
1167 // add new classes to report_splits
1168 const bool leq = deg1_col_sz > deg0_col_sz;
1169
1170 report_split_color_class(c, deg0_col, deg0_col, deg0_col_sz, !leq);
1171 report_split_color_class(c, deg0_col, deg1_col, deg1_col_sz, leq);
1172
1173 // reset neighbours count to -1
1174 neighbours.set(deg0_col, -1);
1175 }
1176
1177 old_color_classes.reset();
1178 }
1179
1180 void refine_color_class_singleton_first(sgraph *g, coloring *c, int color_class) {
1181 int i, cc, deg1_write_pos, deg1_read_pos;
1182 cc = color_class; // iterate over color class
1183
1184 neighbours.reset();
1185 scratch_set.reset();
1186 vertex_worklist.reset();
1187 old_color_classes.reset();
1188
1189 const int vc = c->lab[cc];
1190 const int pe = g->v[vc];
1191 const int end_i = pe + g->d[vc];
1192 for (i = pe; i < end_i; i++) {
1193 const int v = g->e[i];
1194 const int col = c->vertex_to_col[v];
1195
1196 if (c->ptn[col] == 0)
1197 continue;
1198
1199 if (!scratch_set.get(col)) {
1200 scratch_set.set(col);
1201 old_color_classes.push_back(col);
1202 // neighbours acts as the write position for degree 1 vertices of col
1203 // in the singleton scratchpad
1204 neighbours.set(col, col);
1205 }
1206 // write vertex to singleton scratchpad for later use
1207 scratch[neighbours.get(col)] = v;
1208 neighbours.inc_nr(col); // we reset neighbours later...
1209 // old_color_classes can be used as reset information
1210 }
1211
1212 for(int j = 0; j < old_color_classes.cur_pos; ++j) {
1213 const int deg0_col = old_color_classes[j];
1214 const int deg1_col_sz = neighbours.get(deg0_col) - deg0_col;
1215 const int deg0_col_sz = (c->ptn[deg0_col] + 1) - deg1_col_sz;
1216 const int deg1_col = deg0_col + deg0_col_sz;
1217
1218 // no split? done...
1219 if (deg0_col == deg1_col) {
1220 neighbours.set(deg1_col, -1);
1221 continue;
1222 }
1223
1224 // set ptn
1225 c->ptn[deg0_col] = deg0_col_sz - 1;
1226 c->ptn[deg1_col] = deg1_col_sz - 1;
1227 c->ptn[deg1_col - 1] = 0;
1228
1229 deg1_write_pos = deg1_col;
1230 deg1_read_pos = neighbours.get(deg0_col) - 1;
1231
1232 // rearrange vertices of deg1 to the back of deg0 color
1233 while (deg1_read_pos >= deg0_col) {
1234 const int v = scratch[deg1_read_pos];
1235 const int vertex_at_pos = c->lab[deg1_write_pos];
1236 const int lab_pos = c->vertex_to_lab[v];
1237
1238 c->lab[deg1_write_pos] = v;
1239 c->vertex_to_lab[v] = deg1_write_pos;
1240 c->vertex_to_col[v] = deg1_col;
1241 c->lab[lab_pos] = vertex_at_pos;
1242 c->vertex_to_lab[vertex_at_pos] = lab_pos;
1243
1244 deg1_write_pos++;
1245 deg1_read_pos--;
1246 }
1247
1248 // add new classes to report_splits
1249 const bool leq = deg1_col_sz > deg0_col_sz;
1250
1251 report_split_color_class_first(c, deg0_col, deg0_col, deg0_col_sz, !leq);
1252 report_split_color_class_first(c, deg0_col, deg1_col, deg1_col_sz, leq);
1253
1254 // reset neighbours count to -1
1255 neighbours.set(deg0_col, -1);
1256 }
1257
1258 old_color_classes.reset();
1259 }
1260
1261 void refine_color_class_dense_first(sgraph *g, coloring *c, int color_class, int class_size) {
1262 int i, cc, acc, largest_color_class_size, pos;
1263 cc = color_class; // iterate over color class
1264
1265 neighbours.reset();
1266 scratch_set.reset();
1267 old_color_classes.reset();
1268
1269 const int end_cc = color_class + class_size;
1270 while (cc < end_cc) { // increment value of neighbours of vc by 1
1271 const int vc = c->lab[cc];
1272 const int pe = g->v[vc];
1273 const int end_i = pe + g->d[vc];
1274
1275 for (i = pe; i < end_i; i++) {
1276 const int v = g->e[i];
1277 const int col = c->vertex_to_col[v];
1278 if (c->ptn[col] == 0)
1279 continue;
1280
1281 neighbours.inc(v);
1282 if (!scratch_set.get(col)) {
1283 scratch_set.set(col);
1284 old_color_classes.push_back(col);
1285 }
1286 }
1287 cc += 1;
1288 }
1289
1290 while (!old_color_classes.empty()) {
1291 const int col = old_color_classes.pop_back();
1292 const int col_sz = c->ptn[col] + 1;
1293
1294 if (col_sz == 1) {
1295 const int v_degree = neighbours.get(c->lab[col]) + 1;
1296 if (v_degree == -1)
1297 continue;
1298 }
1299
1300 neighbour_sizes.reset();
1301 vertex_worklist.reset();
1302
1303 const int first_index = neighbours.get(c->lab[col]) + 1;
1304 vertex_worklist.push_back(first_index);
1305 int total = 0;
1306 for (i = col; i < col + col_sz; ++i) {
1307 const int v = c->lab[i];
1308 const int index = neighbours.get(v) + 1;
1309 if (index == first_index)
1310 continue;
1311 total += 1;
1312 if (neighbour_sizes.inc(index) == 0)
1313 vertex_worklist.push_back(index);
1314 }
1315
1316 neighbour_sizes.inc(first_index);
1317 neighbour_sizes.set(first_index, col_sz - total - 1);
1318
1319 if (vertex_worklist.cur_pos == 1) {
1320 continue;
1321 }
1322
1323 // enrich neighbour_sizes to accumulative counting array
1324 acc = 0;
1325 while (!vertex_worklist.empty()) {
1326 const int k = vertex_worklist.pop_back();
1327 const int val = neighbour_sizes.get(k) + 1;
1328 if (val >= 1) {
1329 neighbour_sizes.set(k, val + acc);
1330 acc += val;
1331 const int _col = col + col_sz - (neighbour_sizes.get(k));
1332 c->ptn[_col] = -1; // this is val - 1, actually...
1333 }
1334 }
1335
1336 // copy cell for rearranging
1337 memcpy(scratch.get_array(), c->lab + col, col_sz * sizeof(int));
1338 pos = col_sz;
1339
1340 // determine colors and rearrange
1341 // split color classes according to count in counting array
1342 while (pos > 0) {
1343 const int v = scratch[--pos];
1344 const int v_new_color = col + col_sz - (neighbour_sizes.get(neighbours.get(v) + 1));
1345 // i could immediately determine size of v_new_color here and write invariant before rearrange?
1346 dej_assert(v_new_color >= col);
1347 dej_assert(v_new_color < col + col_sz);
1348
1349 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
1350 c->vertex_to_col[v] = v_new_color;
1351 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
1352 c->ptn[v_new_color] += 1;
1353 }
1354
1355 largest_color_class_size = -1;
1356 int largest_color_class = -1;
1357
1358 // determine largest class to throw away
1359 for (i = col; i < col + col_sz;) {
1360 dej_assert(i >= 0 && i < c->domain_size);
1361 dej_assert(c->ptn[i] + 1 > 0);
1362 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
1363 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
1364 largest_color_class = new_largest? i : largest_color_class;
1365 if (i != 0) c->ptn[i - 1] = 0;
1366 i += c->ptn[i] + 1;
1367 }
1368
1369 // report splits
1370 for (i = col; i < col + col_sz;) {
1371 const int i_sz = c->ptn[i] + 1;
1372 report_split_color_class_first(c, col, i, i_sz, i == largest_color_class);
1373 i += i_sz;
1374 }
1375 }
1376 }
1377
1378 void refine_color_class_dense_dense_first(sgraph *g, coloring *c, int color_class, int class_size) {
1379 // for all vertices of the color class...
1380 int i, j, cc, acc, largest_color_class_size, pos;
1381 cc = color_class; // iterate over color class
1382
1383 neighbours.reset();
1384 old_color_classes.reset();
1385
1386 const int end_cc = color_class + class_size;
1387 while (cc < end_cc) { // increment value of neighbours of vc by 1
1388 const int vc = c->lab[cc];
1389 const int pe = g->v[vc];
1390 const int end_i = pe + g->d[vc];
1391 for (i = pe; i < end_i; i++) {
1392 const int v = g->e[i];
1393 neighbours.inc_nr(v);
1394 }
1395 cc += 1;
1396 }
1397
1398 // dont sort, just iterate over all cells
1399 for (j = 0; j < g->v_size;) {
1400 const int col = j;
1401 const int c_ptn = c->ptn[j];
1402 j += c_ptn + 1;
1403 const int col_sz = c_ptn + 1;
1404
1405 if (col_sz == 1)
1406 continue;
1407
1408 neighbour_sizes.reset();
1409 vertex_worklist.reset();
1410
1411 const int first_index = neighbours.get(c->lab[col]) + 1;
1412 vertex_worklist.push_back(first_index);
1413 int total = 0;
1414 for (i = col; i < col + col_sz; ++i) {
1415 const int v = c->lab[i];
1416 const int index = neighbours.get(v) + 1;
1417 if (index == first_index)
1418 continue;
1419 total += 1;
1420 if (neighbour_sizes.inc(index) == 0)
1421 vertex_worklist.push_back(index);
1422 }
1423
1424 neighbour_sizes.inc(first_index);
1425 neighbour_sizes.set(first_index, col_sz - total - 1);
1426
1427 if (vertex_worklist.cur_pos == 1) {
1428 continue;
1429 }
1430
1431 // enrich neighbour_sizes to accumulative counting array
1432 acc = 0;
1433 while (!vertex_worklist.empty()) {
1434 const int k = vertex_worklist.pop_back();
1435 const int val = neighbour_sizes.get(k) + 1;
1436 if (val >= 1) {
1437 neighbour_sizes.set(k, val + acc);
1438 acc += val;
1439 const int _col = col + col_sz - (neighbour_sizes.get(k));
1440 c->ptn[_col] = -1;
1441 }
1442 }
1443
1444 // copy cell for rearranging
1445 memcpy(scratch.get_array(), c->lab + col, col_sz * sizeof(int));
1446 pos = col_sz;
1447
1448 // determine colors and rearrange
1449 // split color classes according to count in counting array
1450 while (pos > 0) {
1451 const int v = scratch[--pos];
1452 const int v_new_color = col + col_sz - (neighbour_sizes.get(neighbours.get(v) + 1));
1453 dej_assert(v_new_color >= col);
1454 dej_assert(v_new_color < col + col_sz);
1455
1456 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
1457 c->vertex_to_col[v] = v_new_color;
1458 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
1459 c->ptn[v_new_color] += 1;
1460 }
1461
1462 largest_color_class_size = -1;
1463 int largest_color_class = 0;
1464
1465 // determine largest class to throw away and finish
1466 for (i = col; i < col + col_sz;) {
1467 dej_assert(i >= 0 && i < c->domain_size);
1468 dej_assert(c->ptn[i] + 1 > 0);
1469 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
1470 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
1471 largest_color_class = new_largest? i : largest_color_class;
1472 if (i != 0) c->ptn[i - 1] = 0;
1473 i += c->ptn[i] + 1;
1474 }
1475
1476 // report splits
1477 for (i = col; i < col + col_sz;) {
1478 const int i_sz = c->ptn[i] + 1;
1479 report_split_color_class_first(c, col, i, i_sz, i == largest_color_class);
1480 i += i_sz;
1481 }
1482 }
1483
1484 neighbours.reset_hard();
1485 }
1486
1487 // distance heuristic inspired by the heuristic of nauty
1488 /*void refine_color_class_singleton_distance_first(sgraph *g, coloring *c, int color_class) {
1489 // for all vertices of the color class...
1490
1491 // worklist arrays
1492 vertex_worklist.reset();
1493 color_vertices_considered.reset();
1494 neighbours.reset(); // storing distances here
1495 neighbour_sizes.reset();
1496
1497 // origin of breadth-first search
1498 const int v = c->lab[color_class];
1499 vertex_worklist.push_back(v);
1500 neighbours.set(v, 0);
1501 neighbour_sizes.set(v, 0);
1502
1503 // breadth-first search through graph to determine distances
1504 for(int j = 0; j < vertex_worklist.size(); ++j) {
1505 const int v_current = vertex_worklist[j];
1506 const int v_current_col = c->vertex_to_col[v_current];
1507 color_vertices_considered.set(v_current, 1);
1508 const int hash_current = neighbours.get(v_current);
1509 const int dis_current = neighbour_sizes.get(v_current);
1510 const int pe = g->v[v_current];
1511 const int end_i = pe + g->d[v_current];
1512
1513 for (int i = pe; i < end_i; i++) {
1514 const int v_next = g->e[i];
1515 const int state = color_vertices_considered.get(v_next);
1516 if(state == -1) {
1517 color_vertices_considered.set(v_next, 0);
1518 vertex_worklist.push_back(v_next);
1519 neighbours.set(v_next, hash_current + 1);
1520 neighbour_sizes.set(v_next, dis_current + 1);
1521 }
1522
1523 const int dis_next = neighbour_sizes.get(v_next);
1524 if(dis_current != dis_next) {
1525 neighbours.set(v_next, neighbours.get(v_next) + v_current_col + hash_current + dis_current);
1526 }
1527 }
1528 }
1529
1530 neighbour_sizes.reset_hard();
1531
1532 for(int j = 0; j < g->v_size; j += 1) {
1533 neighbours.set(j, abs(neighbours.get(j)) % g->v_size);
1534 dej_assert(neighbours.get(j) >= 0);
1535 }
1536
1537 // iterate all cells
1538 for (int j = 0; j < g->v_size;) {
1539 const int col = j;
1540 const int c_ptn = c->ptn[j];
1541 j += c_ptn + 1;
1542 const int col_sz = c_ptn + 1;
1543
1544 if (col_sz == 1) continue;
1545
1546 neighbour_sizes.reset();
1547 vertex_worklist.reset();
1548
1549 const int first_index = neighbours.get(c->lab[col]);
1550 vertex_worklist.push_back(first_index);
1551 int total = 0;
1552 for (int i = col; i < col + col_sz; ++i) {
1553 const int v = c->lab[i];
1554 const int index = neighbours.get(v);
1555 if (index == first_index) continue;
1556 total += 1;
1557 if (neighbour_sizes.inc(index) == 0) vertex_worklist.push_back(index);
1558 }
1559
1560 neighbour_sizes.inc(first_index);
1561 neighbour_sizes.set(first_index, col_sz - total - 1);
1562
1563 if (vertex_worklist.cur_pos == 1) continue;
1564
1565 // enrich neighbour_sizes to accumulative counting array
1566 int acc = 0;
1567 while (!vertex_worklist.empty()) {
1568 const int k = vertex_worklist.pop_back();
1569 const int val = neighbour_sizes.get(k) + 1;
1570 if (val >= 1) {
1571 neighbour_sizes.set(k, val + acc);
1572 acc += val;
1573 const int _col = col + col_sz - (neighbour_sizes.get(k));
1574 c->ptn[_col] = -1;
1575 }
1576 }
1577
1578 // copy cell for rearranging
1579 memcpy(scratch.get_array(), c->lab + col, col_sz * sizeof(int));
1580 int pos = col_sz;
1581
1582 // determine colors and rearrange
1583 // split color classes according to count in counting array
1584 while (pos > 0) {
1585 const int v = scratch[--pos];
1586 const int v_new_color = col + col_sz - neighbour_sizes.get(neighbours.get(v));
1587 dej_assert(v_new_color >= col);
1588 dej_assert(v_new_color < col + col_sz);
1589
1590 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
1591 c->vertex_to_col[v] = v_new_color;
1592 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
1593 c->ptn[v_new_color] += 1;
1594 }
1595
1596 int largest_color_class_size = -1;
1597 int largest_color_class = 0;
1598
1599 // determine largest class to throw away and finish
1600 for (int i = col; i < col + col_sz;) {
1601 dej_assert(i >= 0 && i < c->domain_size);
1602 dej_assert(c->ptn[i] + 1 > 0);
1603 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
1604 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
1605 largest_color_class = new_largest? i : largest_color_class;
1606 if (i != 0) c->ptn[i - 1] = 0;
1607 i += c->ptn[i] + 1;
1608 }
1609
1610 // report splits
1611 for (int i = col; i < col + col_sz;) {
1612 const int i_sz = c->ptn[i] + 1;
1613 report_split_color_class_first(c, col, i, i_sz, i == largest_color_class);
1614 i += i_sz;
1615 }
1616 }
1617
1618 neighbours.reset_hard();
1619 color_vertices_considered.reset_hard();
1620 }*/
1621
1622 // distance heuristic inspired by the heuristic of nauty
1623 /*void refine_color_class_singleton_distance(sgraph *g, coloring *c, int color_class) {
1624 // for all vertices of the color class...
1625
1626 // worklist arrays
1627 vertex_worklist.reset();
1628 color_vertices_considered.reset();
1629 neighbours.reset(); // storing distances here
1630 neighbour_sizes.reset();
1631
1632 // origin of breadth-first search
1633 const int v = c->lab[color_class];
1634 vertex_worklist.push_back(v);
1635 neighbours.set(v, 0);
1636 neighbour_sizes.set(v, 0);
1637
1638 // breadth-first search through graph to determine distances
1639 for(int j = 0; j < vertex_worklist.size(); ++j) {
1640 const int v_current = vertex_worklist[j];
1641 const int v_current_col = c->vertex_to_col[v_current];
1642 color_vertices_considered.set(v_current, 1);
1643 const int hash_current = neighbours.get(v_current);
1644 const int dis_current = neighbour_sizes.get(v_current);
1645 const int pe = g->v[v_current];
1646 const int end_i = pe + g->d[v_current];
1647
1648 for (int i = pe; i < end_i; i++) {
1649 const int v_next = g->e[i];
1650 const int state = color_vertices_considered.get(v_next);
1651 if(state == -1) {
1652 color_vertices_considered.set(v_next, 0);
1653 vertex_worklist.push_back(v_next);
1654 neighbours.set(v_next, hash_current + 1);
1655 neighbour_sizes.set(v_next, dis_current + 1);
1656 }
1657
1658 const int dis_next = neighbour_sizes.get(v_next);
1659 if(dis_current != dis_next) {
1660 neighbours.set(v_next, neighbours.get(v_next) + v_current_col + hash_current + dis_current);
1661 }
1662 }
1663 }
1664
1665 neighbour_sizes.reset_hard();
1666
1667 for(int j = 0; j < g->v_size; j += 1) {
1668 neighbours.set(j, abs(neighbours.get(j)) % g->v_size);
1669 dej_assert(neighbours.get(j) >= 0);
1670 }
1671
1672 // iterate all cells
1673 for (int j = 0; j < g->v_size;) {
1674 const int col = j;
1675 const int c_ptn = c->ptn[j];
1676 j += c_ptn + 1;
1677 const int col_sz = c_ptn + 1;
1678
1679 if (col_sz == 1) continue;
1680
1681 neighbour_sizes.reset();
1682 vertex_worklist.reset();
1683
1684 const int first_index = neighbours.get(c->lab[col]);
1685 vertex_worklist.push_back(first_index);
1686 int total = 0;
1687 for (int i = col; i < col + col_sz; ++i) {
1688 const int v = c->lab[i];
1689 const int index = neighbours.get(v);
1690 if (index == first_index) continue;
1691 total += 1;
1692 if (neighbour_sizes.inc(index) == 0) vertex_worklist.push_back(index);
1693 }
1694
1695 neighbour_sizes.inc(first_index);
1696 neighbour_sizes.set(first_index, col_sz - total - 1);
1697
1698 if (vertex_worklist.cur_pos == 1) continue;
1699
1700 // enrich neighbour_sizes to accumulative counting array
1701 int acc = 0;
1702 while (!vertex_worklist.empty()) {
1703 const int k = vertex_worklist.pop_back();
1704 const int val = neighbour_sizes.get(k) + 1;
1705 if (val >= 1) {
1706 neighbour_sizes.set(k, val + acc);
1707 acc += val;
1708 const int _col = col + col_sz - (neighbour_sizes.get(k));
1709 c->ptn[_col] = -1;
1710 }
1711 }
1712
1713 // copy cell for rearranging
1714 memcpy(scratch.get_array(), c->lab + col, col_sz * sizeof(int));
1715 int pos = col_sz;
1716
1717 // determine colors and rearrange
1718 // split color classes according to count in counting array
1719 while (pos > 0) {
1720 const int v = scratch[--pos];
1721 const int v_new_color = col + col_sz - neighbour_sizes.get(neighbours.get(v));
1722 dej_assert(v_new_color >= col);
1723 dej_assert(v_new_color < col + col_sz);
1724
1725 c->lab[v_new_color + c->ptn[v_new_color] + 1] = v;
1726 c->vertex_to_col[v] = v_new_color;
1727 c->vertex_to_lab[v] = v_new_color + c->ptn[v_new_color] + 1;
1728 c->ptn[v_new_color] += 1;
1729 }
1730
1731 int largest_color_class_size = -1;
1732 int largest_color_class = 0;
1733
1734 // determine largest class to throw away and finish
1735 for (int i = col; i < col + col_sz;) {
1736 dej_assert(i >= 0 && i < c->domain_size);
1737 dej_assert(c->ptn[i] + 1 > 0);
1738 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
1739 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
1740 largest_color_class = new_largest? i : largest_color_class;
1741 if (i != 0) c->ptn[i - 1] = 0;
1742 i += c->ptn[i] + 1;
1743 }
1744
1745 // report splits
1746 for (int i = col; i < col + col_sz;) {
1747 const int i_sz = c->ptn[i] + 1;
1748 report_split_color_class(c, col, i, i_sz, i == largest_color_class);
1749 i += i_sz;
1750 }
1751 }
1752
1753 neighbours.reset_hard();
1754 color_vertices_considered.reset_hard();
1755 }*/
1756
1757 void refine_color_class_sparse_first(sgraph *g, coloring *c, int color_class, int class_size) {
1758 int v_new_color, cc, largest_color_class_size, acc;
1759 cc = color_class; // iterate over color class
1760
1761 scratch_set.reset();
1762 old_color_classes.reset();
1763 neighbours.reset();
1764 color_vertices_considered.reset();
1765
1766 const int end_cc = color_class + class_size;
1767 while (cc < end_cc) { // increment value of neighbours of vc by 1
1768 const int vc = c->lab[cc];
1769 const int pe = g->v[vc];
1770 const int end_i = pe + g->d[vc];
1771 for (int i = pe; i < end_i; i++) {
1772 const int v = g->e[i];
1773 const int col = c->vertex_to_col[v];
1774
1775 if (c->ptn[col] == 0)
1776 continue;
1777
1778 neighbours.inc_nr(v);
1779 if (neighbours.get(v) == 0) {
1780 color_vertices_considered.inc_nr(col);
1781 dej_assert(col + color_vertices_considered.get(col) < g->v_size);
1782 scratch[col + color_vertices_considered.get(col)] = v; // hit vertices
1783 if (!scratch_set.get(col)) {
1784 old_color_classes.push_back(col);
1785 scratch_set.set(col);
1786 }
1787 }
1788 }
1789 cc += 1;
1790 }
1791
1792 // split color classes according to neighbour count
1793 while (!old_color_classes.empty()) {
1794 const int _col = old_color_classes.pop_back();
1795 const int _col_sz = c->ptn[_col] + 1;
1796
1797 neighbour_sizes.reset();
1798 vertex_worklist.reset();
1799
1800 for (int i = 0; i < color_vertices_considered.get(_col) + 1; ++i) {
1801 const int v = scratch[_col + i];
1802 int index = neighbours.get(v) + 1;
1803 if (neighbour_sizes.inc(index) == 0)
1804 vertex_worklist.push_back(index);
1805 }
1806
1807 // enrich neighbour_sizes to accumulative counting array
1808 acc = 0;
1809 while (!vertex_worklist.empty()) {
1810 const int i = vertex_worklist.pop_back();
1811 const int val = neighbour_sizes.get(i) + 1;
1812 if (val >= 1) {
1813 neighbour_sizes.set(i, val + acc);
1814 acc += val;
1815 }
1816 }
1817
1818 // determine colors
1819 vertex_worklist.reset();
1820
1821 for (int i = 0; i < color_vertices_considered.get(_col) + 1; ++i) {
1822 const int v = scratch[_col + i];
1823 if (neighbours.get(v) == -1) {
1824 v_new_color = _col;
1825 dej_assert(false);
1826 } else {
1827 dej_assert((neighbours.get(v) + 1) > 0);
1828 v_new_color = _col + _col_sz - neighbour_sizes.get(neighbours.get(v) + 1);
1829 }
1830 if (v_new_color != _col) {
1831 vertex_worklist.push_back(v_new_color);
1832 vertex_worklist.push_back(v);
1833 c->ptn[v_new_color] = -1;
1834 }
1835 neighbours.set(v, -1);
1836 }
1837
1838 color_vertices_considered.set(_col, -1);
1839
1840 // rearrange vertices
1841 while (!vertex_worklist.empty()) {
1842 const int v = vertex_worklist.pop_back();
1843 const int v_new_color2 = vertex_worklist.pop_back();
1844
1845 const int vertex_old_pos = c->vertex_to_lab[v];
1846 const int vertex_at_pos = c->lab[v_new_color2 + c->ptn[v_new_color2] + 1];
1847 c->lab[vertex_old_pos] = vertex_at_pos;
1848 c->vertex_to_lab[vertex_at_pos] = vertex_old_pos;
1849
1850 c->lab[v_new_color2 + c->ptn[v_new_color2] + 1] = v;
1851 c->vertex_to_col[v] = v_new_color2;
1852 c->vertex_to_lab[v] = v_new_color2 + c->ptn[v_new_color2] + 1;
1853 c->ptn[v_new_color2] += 1;
1854
1855 if (_col != v_new_color2) {
1856 dej_assert(v_new_color2 > _col);
1857 c->ptn[_col] -= 1;
1858 } else
1859 dej_assert(false);
1860 }
1861
1862 // add new colors to worklist
1863 largest_color_class_size = -1;
1864 int largest_color_class = -1;
1865 int i;
1866 for (i = _col; i < _col + _col_sz;) {
1867 dej_assert(i >= 0 && i < c->domain_size);
1868 dej_assert(c->ptn[i] + 1 > 0);
1869 const bool new_largest = largest_color_class_size < (c->ptn[i] + 1);
1870 largest_color_class_size = new_largest? (c->ptn[i] + 1) : largest_color_class_size;
1871 largest_color_class = new_largest? i : largest_color_class;
1872 if (i != 0) c->ptn[i - 1] = 0;
1873 i += c->ptn[i] + 1;
1874 }
1875 if (i != 0) c->ptn[i - 1] = 0;
1876
1877
1878 for (i = _col; i < _col + _col_sz;) {
1879 const int i_sz = c->ptn[i] + 1;
1880 report_split_color_class_first(c, _col, i, i_sz, i == largest_color_class);
1881 i += i_sz;
1882 }
1883 }
1884
1885 neighbour_sizes.reset();
1886 vertex_worklist.reset();
1887 }
1888 };
1889 }
1890}
1891
1892#endif //DEJAVU_REFINEMENT_H
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 set(int pos)
Definition: ds.h:616
void unset(int pos)
Definition: ds.h:626
void push_back(T value)
Definition: ds.h:177
T get(int index)
Definition: ds.h:499
void initialize(int size)
Definition: ds.h:483
Certifies automorphisms.
Definition: refinement.h:24
static bool certify_automorphism_sparse(markset &scratch_set, const sgraph *g, const int *p, int supp, const int *supp_arr)
Definition: refinement.h:88
static bool certify_automorphism(markset &scratch_set, sgraph *g, const int *p)
Definition: refinement.h:55
Color refinement and related algorithms.
Definition: refinement.h:143
bool certify_automorphism(sgraph *g, const int *p)
Definition: refinement.h:362
static int individualize_vertex(coloring *c, int v, const std::function< type_split_color_hook > &split_hook=nullptr)
Definition: refinement.h:245
void refine_coloring_first(sgraph *g, coloring *c, int init_color_class=-1)
Definition: refinement.h:284
bool certify_automorphism_sparse(const sgraph *g, const int *p, int supp, const int *supp_arr)
Definition: refinement.h:379
void refine_coloring(sgraph *g, coloring *c, int init_color=-1, int color_limit=-1, const std::function< type_split_color_hook > *split_hook=nullptr, const std::function< type_worklist_color_hook > *worklist_hook=nullptr)
Definition: refinement.h:161
Internal graph data structure.
Definition: graph.h:19
int * e
Definition: graph.h:46
int v_size
Definition: graph.h:48
int * v
Definition: graph.h:44
bool dense
Definition: graph.h:51
int * d
Definition: graph.h:45
workset_t< int > work_set_int
Definition: ds.h:539
bool type_worklist_color_hook(const int, const int)
Definition: refinement.h:134
bool type_split_color_hook(const int, const int, const int)
Definition: refinement.h:130
Definition: bfs.h:10
#define dej_assert(expr)
Definition: utility.h:40
#define dej_nodiscard
Definition: utility.h:46