Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
Authors: Alexis de Colnet, Stefan Mengel
JAIR 2023 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we prove that a class of unsatisfiable Tseitin-formulas of bounded degree has regular resolution refutations of polynomial length if and only if the treewidth of all underlying graphs G for that class is in O(log |V (G)|). Our proof first connects the length of regular resolution refutations of unsatisfiable Tseitin-formulas to the size of representations of satisfiable Tseitin-formulas in decomposable negation normal form (DNNF). Then we prove that for every graph G of bounded degree, every DNNF-representation of every satisfiable Tseitin-formula with graph G must have size 2Ω(tw(G)) which yields our lower bound for regular resolution. |
| Researcher Affiliation | Academia | Alexis de Colnet EMAIL Algorithms and Complexity Group, TU Wien Vienna, Austria Stefan Mengel EMAIL Univ. Artois, CNRS Centre de Recherche en Informatique de Lens (CRIL) F-62300 Lens, France |
| Pseudocode | No | The paper does not contain any structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide any concrete access to source code for the methodology described. |
| Open Datasets | No | The paper is theoretical and does not use or reference any specific datasets for empirical evaluation. |
| Dataset Splits | No | The paper is theoretical and does not involve experimental evaluation with dataset splits. |
| Hardware Specification | No | The paper is theoretical and does not describe any experimental setup that would require hardware specifications. |
| Software Dependencies | No | The paper is theoretical and does not mention specific software dependencies or versions. |
| Experiment Setup | No | The paper is theoretical and does not describe any experimental setup or training configurations. |