Notice: This website is continuously updated as new conference proceedings and journal volumes are published. Consequently, the figures presented here may differ from those reported in our publications.
A brief overview of our methodology is provided on the Methods page, along with references to publications documenting our approach and links to the code and data used in each study.
The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates.
A Recursive Algorithm for Projected Model Counting
Authors: Jean-Marie Lagniez, Pierre Marquis1536-1543
AAAI 2019 | Venue PDF | LLM Run Details | Input Tokens: 16,531 Total number of tokens sent to the LLM as input for this paper's analysis. | Output Tokens: 4,331 Total number of tokens produced by the LLM (including reasoning/thinking tokens) for this paper's analysis.
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In order to evaluate the benefits offered by proj MC, we performed some experiments. The empirical protocol we followed is precisely the same as the one considered in (Aziz et al. 2015). Thus we have considered 260 instances coming from three data sets. ... Our experiments show that in many cases proj MC challenges the previous algorithms for projected model counting from the literature. |
| Researcher Affiliation | Academia | CRIL, U. Artois & CNRS Institut Universitaire de France F-62300 Lens, France EMAIL |
| Pseudocode | Yes | Algorithm 1: proj MC(Σ, X) ... Algorithm 2: DD(Σ, ω, X) |
| Open Source Code | Yes | The binary code of proj MC, as well as the benchmarks used in our experiments and additional empirical results are available from www.cril.fr/KC/. |
| Open Datasets | Yes | The binary code of proj MC, as well as the benchmarks used in our experiments and additional empirical results are available from www.cril.fr/KC/. |
| Dataset Splits | No | The paper does not mention explicit training, validation, or test dataset splits in the context of machine learning model training. The 'instances' and 'benchmarks' are used for evaluation of the model counting algorithm itself. |
| Hardware Specification | Yes | All the experiments have been conducted on a cluster of Intel Xeon E5-2643 (3.30 GHz) quad core processors with 32 Gi B RAM. |
| Software Dependencies | Yes | The kernel used was Cent OS 7, Linux version 3.10.0-514.16.1.el7.x86 64. The compiler used was gcc version 5.3.1. |
| Experiment Setup | Yes | A time-out of 600s and a memory-out of 7.6 Gi B has been considered for each instance. |