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.
Algorithms for Deciding Counting Quantifiers over Unary Predicates
Authors: Marcelo Finger, Glauber De Bona
AAAI 2017 | Venue PDF | LLM Run Details | Input Tokens: 15,520 Total number of tokens sent to the LLM as input for this paper's analysis. | Output Tokens: 5,494 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 | The latter is shown to lead to a viable implementation and experiments shows this algorithm presents a phase transition behavior. |
| Researcher Affiliation | Academia | Marcelo Finger Department of Computer Science University of Sao Paulo, Brazil; Glauber De Bona Department of Computer Science University College London, UK |
| Pseudocode | Yes | Algorithm 3.1 CQUBranch And Bound(ϕ) |
| Open Source Code | Yes | Available at http://cqu.sourceforge.net |
| Open Datasets | No | The paper states: 'We generate uniformly distributed random CQU-SAT instances in normal form...' rather than using a pre-existing public dataset. |
| Dataset Splits | No | The paper describes generating random instances and evaluating the solver's performance, but does not mention specific training/validation/test dataset splits. |
| Hardware Specification | No | The paper does not provide any specific details about the hardware used for running the experiments (e.g., CPU, GPU models, or memory specifications). |
| Software Dependencies | Yes | Column generation implemented using MINISAT 2.22; we implemented the Solve Relaxed Via Col Gen method using the linear solver Clp of the COIN-OR Project |
| Experiment Setup | Yes | For the first experiment, we fixed L = 100, k = 10 and n = 250 and varied the rate m/n from 0.5 to 8 in steps of 0.05. At each step, we generated randomly 100 cqu-instances and computed the percentage of satisfiable instances (%SAT, left axis) and the average time of computation in seconds (right axis). |