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..
Solving QBF by Clause Selection
Authors: Mikolas Janota, Joao Marques-Silva
IJCAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving. |
| Researcher Affiliation | Academia | Mikol aˇs Janota1 and Joao Marques-Silva1,2 1 INESC-ID, IST, Lisbon, Portugal 2 University College Dublin, Ireland |
| Pseudocode | Yes | Algorithm 1: Two-level Selection QCNF Solving |
| Open Source Code | No | The paper states 'More detailed presentation of the results can be found on the authors website3. 3http://sat.inesc-id.pt/%7Emikolas/sw/qesto/', which points to results, but does not explicitly state that source code for the methodology is available at this link or elsewhere. |
| Open Datasets | Yes | For the evaluation we used the QBFLIB benchmark suite used in the 2014 QBF Gallery2 and the benchmarks from the 2QBF track of the 2010 QBF Evaluation. 2http://www.kr.tuwien.ac.at/events/qbfgallery2013/benchmarks/eval2012r2.tar.7z |
| Dataset Splits | No | The paper mentions using benchmark suites but does not specify any training, validation, or test dataset splits or how the data was partitioned for experiments. |
| Hardware Specification | Yes | The experimental results were carried out on Linux machines with Intel Xeon 5160 3GHz processors and 4GB of memory. |
| Software Dependencies | Yes | The prototype used for the evaluation was implemented in C++ and the SAT solver minisat 2.2 [E en and S orensson, 2003a] was used. |
| Experiment Setup | No | The paper states 'The time limit was set to 800 s and the memory limit to 2GB.' but does not provide specific hyperparameters, training configurations, or detailed system-level settings for the algorithm itself. |