Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Authors: Valeriy Balabanov, Jie-Hong Jiang, Mikolas Janota, Magdalena Widl
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | 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. |