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..
Dependency Learning for QBF
Authors: Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
JAIR 2019 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments on standard benchmark sets demonstrate the effectiveness of this technique. To explore the effectiveness of this technique, we implemented Qute, a QCDCL solver that supports dependency learning. In experiments with benchmark instances from the 2016 2018 QBF Evaluations, Qute is highly competitive with state-of-the-art QBF solvers on both formulas in prenex conjunctive normal form (PCNF), as well as non-CNF formulas in the QCIR format. A comparison of various configurations shows that dependency learning has a significant positive impact on Qute s performance. |
| Researcher Affiliation | Academia | Tom aˇs Peitl EMAIL Friedrich Slivovsky EMAIL Stefan Szeider EMAIL Algorithms and Complexity Group, TU Wien Favoritenstraße 9-11, 1040 Vienna, Austria |
| Pseudocode | Yes | Algorithm 1 QCDCL with Dependency Learning and Algorithm 2 Conflict Analysis with Dependency Learning |
| Open Source Code | Yes | To see whether dependency learning works in practice, we implemented a QCDCL solver that supports this technique named Qute.3 We evaluated the performance of Qute in several experiments. 3. http://github.com/perebor/qute |
| Open Datasets | Yes | In our first experiment, we used the prenex non-CNF (QCIR, Jordan, Klieber, & Seidl, 2016) benchmark sets from the 2016 2018 QBF Evaluation, consisting in total of 1240 formulas. [...] For our second experiment, we used the prenex CNF (PCNF) benchmark sets from the 2016 2018 QBF Evaluations consisting of 1314 instances. |
| Dataset Splits | No | The paper uses standard benchmark sets from QBF Evaluations, but does not provide specific details on training/test/validation splits within the paper itself. It discusses 'instances' (e.g., '1240 formulas', '1314 instances') rather than dataset splits. |
| Hardware Specification | Yes | For our experiments, we used a cluster with Intel Xeon E5649 processors at 2.53 GHz running 64-bit Linux. |
| Software Dependencies | No | The paper mentions several tools and solvers used or compared against (e.g., Qute, HQSPre, qcir-conv, Dep QBF, CAQE) but does not provide specific version numbers for any of them, nor for any other software dependencies like programming languages or libraries. |
| Experiment Setup | Yes | Appendix A. Solver Parameters for Experiments in Section 5 parameter value description --decision-heuristic VMTF Decision heuristic, see Section 5. --restarts inner-outer Restart strategy, see Section 5. --inner-restart-distance 250 Initial number of conflicts before restart. --outer-restart-distance 20 Initial number of restarts before outer restart. --restart-multiplier 2.5 Multiplier for increasing inner and outer restart distance. --initial-clause-DB-size 1000 Initial limit on learned clauses. --initial-term-DB-size 4000 Initial limit on learned terms. --clause-DB-increment 1000 Upon reaching the current limit on the number of learned clauses, increase the limit by this value. --term-DB-increment 500 Upon reaching the current limit on the number of learned terms, increase the limit by this value. --clause-removal-ratio 0.4 Fraction of learned clauses to delete upon reaching the current limit. --term-removal-ratio 0.3 Fraction of learned terms to delete upon reaching the current limit. --LBD-threshold 5 Only delete constraints whose LBD is greater than this value. --constraint-activity-decay 0.99 Multiply constraint activities with this value after each conflict. --constraint-activity-inc -2 Add this value to the activity score of a constraint whenever it is seen during conflict analysis. --dependency-learning all Add all variables involved in an illegal merge as learned dependencies. --phase-heuristic inv JW Heuristic for choosing the assignment of a decision variable. --model-generation dep QBF Use Dep QBF-style model generation for PCNF instances: pick the first satisfying literal in each clause, with a preference for existential literals. |