Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs.

DOI10.4230/LIPIcs.MFCS.2017.26zbMath1441.68156OpenAlexW2771167559MaRDI QIDQ5111240

Ludmila Glinskih, Dmitry Itsykson

Publication date: 26 May 2020

Full work available at URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.26

zbMATH Keywords

expanderread-once branching programTseitin formula

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Data structures (68P05) Computational aspects of satisfiability (68R07)

Related Items (5)

Characterizing Tseitin-Formulas with Short Regular Resolution Refutations ⋮ MCSP is hard for read-once nondeterministic branching programs ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ On tseitin formulas, read-once branching programs and treewidth ⋮ Characterizing Tseitin-formulas with short regular resolution refutations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A nondeterministic space-time tradeoff for linear codes
• A lower bound for read-once-only branching programs
• Ramanujan graphs
• On multi-partition communication complexity
• On lower bounds for read-\(k\)-times branching programs
• Explicit construction of linear sized tolerant networks. (Reprint)
• Hard examples for bounded depth frege
• Hard examples for resolution
• A note on read-$k$ times branching programs
• Branching Programs and Binary Decision Diagrams
• Lower Bounds for Nondeterministic Semantic Read-Once Branching Programs
• On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables
• Search Problems in the Decision Tree Model
• Poly-logarithmic Frege depth lower bounds via an expander switching lemma

This page was built for publication: Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs.