QCDCL with Cube Learning or Pure Literal Elimination - What is Best?
Authors: Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our theoretical results on the strength of different QCDCL models are empirically confirmed by experiments with stateof-the-art QCDCL solvers (cf. Section 8). |
| Researcher Affiliation | Academia | 1Friedrich Schiller University Jena, Germany 2TU Wien, Vienna, Austria |
| Pseudocode | No | The paper does not contain any pseudocode or clearly labeled algorithm blocks. |
| Open Source Code | No | The paper mentions using existing state-of-the-art solvers (Dep QBF, Qute) but does not state that the authors are releasing any source code for their own contributions or formal systems. |
| Open Datasets | Yes | We recall the equality formulas Eqn of Beyersdorff et al. [2019a]. ... We ran Dep QBF on each of the formulas used for separations in this paper, as well as on the PCNF track of the QBF Evaluation 2020.2 |
| Dataset Splits | No | The paper does not discuss typical machine learning datasets or provide information on train/validation/test splits. Its experiments involve running solvers on pre-defined QBF formulas. |
| Hardware Specification | Yes | The computation was performed on a machine with two 16-core Intel Xeon E52683 v4@2.10GHz CPUs and 512GB RAM running Ubuntu 20.04.3 LTS on Linux 5.4.0-48. |
| Software Dependencies | Yes | We picked the solver Dep QBF [Lonsing and Egly, 2017]... We additionally ran Qute [Peitl et al., 2019]... The computation was performed on a machine with... Ubuntu 20.04.3 LTS on Linux 5.4.0-48, and organized with the help of GNU Parallel [Tange, 2011]. |
| Experiment Setup | Yes | We set the time limit on each formula to 10 minutes (no memory limit). ... We evaluated 24 configurations of Dep QBF with and without PLE and with and without SDCL, and for each of these four, with each of the 6 possible heuristics.3 ... 3Using --dec-heur= (--phase-heuristic for Qute). |