Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
From MaRDI portal
Publication:1983330
DOI10.1007/s00037-021-00213-2zbMath1497.03066OpenAlexW3198039724WikidataQ113906241 ScholiaQ113906241MaRDI QIDQ1983330
Danil Sagunov, Petr Smirnov, Artur Riazanov, Dmitry Itsykson
Publication date: 10 September 2021
Published in: Computational Complexity (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00037-021-00213-2
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Related Items (4)
Characterizing Tseitin-Formulas with Short Regular Resolution Refutations ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Reflections on Proof Complexity and Counting Principles ⋮ Characterizing Tseitin-formulas with short regular resolution refutations
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Satisfiability, branch-width and Tseitin tautologies
- Constant-degree graph expansions that preserve treewidth
- The treewidth of line graphs
- Graph multiplication
- Safe separators for treewidth
- Graph minors. I. Excluding a forest
- On embedding graphs in trees
- On the complexity of regular resolution and the Davis-Putnam procedure
- On tseitin formulas, read-once branching programs and treewidth
- Characterizing Tseitin-formulas with short regular resolution refutations
- On digraph coloring problems and treewidth duality
- Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Width and size of regular resolution proofs
- Excluded Grid Theorem
- Size space tradeoffs for resolution
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Short proofs are narrow—resolution made simple
- On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables
- Search Problems in the Decision Tree Model
- Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
- Cops-Robber Games and the Resolution of Tseitin Formulas
- Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
- Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs.
- Towards Tight(er) Bounds for the Excluded Grid Theorem
- Poly-logarithmic Frege depth lower bounds via an expander switching lemma
- Parameterized Algorithms
- Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity
This page was built for publication: Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
