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 [1].
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. |