search

ciaranm / glasgow-subgraph-solver

A solver for subgraph isomorphism problems, based upon a series of papers by subsets of McCreesh, Prosser, and Trimble.
MIT License
70 stars 23 forks source link

readme

The Glasgow Subgraph Solver

This is a solver for subgraph isomorphism (induced and non-induced) problems, based upon a series of papers by subsets of Blair Archibald, Ciaran McCreesh, Patrick Prosser and James Trimble at the University of Glasgow, and Fraser Dunlop and Ruth Hoffmann at the University of St Andrews. A clique decision / maximum clique solver is also included.

If you use this software for research, please cite [icgt/McCreeshP020]. If you use this solver in a non-research setting, please get in touch if you can. This software is an output of taxpayer funded research, and it is very helpful for us if we can demonstrate real-world impact when we write grant applications.

Please contact Ciaran McCreesh with any queries.

Compiling

To build, you will need a C++20 compiler, such as GCC 10.3, as well as Boost (use libboost-all-dev on Ubuntu).

cmake -S . -B build
cmake --build build

Running

To run:

$ ./build/glasgow_subgraph_solver pattern-file target-file

If you would like induced subgraph isomorphisms rather than non-induced (that is, if non-adjacent vertices must be mapped to non-adjacent vertices), you must request it:

$ ./build/glasgow_subgraph_solver --induced pattern-file target-file

The default mode is to display the first found solution, or to prove unsatisfiability if no solution exists. To count or print all solutions, use one of:

$ ./build/glasgow_subgraph_solver [ --count-solutions | --print-all-solutions ] pattern-file target-file

Note that printing all solutions can be exponentially slower than counting solutions.

The solver supports parallel search. Usually you should enable this, as follows:

$ ./build/glasgow_subgraph_solver --parallel ...

Note that parallel search, in its default configuration, is non-deterministic.

File Formats

We try to auto-detect the input format, but it's best to specify it using, for example:

$ ./build/glasgow_subgraph_solver --format lad pattern-file target-file

In particular, note that auto-detection can easily fail if, for example, the first vertex in the graph has no neighbours. We can read LAD, Labelled LAD (labels on vertices, and optionally also on edges), CSV, and DIMACS 2 formatted graphs. The LAD format is a nice simple choice. If you need to support named vertices, labels on vertices and / or edges, or directed edges, consider using the CSV format. To specify a directed edge, use a greater-than sign rather than a comma as the delimiter between the first two columns. To specify an edge label, include a third column in the file. To specify a vertex label, leave the second column empty and use the third column for the label. For example, the following describes a graph with four vertices, with colours for edge labels and shapes for vertex labels.

first>second,red
second>first,blue
first,third,purple
first>first,green
first,,circle
second,,circle
third,,square
fourth,,square

Symmetries

Symmetry elimination support is currently very experimental, only usable on pattern symmetries, and is probably only useful for solution counting. To use it, you must have the GAP computer algebra system in your PATH as 'gap', with the 'digraph' library installed. Then, do:

$ ./build/glasgow_clique_solver --pattern-symmetries --count-solutions pattern-file target-file

Proof Logging

As a highly experimental feature, the solver can output a proof log. First, install the following program:

And then you can produce and verify a log like this:

$ ./build/glasgow_subgraph_solver --no-supplementals --no-clique-detection --no-nds \
    --prove myproof --proof-solutions pattern-file target-file
$ veripb myproof.opb myproof.pbp

Note that most features are not yet supported with proof logging. This is a "not yet implemented" problem, not a fundamental restriction.

Clique Solving

To run the clique solver, use:

$ ./build/glasgow_clique_solver graph-file

Details on the Algorithms

The subgraph solver is a constraint programming style backtracker, which recursively builds up a mapping from pattern vertices to target vertices. It includes inference based upon paths (not just adjacency) and neighbourhood degree sequences, has a fast all-different propagator, and uses sophisticated variable- and value-ordering heuristics to direct a slightly-random restarting search.

Chronologically, our first subgraph isomorphism solver is [cp/McCreeshP15]. We introduced new variants of this solver in [lion/KotthoffMS16], and described a refactored version (which can solve an optimisation variant of the problem) in [aaai/HoffmannMR17]. We also investigated search ordering heuristics in more detail in [jair/McCreeshPST18], and [cpaior/ArchibaldDHMPT19] describes its new restarting search algorithm. There is currently no paper describing the entire algorithm, but [icgt/McCreeshP020] summarises the main aspects of it.

The clique solver (with its default configuration) is a branch and bound solver that uses a greedy colouring both as the bound function, and as a branching heuristic. It is based upon the "domains of size two first" variant described in [cp/McCreeshP14], which is in turn derived from the "MCSa1" algorithm described by [algorithms/Prosser12] combined with the bit-parallelism techniques discussed by [ol/SegundoMRH13]; this in turn is a simplification of "MCS" described by [walcom/TomitaSHTW10]. The solver also incorporates the fast clique detection technique described by [jco/BatsynGMP14].

Funding Acknowledgements

This work was supported by the Engineering and Physical Sciences Research Council (grant numbers EP/P026842/1, EP/M508056/1, and EP/N007565). This work used the Cirrus UK National Tier-2 HPC Service at EPCC (http://www.cirrus.ac.uk) funded by the University of Edinburgh and EPSRC (EP/P020267/1).

References