Haydi: Rapid Prototyping and Combinatorial Objects
Stanislav Böhm Jakub Beránek Martin Šurkovský


Finite tidal effects in GW170817: Observational evidence or model assumptions?
    F. Ohme
    September 2019; updated September 2020
==============================================================================




	 (http://haydi.readthedocs.io) is a framework for generating discrete structures. It provides a way to define a structure from basic building blocks and then enumerate all elements, all non-isomorphic elements, or generate random elements in the structure.  is designed as a tool for rapid prototyping. It is implemented as a pure Python package and supports execution in distributed environments. The goal of this paper is to give the overall picture of Haydi together with a formal definition for the case of generating canonical forms.



	combinatorial objects, rapid prototyping, canonical representation




§ INTRODUCTION


The concept of rapid prototyping helps in verifying the feasibility of an initial idea and reject the bad ones fast. In mathematical world, there are tools like Matlab, SageMath, or R that allow one to build a working prototype and evaluate an idea quickly.
This paper is focused on the field of combinatorial objects and provides a prototyping tool
that allows to check claims on small instances by search over relevant objects.  (Haystack Diver) is an open-source Python package that provides an easy way of describing such structures by composing basic building blocks (e.g. Cartesian product, mappings) and then enumerating all elements, all non-isomorphic elements, or generating random elements.

The main design goal is to build a tool that is simple to use, since building prototypes have to be cheap and fast.
There has been an attempt to build a flexible tool that describes various structures and reduces limitations for the user.
The reasonable performance of the solution is also important, but it has a lower priority than the first two goals.

To fulfill these goals,  has been built as a Python package.
Python is a well-known programming language and is commonly used as a prototyping language that provides a high degree of flexibility.
Since  is written purely in Python, it is compatible with PyPyhttps://pypy.org/ – a fast Python implementation with JIT compiler.
Moreover,  is designed to transparently utilize a cluster of computers to provide a better performance without sacrificing simplicity or flexibility.
The distributed execution is built over Dask/distributedhttps://github.com/dask/distributed and it was tested on Salomon clusterhttps://docs.it4i.cz/salomon/introduction/. 

The goal of this paper is to give the overall picture of  together with
a formal definition for the case of generating canonical forms.
More detailed and programmer-oriented text can be found in the user guidehttp://haydi.readthedocs.io/.
 is released as an open source project at <https://github.com/spirali/haydi> under MIT license.

The original motivation for the tool was to investigate hard instances for equivalence of deterministic push-down automata (DPDAs).
We have released a data set containing non-equivalent normed DPDAs <cit.>.  


The paper starts with two motivation examples in Section <ref> followed by covering related works in Section <ref>.
Section <ref> introduces the architecture of . Section <ref> shows a theoretical framework for generating canonical forms.
Section <ref> covers a basic usage of distributed computations and used optimizations. The last section shows performance measurements. 




§ EXAMPLES


To give an impression of how  works, basic usage of  is
demonstrated on two examples.
The first one is a generator for directed graphs and the second one
is a generator of finite state automata for the reset word problem.



 §.§ Example: Directed graphs


In this example, our goal is to generate directed graphs with n nodes.
Our first task is to describe the structure itself: we represent a graph as a set of edges,
where an edge is a pair of two (possibly the same) nodes. For the simplicity of outputs,
we are going to generate graphs on two nodes. However, this can be simply changed by editing a single constant,
namely the number 2 on the second line in following code:

python
>>> import haydi as hd
>>> nodes = hd.USet(2, "n")  # A two-element set with elements n0, n1
>>> graphs = hd.Subsets(nodes * nodes)  # Subsets of a cartesian product


The first line just imports  package. The second one creates a set of nodes, namely a set of two “unlabeled” elements.
The first argument is the number of elements, the second one is the prefix of each element name.
The exact meaning of USet will be discussed further in the paper.
For now, it just creates a
set with elements without any additional quality, the elements of this set can
be freely relabeled. In this example, it provides us with the standard graph isomorphism.
The third line constructs a collection of all graphs on two nodes, 
in a mathematical notation it could be written as “𝗀𝗋𝖺𝗉𝗁𝗌 = 𝒫(𝗇𝗈𝖽𝖾𝗌×𝗇𝗈𝖽𝖾𝗌)”.

With this definition, we can now iterate all graphs:

python
>>> list(graphs.iterate())
[, (n0, n0), (n0, n0), (n0, n1), (n0, n0), (n0, n1), (n1, n0),
# ... 3 lines removed ...
n1), (n1, n0), (n1, n0), (n1, n1), (n1, n1)]


