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..
Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Authors: Valeriy Balabanov, Jie-Hong Jiang, Mikolas Janota, Magdalena Widl
AAAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show the distinct benefits of the proposed method in extracting high quality certificates from some LQ-resolution proofs that are not obtainable from Q-resolution proofs. We implemented the countermodel extraction algorithm of Figure 1 and its dual model extraction algorithm in the C++ language in the tool RESQU2, and named the new implementation as RESQU-LP. The experiments were conducted on a Linux machine with a Xeon 2.53 GHz CPU and 48 GB RAM for two sets of test cases: the KBKF family of formulas (Kleine Büning, Karpinski, and Flögel 1995) and the benchmark formulas of QBFEVAL 10 (QBFEVAL 2010). |
| Researcher Affiliation | Academia | Valeriy Balabanov1, Jie-Hong R. Jiang1, Mikoláš Janota2, and Magdalena Widl3 1GIEE, National Taiwan University, Taipei, Taiwan 2INESC-ID, Lisbon, Portugal 3Vienna University of Technology, Austria |
| Pseudocode | Yes | Figure 1: Algorithm extracting a countermodel from an LQresolution proof. input: a false QBF Φ and its LQ-res DAG GΠ(VΠ, EΠ) output: a countermodel in RFAO formulas begin 01 foreach universal variable x of Φ 02 RFAO[x] := ; ... |
| Open Source Code | Yes | We implemented the countermodel extraction algorithm of Figure 1 and its dual model extraction algorithm in the C++ language in the tool RESQU2, and named the new implementation as RESQU-LP. 2http://alcom.ee.ntu.edu.tw/resqu/ |
| Open Datasets | Yes | The experiments were conducted on a Linux machine with a Xeon 2.53 GHz CPU and 48 GB RAM for two sets of test cases: the KBKF family of formulas (Kleine Büning, Karpinski, and Flögel 1995) and the benchmark formulas of QBFEVAL 10 (QBFEVAL 2010). |
| Dataset Splits | No | The paper mentions using "test cases" and "benchmark formulas" like KBKF and QBFEVAL 10, but it does not provide specific train, validation, or test dataset splits, percentages, or sample counts. |
| Hardware Specification | Yes | The experiments were conducted on a Linux machine with a Xeon 2.53 GHz CPU and 48 GB RAM |
| Software Dependencies | No | The paper mentions the C++ language, the RESQU2 tool, DEPQBF, MINISAT, and ABC, but it does not provide specific version numbers for any of these software dependencies. |
| Experiment Setup | No | The paper does not contain specific hyperparameter values, model initialization details, training schedules, or detailed optimizer settings for the experiments. |