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].
QCDCL vs QBF Resolution: Further Insights
Authors: Benjamin Böhm, Olaf Beyersdorff
JAIR 2024 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants parameterised by different policies for decisions, unit propagations and reductions lead to incomparable systems for almost all choices of these policies. The central quest of our research here is to find different QCDCL variants that are as strong as QU-Resolution and long-distance Q-Resolution. While we do not claim that these new algorithms are of immediate practical interest, we believe it is important to theoretically gauge the full potential of QCDCL. Our results can be summarised as follows. (a) New QCDCL Versions. (b) Characterisation of QBF Proof Systems. (c) Separations between QCDCL Variants. |
| Researcher Affiliation | Academia | Benjamin B ohm EMAIL Olaf Beyersdorff EMAIL Friedrich Schiller University Jena, Germany |
| Pseudocode | No | The paper describes QCDCL procedures and policies (Decision policies, Reduction policies, Propagation policies) in descriptive text, and uses formal definitions and proofs to explain the theoretical concepts. It does not include any clearly labeled pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not contain any explicit statements about releasing source code, nor does it provide links to any code repositories or mention code in supplementary materials. |
| Open Datasets | No | The QCNF Mirror CRn consists of the prefix... and the matrix... The QCNF QParitynp Y, w, Sq consists of the prefix... and the matrix... These are not external datasets but formal definitions used in the theoretical analysis. |
| Dataset Splits | No | This paper is theoretical, focusing on proof complexity and resolution systems for Quantified Boolean Formulas (QBFs). It does not involve empirical experiments with datasets, therefore, there is no mention of training/test/validation dataset splits. |
| Hardware Specification | No | This paper is theoretical and focuses on proof complexity and resolution systems. It does not describe any experimental evaluations that would require specific hardware specifications. |
| Software Dependencies | No | This paper is theoretical and focuses on proof complexity and resolution systems. It does not describe any experimental implementations that would require specific software dependencies or version numbers. |
| Experiment Setup | No | This paper is theoretical, presenting conceptual and mathematical contributions to QBF resolution systems. It does not involve empirical experiments, therefore, no experimental setup details, hyperparameters, or training configurations are provided. |