or iterate in a way in which we can see only one graph per isomorphic class:

python
>>> list(graphs.cnfs())  # cnfs = canonical forms
[, (n0, n0), (n0, n0), (n1, n1), (n0, n0), (n0, n1),
(n0, n0), (n0, n1), (n1, n1), (n0, n0), (n0, n1), (n1, n0),
(n0, n0), (n0, n1), (n1, n0), (n1, n1), (n0, n0), (n1, n0),
(n0, n1), (n0, n1), (n1, n0)]


or generate random instances (3 instances in this case):

python
>>> list(graphs.generate(3))
[(n1, n0), (n1, n1), (n0, n0), (n0, n1), (n1, n0)]


 supports standard operations such as map, filter, and reduce.
The following example shows how to define graphs without loops, i.e. graphs such that for all edges (a, b) hold that a ≠ b:

python
>>> no_loops = graphs.filter(lambda g: all(a!=b for (a,b) in g.to_set()))


All these constructions can be transparently evaluated as a pipeline distributed across a cluster.
 uses Dask/distributed for distributing tasks, the following code assumes that dask/distributed server
runs at :

python
# Initialization
>>> from haydi import DistributedContext
>>> context = DistributedContext("hostname", 1234)

# Run a pipeline
>>> graphs.iterate().run(ctx=context)





 §.§ Example: Reset words



A reset word is a word that sends all states of a given finite automaton to a unique state.
The following example generates automata and computes the length of a minimal reset word.
It can be used for verifying the Černý conjecture on bounded instances.
The conjecture states that the length of a minimal reset word is bounded by (n-1)^2 where n is the number of states of the automaton <cit.>.

First, we describe deterministic automata by their transition functions (a mapping from a pair of state and symbol to a new state).
In the following code,  is the number of states and  is the size of the alphabet.
We use  even for the alphabet, since we do not care about the meaning of particular symbols, we just need to distinguish them.

python
# set of states q0, q1, ..., q_n_states-1
>>> states = hd.USet(n_states, "q")
# set of symbols a0, ..., a_a_symbols-1
>>> alphabet = hd.USet(n_symbols, "a")

# All mappings (states * alphabet) -> states
>>> delta = hd.Mappings(states * alphabet, states)


Now we can create a pipeline that goes through all the automata of the given size (one per an isomorphic class) and finds the maximal length among minimal reset words:

python
>>> pipeline = delta.cnfs().map(check_automaton).max(size=1)
>>> result = pipeline.run()

>>> print ("The maximal length of a minimal reset word for an "
...        "automaton with  states and  symbols is .".
...        format(n_states, n_symbols, result[0]))



The function  takes an automaton (as a transition function) and returns the length of the minimal reset word, or 0 when there is no such a word. It is just a simple breadth-first search on sets of states. The function is listed in Appendix <ref>.



§ RELATED WORKS


Many complex software frameworks are designed for rapid checking mathematical ideas, for example Maple, Matlab, SageMath.
Most of them also contain a package for combinatorial structures, e.g. Combinatorics in SageMathhttp://doc.sagemath.org/html/en/reference/combinat/sage/combinat/tutorial.html,
combstruct in Maplehttps://www.maplesoft.com/support/help/Maple/view.aspx?path=combstruct.

