Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions

Authors: Stephan Gocht, Ciaran McCreesh, Jakob Nordström

IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental 4 Implementation and Evaluation We implemented the proof logging techniques described above in the Glasgow Subgraph Solver... Evaluation. ... we can demonstrate that the techniques we have described can be implemented, and that producing and verifying subgraph isomorphism proofs works in practice, at least on smaller graphs. Hardware setup. Our experiments are performed on a cluster of machines with dual Intel Xeon E5-2697A v4 CPUs and 512GBytes RAM, running Ubuntu 18.04... Instances. We use the instances collected by Kotthoff et al. [2016] for evaluation... Time costs of proof logging and verification. In the top row of Figure 1 we show the time costs of performing proof logging and verification on these instances.
Researcher Affiliation Academia Stephan Gocht1,2 , Ciaran Mc Creesh3 and Jakob Nordstr om2,1 1Lund University, Lund, Sweden 2University of Copenhagen, Copenhagen, Denmark 3University of Glasgow, Glasgow, Scotland
Pseudocode No The paper describes algorithmic steps and proof structures in prose and mathematical expressions, but does not include a formally labeled 'Pseudocode' or 'Algorithm' block.
Open Source Code Yes We implemented3 the proof logging techniques described above in the Glasgow Subgraph Solver;... 3https://github.com/ciaranm/glasgow-subgraph-solver
Open Datasets Yes Instances. We use the instances collected by Kotthoff et al. [2016] for evaluation.
Dataset Splits No The paper uses 'standard enumeration benchmark instances' from Kotthoff et al. [2016] for evaluation but does not specify dataset splits for training, validation, or testing. The problem addressed is combinatorial solving, not machine learning, so traditional data splits are not described.
Hardware Specification Yes Hardware setup. Our experiments are performed on a cluster of machines with dual Intel Xeon E5-2697A v4 CPUs and 512GBytes RAM, running Ubuntu 18.04.
Software Dependencies No The paper mentions 'Ubuntu 18.04' as the operating system and refers to 'Veri PB' but does not provide specific version numbers for 'Veri PB' or other software dependencies.
Experiment Setup Yes We therefore select every instance where the target graph has no more than 260 vertices, and where the unmodified Glasgow solver without proof logging can enumerate every solution in no more than ten seconds." and "The Glasgow solver uses a bit-parallel all-different propagator" and "Archibald et al. [2019] showed that rather than performing a simple backtracking search, it is better to repeatedly perform a small amount of search and then restart the solver with a new branching strategy. At every restart, a set of nogoods [Lecoutre et al., 2007; Lee et al., 2016] is recorded