DMC: A Distributed Model Counter
Authors: Jean-Marie Lagniez, Pierre Marquis, Nicolas Szczepanski
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present and evaluate DMC, a distributed model counter for propositional CNF formulae based on the state-of-the-art sequential model counter D4. DMC can take advantage of a (possibly large) number of sequential model counters running on (possibly heterogeneous) computing units spread over a network of computers. For ensuring an efficient workload distribution, the model counting task is shared between the model counters following a policy close to work stealing. The number and the sizes of the messages which are exchanged by the jobs are kept small. The results obtained show DMC as a much more efficient counter than D4, the distribution of the computation yielding large improvements for some benchmarks. DMC appears also as a serious challenger to the parallel model counter Count Antom and to the distributed model counter d Count Antom. ... The empirical results we obtained show DMC as a much more efficient counter than D4, the distribution of the computation leading to significant time savings and yielding large improvements for some benchmarks. We also compared DMC with Count Antom and d Count Antom, and again, empirically, the computational benefits were often very significant. ... We have presented DMC, a distributed model counter for CNF formulae, based on the sequential model counter D4. ... The empirical results we have obtained show DMC as a much more efficient counter than D4, the distribution of the computation leading to time savings of several orders of magnitude and yielding large improvements for some benchmarks. Experimentally, DMC appears also as a serious challenger to Count Antom and to d Count Antom. |
| Researcher Affiliation | Academia | Jean-Marie Lagniez1, Pierre Marquis1,2, Nicolas Szczepanski1 1 CRIL-CNRS UMR 8188, Universit e d Artois, Lens, France 2 Institut Universitaire de France |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks labeled |
| Open Source Code | No | The binary code of DMC is available from the web page of the Compile! project, at www.cril.fr/KC/. The paper states |
| Open Datasets | Yes | All the instances from the first 7 families come from the SAT LIBrary www.cs.ubc.ca/ hoos/SATLIB/index-ubc.html. ... The instances of the last two families include those considered in the experiments reported in [Burchard et al., 2015; 2016] and are available from https://projects.informatik.uni-freiburg.de/projects/countantom/files. |
| Dataset Splits | No | The paper uses |
| Hardware Specification | Yes | The experiments have been conducted on a cluster of sixteen 32 Gi B RAM computers containing each two quad-core bi-processors Intel XEON X5500 at 2.67 GHz. The cluster is equipped with an Ethernet controller at 1 Gi B/s. |
| Software Dependencies | No | In our implementation of DMC, the communications between processes are managed using the library Open MPI for message passing interface (MPI). The paper mentions |
| Experiment Setup | Yes | A time-out (wall clock time) of 3600s has been considered for each instance. In the experiments, every worker used within DMC is an avatar of D4, which takes advantage of the same preprocessing combination, namely the computation of the backbone of the input [Monasson et al., 1999], followed by an occurrence reduction step [Lagniez and Marquis, 2017a]. A worker does not ask any help whenever the number of variables V of its current job (γ, V ) does not exceed the value of the parameter nb Var Seq of DMC, fixed to 30 in our experiments. |