From the perspective of the mentioned tools,  is a small single-purpose package.
But as far as we know, there is no other tool that allows building structures by composition, searching only one structure of each isomorphism class as well as offering simple execution in distributed environment.

Tools focused on the generation of specific structures are on the other side of
the spectrum.
One example is Nauty <cit.> that contains Geng
for generating graphs, another ones are generators for parity games in PGSolver <cit.> or automata generator for SageMath <cit.>. These tools provide highly optimized generators for a given structure.



§ ARCHITECTURE


 is a Python package for rapid prototyping of generators for discrete structures. 
The main two components are domains and pipelines.
The former is dedicated to defining structures and the latter executes an operation over domains.
In this section, both domains and pipelines are introduced. Parts that are
related to generating canonical forms are omitted. This is covered separately in Section <ref>.



 §.§ Domains


The basic structure in  is a domain that represents an unordered collection of (Python) objects.
On abstract level, domains can be viewed as countable sets with some implementation details.
The basic operations with the domains are iterations through their elements and generating a random element. 
Domains are composable, i.e., more complex domains can be created from simpler ones.

There are six elementary domains: Range (a range of integers), Values (a domain of explicitly listed Python objects), Boolean (a domain containing  and ), and NoneDomain (a domain containing only one element: ). Examples are shown in Figure <ref>.
There are also domains  and ; their description is
postponed to Section <ref>, since it is necessary to develop a theory to explain their purpose.




New domains can be created by composing existing ones or applying a transformation. There are the following compositions: 
Cartesian product, sequences, subsets, mappings, and join. Examples are shown in Figure <ref>, more details can be found in the user guide. There are two transformations map and filter with the standard meaning. Examples are shown 
in Figure <ref>.








 §.§ Pipeline


Domains in the previous section describe a set of elements.
Pipelines provide a way how to work with elements in these sets.
Generally, a pipeline provides methods for generating and iterating elements and optionally 
applying simple “map & reduce” transformations.  

The pipeline creates a stream of elements from a domain by one of the three methods.
We can apply transformations on elements in the stream. The pipeline ends by a reducing action.
The schema is shown in Figure <ref>. The pipeline consists of:











 
Method  It specifies how to take elements from the domain into the stream. Haydi provides three options: , , and .
Method
  iterates all elements of a given domain,  creates n random elements of the domain (by default with the uniform distribution over all elements),
and  iterates over canonical forms (Section <ref>).

Transformations  Transformation modifies/filters elements in a stream.
 There are three pipeline transformations:
 – applies the function  on each element that goes through the pipeline,
 – filters elements in the pipeline according to the provided function,
 – takes only first  elements from the stream. 
The reason why transformations on domains and in pipeline are distinguished is described in <https://haydi.readthedocs.io/en/latest/pipeline.html#transformations>.

Actions  Action is a final operation on a stream of elements. 
For example there are:  – creates a list form of the stream,
 – applies binary operation on elements of the stream,
 – takes maximal elements in the stream.

run()  The previous operations declare the pipeline, which is an immutable representation of a computational graph. The  method actually executes the pipeline. The optional  (context) parameter specifies how should the computation be performed (serially or in a distributed way on a cluster).


The examples of pipelines are shown in Figure <ref>.
Not all parts of a pipeline have to be specified, if some of them are missing, defaults are used; the default method is 
and the default action is .






§ GENERATING CANONICAL FORMS


In many cases, when we want to verify a property of a discrete structure, 
we are not interested in the names of the elements in the structure.
For example, in the case of graphs we usually want to see only one graph for each isomorphic class.
Another example can be finite-state automata; in many cases we are not especially interested in names of states
and actual symbols in the input alphabet. For example, in Černý conjecture, the minimal length of reset words is not changed when the alphabet 
is permuted. On the other hand, symbols in some other problems may have special meanings and we cannot freely interchange them.

 introduces  as a simple but expressive mechanism for describing what permutations we are interested in.
