Cardinality Encodings for Graph Optimization Problems
Authors: Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | More importantly, the experimental results show that the proposed encoding enables existing SAT solvers to compute a maximum clique for large sparse networks, often more efficiently than the state of the art. |
| Researcher Affiliation | Academia | Alexey Ignatiev 1,2, Antonio Morgado 1, and Joao Marques-Silva 1 1 LASIGE, Faculdade de Ciˆencias, Universidade de Lisboa, Portugal 2 ISDCT SB RAS, Irkutsk, Russia {aignatiev,ajmorgado,jpms}@ciencias.ulisboa.pt |
| Pseudocode | Yes | Algorithm 1: Algorithm for finding a Maximal Clique |
| Open Source Code | No | The paper mentions that "SATClq is an initial prototype" but does not provide any link or explicit statement about making its source code publicly available. |
| Open Datasets | Yes | The networks considered were obtained from two sources. First, a well-known benchmark generator of networks with community structure [Lancichinetti et al., 2008]. Second, a selection of examples from comprehensive collections of networks [Leskovec and Krevl, 2014; Rossi and Ahmed, 2015]. |
| Dataset Splits | No | The paper describes the datasets used but does not provide specific details on training, validation, or test dataset splits (e.g., percentages or counts for each split). |
| Hardware Specification | Yes | The experiments were performed in Ubuntu Linux on an Intel Xeon E5-2630 2.60GHz processor with 64GByte of memory. |
| Software Dependencies | Yes | The approach to the Max Clique problem proposed in Section 4 was implemented in a prototype as a Python script instrumenting calls to the Glucose 3.0 SAT solver [Audemard et al., 2013]. |
| Experiment Setup | Yes | The time limit was set to 3600s and the memory limit to 10GByte for each process to run. |