Towards Generalization in QBF Solving via Machine Learning
Authors: Mikoláš Janota
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The evaluation considers the following configurations of algorithm QFUN (Algorithm 3): QFUN without any learning, which is in the fact RARe QS; versions QFUN-16, QFUN-64, and QFUN-128 where learning is triggered every 16/64/128 iterations, respectively; QFUN-64-f forgetful version of QFUN where previously learned strategies are not used in the future. All the other versions accumulate strategies as described in Section 4.3. Additionally we compare to the highly competitive non-CNF solvers Ghost Q (Klieber et al. 2010) and Qu Ab S (Tentrup 2016). The evaluated prototype is implemented in C++ and minisat 2.2 (E en and S orensson 2003) is used as the backend solver. The experiments were carried out on Linux machines with Intel Xeon 5160 3GHz processors and 4GB of memory with the time limit 800 s and memory limit 2GB. For the evaluation we used the non-CNF suite from the 2017 QBF Competition counting 320 instances.1 The overall results are summarized in Table 1. The cactus plot in Fig. 1a summarizes the performance. |
| Researcher Affiliation | Academia | Mikol aˇs Janota INESC-ID / Instituto Superior T ecnico, Universidade de Lisboa, Portugal mikolas.janota@gmail.com |
| Pseudocode | Yes | Algorithm 1: Playing 1-move multi-game; Algorithm 2: QFUN2: 2-level QBF Refinement with Learning; Algorithm 3: QBF Refinement with Learning |
| Open Source Code | No | The paper mentions that the prototype is implemented in C++ and uses minisat 2.2 as a backend, but it does not provide a link or explicit statement about the availability of its own source code. |
| Open Datasets | Yes | For the evaluation we used the non-CNF suite from the 2017 QBF Competition counting 320 instances.1 ... 1www.qbflib.org/event page.php?year=2017 |
| Dataset Splits | No | The paper states that the 'non-CNF suite from the 2017 QBF Competition counting 320 instances' was used for evaluation, but it does not specify how this dataset was split into training, validation, or test sets for the experimental evaluation. It mentions 'samples E' for internal learning but not for the overall benchmark evaluation. |
| Hardware Specification | Yes | The experiments were carried out on Linux machines with Intel Xeon 5160 3GHz processors and 4GB of memory with the time limit 800 s and memory limit 2GB. |
| Software Dependencies | Yes | The evaluated prototype is implemented in C++ and minisat 2.2 (E en and S orensson 2003) is used as the backend solver. |
| Experiment Setup | Yes | The evaluation considers the following configurations of algorithm QFUN (Algorithm 3): QFUN without any learning, which is in the fact RARe QS; versions QFUN-16, QFUN-64, and QFUN-128 where learning is triggered every 16/64/128 iterations, respectively; QFUN-64-f forgetful version of QFUN where previously learned strategies are not used in the future. |