It serves to define partitions of atomic objects. Each partition creates a
set of atomic objects that can be freely interchanged with one another; 
we call these partitions Unlabeled sets.
They then establish semantics to what structure should be preserved when isomorphisms on various structures are defined.

 allows to iterate a domain in a way where we see only one element for
each isomorphic class. It is implemented as an iteration through canonical forms (CNFS).

In this section, a simple theoretical framework is built. It gives a formal background to this feature.
Paragraphs starting with “Abstract:” are meant as part of a theoretical description. 
Paragraphs starting with “Haydi:” describe the implementation of the framework in . 

Abstract:
Let  be a set of all atomic objects whose structure is not investigated any further.
The set of objects  is the minimal set with the following properties:



  * ⊆   (atoms)

  * If o_i ∈ for i ∈{1, 2, …, n } then {o_1, o_2, …, o_n}∈   (finite sets)

  * If o_i ∈ for i ∈{1, 2, …, n } then (o_1, o_2, …, o_n) ∈   (finite sequences)


It is assumed that type of each object (atom, sequence, and set) can always be determined.
Therefore, it is assumed that sequences and sets are not contained in atoms. 

Function : → 2^ that returns the atoms
contained in an object is defined as follows:


	
  * (o) = {o} if o ∈
	
  * (o) = ⋃_i ∈{ 1, …, n }(o_i) if 
	o = {o_1, …, o_n} or o = (o_1, …, o_n)


:
The used Python instantiation of the definitions is the following:  contains , , , all instances of types  (integers) and  (strings) and instances of the class .
Except for the last one, they are Python built-in objects; the last one is related to unlabeled sets and will be explained later.
Sequences in  are identified with Python tuples, sets with  (analogous to standard ).
 also contains the type  (analogous to ) for
mappings. In the theoretical framework, mappings were not explicitly
distinguished, as they can be considered sets of pairs.
For sets and maps, standard python objects are not directly used for performance reasons[
Built-in classes  and  are optimized for lookups;
however, Haydi needs fast comparison methods as will be seen later.  and  are stored in a sorted state to enable this.]; however, both  and  can be directly transformed into their standard Python counter-parts.

Note: Generally, domains in  may contain any Python object; however, domains that support iterating over CNFS 
impose some restrictions that will be shown later. Since the theoretical framework 
is built just for CNFS, its formalization to Python is mapped in a way that
respects these limitations from the beginning. For this reason,  is not
identified with all Python objects.
The Python incarnation of  is called basic objects.

Now we established an isomorphism between objects. 
We define that two objects are isomorphic if they can be obtained
one from another by permuting its atoms.
To control permutations, partitioning of atoms is introduced and permutation of
atoms is allowed only within its “own” class.
These classes are defined through , that is an abbreviation of “unlabeled set”.







Abstract:
Let us fix a function : → 2^ in the following way:


  * ∀ a ∈: a ∈(a)

  * ∀ a, b ∈: (a) = (b) (a) ∩(b) = ∅


Obviously  partitions  into disjoint classes.

Let  be a set of all bijective functions from  to  such that for each π∈ holds ∀ a ∈: π(a) ∈(a).

Applying π∈ to an object o ∈ (written as o^π) is defined as follows:


  * o^π = π(o) if o ∈

  * o^π = {o_1^π, …, o_n^π} if {o_1, …, o_n} = o

  * o^π = (o_1^π, …, o_n^π) if (o_1, …, o_n) = o


Let o_1, o_2 ∈ then o_1 and o_2 are isomorphic (written as o_1 ≡ o_2) if there exists π∈ such that o_1 = o_2^π.


:
All integers, strings, , , and  have a singleton unlabeled set, i.e., (a) = {a}.
Therefore, all objects that contain only these atoms always form their own “private” isomorphic class. 
For example:  cannot be isomorphic to anything else since string  and integer  cannot be replaced,
because for each π∈ holds π("𝚊𝚋𝚌") = "𝚊𝚋𝚌" and π(1) = 1.

The only way to create a non-singleton unlabeled set is to use domain  (Unlabled set) that creates a set of atoms belonging to the same unlabeled set; in other words, if X is created by  then for each o ∈ X holds (o) = X.

