Improved Separations of Regular Resolution from Clause Learning Proof Systems
Authors: M. L. Bonet, S. Buss, J. Johannsen
JAIR 2014 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | This paper studies the relationship between resolution and conflict driven clause learning (CDCL) without restarts, and refutes some conjectured possible separations. We prove that the guarded, xor-ified pebbling tautology clauses, which Urquhart proved are hard for regular resolution, as well as the guarded graph tautology clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. For the latter set of clauses, we extend this to prove that a CDCL search without restarts can refute these clauses in polynomial time, provided it makes the right choices for decision literals and clause learning. |
| Researcher Affiliation | Academia | Maria Luisa Bonet EMAIL Lenguajes y Sistemas Inform aticos, Universidad Polit ecnica de Catalu na, Barcelona, Spain Sam Buss EMAIL Department of Mathematics, University of California, San Diego, La Jolla, CA 92093-0112, USA Jan Johannsen EMAIL Institut f ur Informatik, Ludwig-Maximilians Universit at M unchen, D-80538 M unchen, Germany |
| Pseudocode | No | The paper describes algorithms and procedures in descriptive text, such as: "We will give a direct description of the CDCL search. The search initially chooses to set the literals x1,0, x2,1 . . ., xn 2,n 3 true as decision literals, in that order, so xi+1,i is set true at (decision) level i + 1." However, it does not provide any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not contain any explicit statements about releasing source code or links to a code repository for the methodology described. |
| Open Datasets | No | The paper deals with theoretical constructs such as "pebbling tautology clauses Peb(G)" and "graph tautology clauses GTn", not empirical datasets. Therefore, there is no mention of publicly available datasets. |
| Dataset Splits | No | The paper is theoretical and does not involve experiments with datasets, so there is no information about dataset splits. |
| Hardware Specification | No | The paper does not describe any specific hardware used for running experiments, as the research is theoretical. |
| Software Dependencies | No | The paper mentions "conflict-driven clause learning (CDCL) based on the work of Marques Silva and Sakallah (1999)" and "DPLL (Davis-Putnam-Logemann Loveland) search procedure", but does not specify any particular software or library names with version numbers used in the authors' work. |
| Experiment Setup | No | The paper is purely theoretical, focusing on mathematical proofs and algorithms. It does not describe any experimental setup details, hyperparameters, or training configurations. |