Error & Certification

We discuss in detail how symmetries are certified in dejavu, and how certification can be made more thorough if so desired.

Error? Certification? #

The underlying algorithm of dejavu is a randomized algorithm: a Monte Carlo algorithm with bounded error. The user may set a likelihood for error, e.g., the default is \( \epsilon \leq 0.001 \), and the algorithm may only err in a given run with probability \( \epsilon \).

More specifically, the error in dejavu is one-sided, meaning the solver may miss some symmetries, but it will never report permutations that are not symmetries of the graph. Crucially, for almost all applications that we know of, this kind of error does indeed not matter for correctness. Note that in practice, the error probability of course also depends on the quality of the employed random number generator. Options for random number generation and error probability are available through the class solver:

// let's say we have some graph
dejavu::static_graph g;

// ...

dejavu::solver d;
d.set_error_bound(10)
d.automorphisms(&g);

The set_error_bound(e) method sets the error to be at most \( 1/2^e \), assuming uniform random numbers. There are more options: the method set_seed which can be used to set a seed for pseudo random numbers used in the solver, whereas set_true_random attempts to use a random device as provided by the operating system.

Moreover, dejavu certifies its results, meaning for a permutation \( \varphi \) reported as a symmetry, the test \( \varphi(G) = G \) – with some caveats – is performed. The limitations of the certification itself are discussed below.

Limitations #

Some limitations apply to the certification.

Non-isomorphism #

First of all, there are no certificates for non-isomorphism. Hence, we may not certify whether the graph actually contains more symmetries than stated. Note that this is precisely the case in which dejavu has one-sided bounded error: the solver may miss symmetries.

Preprocessed Graphs #

Secondly, dejavu preprocesses the graph, i.e., it removes vertices of low degree and other simple structures from the graphs (see our page on the preprocessor). The main solver in turn only certifies generators on the smaller, already preprocessed graph. In a way, this means that the preprocessor itself is part of the trusted code base. This reliance can however be mitigated, as is described below.

Strong Certification #

If a more thorough certification is desired, it is possible to use the strong certification flag to certify all the generators on the original graph. The solver makes a copy of the original graph, and only returns generators which pass certification on that graph.

// let's say we have some graph
dejavu::static_graph g;

// ...

// let's say we want to call the orbit_hook below
dejavu::groups::orbit orbits(n);
dejavu::hooks::orbit_hook hook(orbits);

// create the solver object
dejavu::solver d;

// set strong certification
d.set_strong_certification();

// call the solver
d.automorphisms(&g, hook.get_hook());

// all generators are now certified on the original graph, and only 
// if they pass certification, hook1 is called