python
>>> a = hd.USet(3, "a")
>>> list(a)
[a0, a1, a2]	


The first argument is the size of the set, and the second one is the name of the set that has only informative character.
The name is also used as the prefix of element names, again without any semantical meaning.
Elements of  are instances of  that is a wrapper over an integer and a reference to the  that contains them.

Method  takes two objects and returns  iff the objects are isomorphic according to our definition.
Several examples are shown in Figure <ref>.


 




 §.§ Canonical forms


 implements an iteration over canonical forms as a way to obtain exactly one element for each isomorphic class.
We define a canonical form as the smallest element from the isomorphic class according to a fixed ordering. 

Abstract: We fix a binary relation ≤ for the rest of the section 
such that  is well-ordered under ≤. As usual, we write o_1 < o_2 if o_1 ≤ o_2 and o_1 ≠ o_2.
A canonical form of an object o is (o) = min{ o' ∈| o ≡ o' }.
We denote = { o ∈| o = (o) } as a set of all canonical forms.






: Canonical forms can be generated by calling  on a domain.
Figure <ref> shows simple examples of generating CNFS. In case 1, we have only two 
results  and ; the former represents a pair with
the same two values
and the latter represents a pair of two different values. Obviously, we cannot get one from the other by applying any permutation,
and all other elements of Cartesian product  can be obtained by permutations. This fact is independent of the size of  (as it has at least two elements).
In case 2, the result is two elements, since we cannot permute elements from different usets. The third case shows 
canonical forms of a power set of , as we see there is exactly one canonical form for each size of sets.



Generating CNFS is limited in  to strict domains that have the following features:



  * A strict domain contains only basic objects (defined at the beginning of this section).

  * A strict domain is closed under isomorphism.


The first limitation comes from the need of ordering. The standard comparison method  is
not sufficient since it may change between executions. To ensure deterministic
canonical forms[
In Python 2, instances of different types are generally unequal, and they are ordered consistently but arbitrarily.
Switching to Python 3 does not help us, since comparing incompatible types throws an error (e.g. ), hence
standard comparison cannot serve as ordering that we need for basic objects.
],
 defines  method. This  method is responsible for deterministic 
comparison of basic objects and provides some additional properties that are
explained later. The second condition ensures that canonical forms represent all
elements of a domain. Usually these conditions do not present a practical
limitation. Elementary domains except for  are always strict and standard compositions preserve strictness. Elementary domain  allows to define a (strict) domain through canonical elements,
hence it serves as a substitute for  in a case when a strict
domain from explicitly listed elements is needed.



 §.§ The Algorithm


This section describes implementation of the algorithm that generates
canonical forms. A naïve approach would be to iterate over all elements and filter out non-canonical ones.
 avoids the naïve approach and makes the generation of canonical forms more efficient. It constructs new elements from smaller ones in a depth-first search manner. 
On each level, relevant extensions of the object are explored, and non-canonical
ones are pruned.
The used approach guarantees that all canonical forms are generated, and each will be generated exactly once, 
hence the already generated elements do not need to be remembered (except the current branch in a building tree).

This approach was already used in many applications and extracted into an abstract framework (e.g.  <cit.>).
The main goal of this section is to show correctness of the approach used in
 and not to give an abstract framework for generating canonical elements, since it was done before. However, the goal is
not to generate a specific kind of structures, but provide a framework for their
describing, therefore, a rather abstract approach must still be used.

Let us note that the algorithm is not dealing here with efficiency of deciding whether a given element is in a canonical form. In our use cases, most elements are relatively
small, hence all relevant permutations are checked during checking the canonicity
of an element. Therefore, the implementation in  is quite straightforward.
It exploits some direct consequences of Proposition <ref> that allow
the algorithm to reduce the set of relevant permutations and in some cases immediately claim non-canonicity.

