You are provided with the abstract of a scientific paper and the abstracts of the papers it references. Your task is to write a Related Work section for the main paper. This section should concisely summarize and integrate the key points from the cited abstracts, reflecting how they relate to the main paper's contributions and context. In your summary, use numerical citation markers like [1], [2], etc., to refer to the corresponding papers.

Main Abstract:
Graph mining is one of the most important categories of graph algorithms. However, exploring the subgraphs of an input graph produces a huge amount of intermediate data. The 'think like a vertex' programming paradigm, pioneered by Pregel, cannot readily formulate mining problems, which is designed to produce graph computation problems like PageRank. Existing mining systems like Arabesque and RStream need large amounts of computing and memory resources. In this paper, we present Kaleido, an efficient single machine, out-of-core graph mining system which treats disks as an extension of memory. Kaleido treats intermediate data in graph mining tasks as a tensor and adopts a succinct data structure for the intermediate data. Kaleido utilizes the eigenvalue of the adjacency matrix of a subgraph to efficiently solve the subgraph isomorphism problems with an acceptable constraint that the vertex number of a subgraph is less than 9. Kaleido implements half-memory-half-disk storage for storing large intermediate data, which treats the disk as an extension of the memory. Comparing with two state-of-the-art mining systems, Arabesque and RStream, Kaleido outperforms them by a GeoMean 12.3 @math and 40.0 @math respectively.

Cited Abstract(s):
[1]: Instances of the Boolean satisfiability problem (SAT) arise in many areas of circuit design and verification. These instances are typically constructed from some human-designed artifact, and thus are likely to possess much inherent symmetry and sparsity. Previous work[4] has shown that exploiting symmetries results in vastly reduced SAT solver run times, often with the search for the symmetries themselves dominating the total SAT solving time. Our contribution is twofold. First, we dissect the algorithms behind the venerable NAUTY[9] package, particularly the partition refinement procedure responsible for the majority of search space pruning as well as the majority of run time overhead. Second, we present a new symmetry-detection tool, SAUCY, which outperforms NAUTY by several orders of magnitude on the large, structured CNF formulas generated from typical EDA problems.

[2]: The problem of canonically labeling a graph is studied. Within the general framework of backtracking algorithms based on individualization and refinement, data structures, subroutines, and pruning heuristics especially for fast handling of large and sparse graphs are developed. Experiments indicate that the algorithm implementation in most cases clearly outperforms existing state-of-the-art tools.

[3]: A new algorithm is presented for the related problems of canonically labelling a graph or digraph and of finding its automorphism group. The automorphism group is found in the form of a set of less than n generators, where n is the number of vertices. An implementation is reported which is sufficiently conserving of time and space for it to be useful for graphs with over a thousand vertices.

[4]: The individualization-refinement paradigm for computing a canonical labeling and the automorphism group of a graph is investigated. A new algorithmic design aimed at reducing the size of the associated search space is introduced, and a new tool, named "Traces", is presented, together with experimental results and comparisons with existing software, such as McKay's "nauty". It is shown that the approach presented here leads to a huge reduction in the search space, thereby making computation feasible for several classes of graphs which are hard for all the main canonical labeling tools in the literature.
The most common practical approach for the graph isomorphism problems is canonical labeling, a process in which a graph is relabeled in such a way that isomorphic graphs are identical after relabeling. The mainly strategy of the canonical labeling is building search tree for the input graph. Nauty [3] is the first program that could handle large automorphism groups; it uses automorphism to prune the search in testing automorphism. Nauty generates the search tree in depth-first order, while Trace [4] introduces a breadth-first search in generating the search tree. Saucy [1] is an implementation of the Nauty system by utilizing the sparsity and particular construction of colored graphs. However, these libraries focus on the checking of the automorphism, which only suits for the unlabeled graphs. Bliss [2] supports the isomorphism checking of labeled graphs. However, building the search tree brings frequently memory allocating and deallocating which slow down the processing and consume a huge amount of memory. In addition, bliss is designed for the large graph isomorphic checking, while the eigenvalue checking strategy is sufficient in the mining scenes.