Solving QBF by Clause Selection
Authors: Mikolas Janota, Joao Marques-Silva
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | 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. |