The used approach is based on the following two propositions.
The first says that an object cannot be canonical if it  contains “gaps” in
atoms occurring in the object. The second shows that new elements can only be
constructed from existing canonical forms and still all of them are reached.
 
At the beginning, let us introduce some properties of the ordering given by
 which allow the propositions to be established.
On the abstract level, the following properties for ordering ≤ are assumed where o, o' ∈:



  * Tuples of the same length are lexicographically ordered.

  * If o = { o_1, …, o_n } where o_1 < … < o_n and o' = { o'_1, …, o'_n } where o'_1 < … < o'_n then
o ≤ o' if (o_1, …, o_n) ≤ (o'_1, …, o'_n).


A set X ⊆ contains a gap if there exists a ∈ X such that there is a' ∈∖ X and a' ∈(a) where (a) = { a' ∈(a) | a' < a  }.


If o ∈ and (o) contains a gap, then o is not a canonical form. 	


Proposition <ref> is a direct consequence of the following claim:


If o ∈ O and a', a ∈ such that a' ∈(a), a ∈(o), a' ∉(o)
and π∈ is a permutation that only swaps a and a'
then o^π < o.




The proposition is proved by induction on the structure of o; let a, a', π be as in the statement of the proposition:
If o is an atom then directly o = a, o^π = a' and a' < a from assumptions.
Now assume that o = (o_1, …, o_n) and the proposition holds for all o_i, i ∈{1, …, n}.
From assumptions we get that each o_i does not contain a' and there is the
minimal index f ∈{1, …, n} such that o_f contains a. Hence o_i =
o_i^π for all i ∈{1, …, f-1} and o_f^π < o by the induction
assumption. Since tuples are lexicographically ordered it follows that o^π < o. Similar ideas apply also for sets.


Let us define function : →∪{} (where  is a fresh symbol) that gives rise to a search tree. The function returns
a “smaller” object from which the object may be constructed. The function returns  for “ground” objects (atoms, empty tuples/sets). 


    (o) = 
       if  o ∈∪{ (), {}}
    
    (o_1, …, o_n)    if  o = (o_1, …, o_n+1) 
    
    o ∖{ x }   if  o  is a non-empty set and  x = max o







	
	For each o ∈ holds:
	
	
  * Exists n ∈{1, 2, …} such that ^n(o) =.
	
  * If o is a canonical form then (o) is  or a canonical form. 
	


	(1) If o ∈ then n = 1, if o is a set/tuple then n is the number of elements in the set/tuple.
	
	(2) Assume that there is o ∈ and o' = (o) ≠ and there
  is π∈ such that o'^π < o'. Since o' ≠, o has to
  be a non-empty tuple or set by definition of . If o is a tuple then
  from the lexicographic ordering of tuples follows that o^π < o and this is
  a contradiction. Now we explore the case o = { o_1, … o_n+1} where o_i < o_j for i
  < j and i, j ∈{1, …, n+1 }. If there is {p_1, … p_n} = o'^π such that p_i < p_j for i,j ∈{1, …, n} then from fact that o'^π < o' follows that there has to be f ∈{1, …, n} such that p_f < o_f and p_i = o_i < p_f for all i ∈{1, …, f - 1}.
	The last step is to explore what happens when π is applied on o; let {q_1, … q_n+1} = o^π such that q_i < q_j for i,j ∈{1, …, n + 1} and let k ∈{1, …, n + 1} such that q_k = o_n+1^π.

	Since applying π on an object is bijective, k ≠ f. 
	If f < k then it follows that
	o_i = p_i = q_i for i ∈{1, …, f - 1 } and q_f = p_f < o_f and hence o^π < o.
	If k < f then
	o_i = p_i = q_i for i ∈{1, …, k - 1 } and q_k < q_k+1 = p_k = o_k and hence o^π < o.	
	

Proposition <ref>.1 shows that  defines a tree where:
 is the root; non-root nodes are elements from ;
<ref>.2 shows that each canonical form can be reached from the root by a path that contains only canonical forms.
Moreover, the elements “grow” with the distance from the root.

