Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs
DOI10.4230/LIPICS.MFCS.2017.26zbMATH Open1441.68156OpenAlexW2771167559MaRDI QIDQ5111240FDOQ5111240
Ludmila Glinskih, Dmitry Itsykson
Publication date: 26 May 2020
Full work available at URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.26
Recommendations
- On Tseitin formulas, read-once branching programs and treewidth
- On Tseitin formulas, read-once branching programs and treewidth
- No small nondeterministic read-once branching programs for CNFs of bounded treewidth
- Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
- On the read-once property of branching programs and CNFs of bounded treewidth
Graph theory (including graph drawing) in computer science (68R10) Data structures (68P05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Computational aspects of satisfiability (68R07)
Cites Work
- Title not available (Why is that?)
- Branching Programs and Binary Decision Diagrams
- Ramanujan graphs
- Hard examples for resolution
- A lower bound for read-once-only branching programs
- On lower bounds for read-\(k\)-times branching programs
- A note on read-$k$ times branching programs
- Title not available (Why is that?)
- A nondeterministic space-time tradeoff for linear codes
- On multi-partition communication complexity
- Search Problems in the Decision Tree Model
- Title not available (Why is that?)
- On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables
- Poly-logarithmic Frege depth lower bounds via an expander switching lemma
- Lower Bounds for Nondeterministic Semantic Read-Once Branching Programs
- Explicit construction of linear sized tolerant networks. (Reprint)
- Hard examples for bounded depth frege
Cited In (6)
- Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
- Characterizing Tseitin-formulas with short regular resolution refutations
- On tseitin formulas, read-once branching programs and treewidth
- MCSP is hard for read-once nondeterministic branching programs
- Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
- Perspective on complexity measures targeting read-once branching programs
This page was built for publication: Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111240)
