Enumerating Potential Maximal Cliques via SAT and ASP

Authors: Tuukka Korhonen, Jeremias Berg, Matti Järvisalo

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

Reproducibility Variable Result LLM Response
Research Type Experimental Empirically, we show that integrating the proposed approaches into a recent BT implementation compares favorably with the use of specialized enumeration on the tasks of determining treewidth and generalized hypertreewidth. 6 Experiments We integrated the three declarative approaches to PMC enumeration to the recent BT implementation Triangulator [Korhonen et al., 2019] that supports both treewidth and generalized hypertreewidth.
Researcher Affiliation Academia Tuukka Korhonen , Jeremias Berg and Matti J arvisalo HIIT, Department of Computer Science, University of Helsinki, Finland
Pseudocode Yes Algorithm 1 SAT-based lazy enumeration of size-k PMCs
Open Source Code Yes The implementation is available at https://github.com/Laakeri/pmcenum-ijcai.
Open Datasets Yes For further experiments, we used all of the benchmarks instances from [Korhonen et al., 2019], consisting of 589 graphs for treewidth and 265 for generalized hypertreewidth gathered from various different sources (including PACE 2016 and 2017 instances).
Dataset Splits No The paper describes an iterative algorithm that uses a parameter 'k' to enumerate PMCs, but does not provide explicit training, validation, or test dataset splits in the context of machine learning model training.
Hardware Specification Yes All experiments were run single-threaded on computing nodes with 2.4-GHz Intel Xeon E5-2680-v4 processors.
Software Dependencies Yes We used Clingo 5.3.0 [Gebser et al., 2016] as the de-facto ASP solver, and based on preliminary experiments of several state-of-the-art SAT solvers Glucose 4.1 as the SAT solver [Audemard and Simon, 2018] through its incremental API.
Experiment Setup Yes A per-instance 2-hour time limit and 32-GB memory limit was imposed. For ASP, we used Clingo s built-in support for enumerating all answer sets.