Boosting MCSes Enumeration
Authors: Éric Grégoire, Yacine Izza, Jean-Marie Lagniez
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Then, we present our extensive experimental study. |
| Researcher Affiliation | Academia | Eric Gr egoire, Yacine Izza, Jean-Marie Lagniez CRIL Universit e d Artois & CNRS, Lens, France {gregoire,izza,lagniez}@cril.fr |
| Pseudocode | Yes | Algorithm 1: Enum-ELS (Enumerate All MCSes Computed with the Extract Partial MCS procedure); Algorithm 2: TC-MCS ( Σ1 ΣS 2 , U ); Algorithm 3: Enum-ELS-RMR; |
| Open Source Code | Yes | All data, results and software used in the experimentations are available from http://www.cril.fr/enumcs. |
| Open Datasets | Yes | We have selected the 866 benchmarks used in [Previti et al., 2017; Marques-Silva et al., 2013]: 269 instances are plain Max-SAT ones and the remaining 597 are Partial Max-SAT ones. We have enriched this experimental setting by also considering a second series of plain Max-SAT benchmarks made of the instances from the MUS competition http://www.satcompetition.org/2011. |
| Dataset Splits | No | The paper refers to established benchmarks but does not provide explicit train/validation/test splits within these benchmarks in the text. |
| Hardware Specification | Yes | All experimentations have been conducted on Intel Xeon E5-2643 (3.30GHz) processors with 64Gb memory on Linux CentOS. |
| Software Dependencies | No | We have implemented all our algorithms in C++ and used Minisat http://minisat.se/ as backend SAT solver. No version number for Minisat is provided. |
| Experiment Setup | Yes | Time-out was set to 1800 seconds for each run of an algorithm on an instance; memory-out was set to 8 Gb for each such run. |