This serves as a basis for the algorithm generating canonical forms
of elements from a domain. It recursively takes an object and tries to create a
bigger one, starting from . On each level, it checks whether the new
element is canonical, if not, the entire branch is terminated. The way of getting a bigger object from a smaller one,     
depends on the specific domain, what type of objects are generated and by which
elements the already found elements are extended.
Since domains are composed from smaller ones,  iterates the elements of a subdomain to gain possible “extensions” to create a new object; such extensions are then added to the existing object to obtain a possible continuation in the tree.
Since subdomains are also strict domains, only through canonical elements of the
subdomain is iterated and 
new extensions are created by applying permutations on the canonical forms. 
Once it is clear that the extension leads to an object with a gap, then such a
permutation is omitted. Therefore, it is not necessary to go through all of the permutations.

Example:

python
>>> a = hd.USet(1000, "a")
>>> b = a * a
<Product size=1000000 (a0, a0), (a0, a1), (a0, a2), (a0, a3), ...>
>>> list(b.cnfs())
[(a0, a0), (a0, a1)]


The domain in variable  has one million of elements; however, only two 
of them are canonical forms.  starts with an empty tuple, then it asks for canonical forms of the subdomain  that is a set containing only . The only permutation on  that does not create a gap after adding into empty tuple is identity,
so the only relevant extension is . Therefore, only  is
examined as a continuation. It is a canonical form, so the generation continues. Now the second domain from Cartesian product is used, 
in this particular example, again canonical forms of  is used. At this
point the only no-gap (partial) permutations are identity and swap of
 and , hence possible extensions are  and
. Extending  give us  and  as results.

The approach is similar when sets are generated. The only thing that needs to be
added for this case is a check that the extending object is bigger (w.r.t. ≤) than previous
ones, to ensure that the current object is the actual parent of the resulting object.




§ DISTRIBUTED COMPUTATIONS


 was designed to enable parallel computation on cluster machines from the beginning.
Dask/distributedhttps://github.com/dask/distributed serves as the backend for computations.
The code that uses this feature was already shown at the end of Section <ref>.



 contains a scheduler that dynamically interacts with dask/distributed scheduler.
's scheduler gradually takes elements from a pipeline and assigns them to dask/distributed.
 calculates an average execution time of recent jobs and the job size is altered to having neither too small jobs
nor too large with respect to job time constraints.

 chooses a strategy to create jobs in dependence on a chosen method of a domain exploration. 
The simplest strategy is for randomly generated elements; the stream in the pipeline induces independent jobs and the scheduler has to care only about collecting results and adhering to a time constraint (that may be specified in  method). 

In the case of iterating over all elements, there are three supported strategies: strategy for domains that support full slicing, for domains with filtered slicing, and a generic strategy for domains without slicing. 
The last one is a fallback strategy where  scheduler itself generates elements, these elements with the rest of the pipeline
are sent as jobs into dask/distributed.

The full slicing is supported if the number of elements in a domain is known and an iterator over the domain that skips the first n elements can be
efficiently created.
In this case, the domain may be sliced into disjunct chunks of arbitrary sizes.  scheduler simply creates 
lightweight disjoint tasks to workers in form “create iterator at i steps and process m elements” without transferring 
explicit elements of domains. All built-in domains support full slicing as long as the filter is not applied.

If a domain is created by applying a filter, both properties are lost generally,
i.e., the exact number of elements, 
and an efficient iterator from the n-th item. However, if the original domain
supports slicing it is possible to utilize this fact. 
Domains can be sliced as if there was no filter present in domain or subdomains
at all, 
while allowing to signalize that some elements were skipped. Note, the filtered
elements cannot be silently swallowed, because the knowledge of how many elements
were already generated in the underlying domain would be lost. In such a case it
could not be possible to ensure that the iterations go over disjunct chunks of a domain.
The iterators that allow to signalize that one or more elements were internally
skipped are called “skip iterators”.
The ability to signalize skipping more elements at once allows to implement efficient slicing when
filter domains are used in composition. For example, assume a Cartesian product of two filtered domains, where consecutive chunks of elements are dropped when a single element is filtered in a subdomain. This strategy usually works well in practice for domains
when elements dropped by the filter are spread across the whole domain. 

