Notice: 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. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Algorithms for Deciding Counting Quantifiers over Unary Predicates
Authors: Marcelo Finger, Glauber De Bona
AAAI 2017 | Venue PDF | LLM Run Details
| 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). |