If canonical forms are generated, then the goal is to build a search tree. One job assigned to dask/distributed 
represents a computation of all direct descendants of a node in a search tree.
In the current version, it is quite a simple way of distributed tree search and there is a space for improvements; it is the youngest part of .



§ PERFORMANCE


The purpose of this section is to give a basic impression of 's
performance. For comparison the two examples from
Sections <ref> ad <ref> are used.


First of all, Haydi is compared with other tools. This comparison is
demonstrated on the example of generating directed graphs.
Geng <cit.> is used as a baseline within the comparison,
since it is a state of the art generator for graphs. In order to simulate a
prototyping scenario a special version is included. This version loads graphs
generated by geng into Python. The loading process is done using the networkxhttps://networkx.github.io/ library and a small manual wrapper.
Moreover, the results of two other experiments are included. Both experiments summarize
graphs generated by SageMath, in the first case SageMath
uses geng as the backend while in the other one it uses its own graph
implementation Cgraph.
 was executed with Python 2.7.9 and PyPy 5.8.0. Geng 2.6r7
and SageMath 8.0 were used. Experiments were executed on a laptop
with Intel Core i7–7700HQ (2,8 GHz). Source codes of all test scripts can be
found in the 's git repository. The results are shown in Table <ref>.
In all cases, except the last one, the goal was to generate all non-isomorphic graphs  with the given number of vertices without any additional computation on them. The last entry generates all possible graphs (including isomorphic ones) and runs in parallel on 8 processes. 



It is obvious that Haydi cannot compete with Geng in generating graphs. Geng is hand-tuned for this specific use case,
in contrast to Haydi that is a generic tool. On the other hand, the Haydi program that generates graphs can be simply extended or modified to generate different custom structures while modifying Geng would be more complicated.






The second benchmark shows strong scaling of parallel execution of the reset word generator from Section <ref> for six vertices and two alphabet characters for variants where  was replaced by , since the parallelization 
of  is not fully optimized, yet. The iterated domain supports the full slicing mode.
The experiment was executed on the Salomon cluster.



The last note on performance: we have experimented with several concepts of 
the tool. The first version was a tool named Qithttps://github.com/spirali/qit,
that shares similar ideas in API design with . It also has Python API, but generates 
C++ code behind the scene that is compiled and executed.
Benchmarks on prototypes showed it was around 3.5 times faster than pure Python version (executed in PyPy);
however, due to C++ layer, Qit was less flexible than the current version  and hard to debug for the end user.
Therefore, this version was abandoned in favor of the pure-python version to obtain a more flexible environment for experiments and prototyping. As the problems encountered in generation of combinatorial objects are often exponential, 3.5× speedup does not compensate inflexibility.

splncs03






§ FUNCTION 



python
from haydi.algorithms import search

# Let us precompute some values that will be repeatedly used
init_state = frozenset(states)
max_steps = (n_states**3 - n_states) / 6
# Known result is that we do not need more than (n^3 - n) / 6 steps

def check_automaton(delta):
	# This function takes automaton as a transition function and
	# returns the minimal length of reset word or 0 if there
	# is no such word

	def step(state, depth):
		# A step in bread-first search; gives a set of states
		# and return a set reachable by one step
		for a in alphabet:
		    yield frozenset(delta[(s, a)] for s in state)

	delta = delta.to_dict()
	return search.bfs(
		init_state,  # Initial state
		step,        # Function that takes a node and
                             # returns the followers
		lambda state, depth: depth if len(state) == 1 else None,
		# Run until we reach a single state
		max_depth=max_steps,  # Limit depth of search
		not_found_value=0)    # Return 0 when we exceed
                                      # depth limit


