Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs

DOI10.4230/LIPICS.MFCS.2017.26MaRDI QIDQ5111240zbMATH OpenOpenAlexFDO

Authors 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) Data structures (68P05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Computational aspects of satisfiability (68R07)

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

Cites work

• scientific article; zbMATH DE number 5161489 (Why is no real title available?)
• scientific article; zbMATH DE number 1775455 (Why is no real title available?)
• scientific article; zbMATH DE number 3337135 (Why is no real title available?)
• A lower bound for read-once-only branching programs
• A nondeterministic space-time tradeoff for linear codes
• A note on read-$k$ times branching programs
• Branching Programs and Binary Decision Diagrams
• Explicit construction of linear sized tolerant networks. (Reprint)
• Hard examples for bounded depth frege
• Hard examples for resolution
• Lower bounds for nondeterministic semantic read-once branching programs
• On OBDD-based algorithms and proof systems that dynamically change order of variables
• On lower bounds for read-\(k\)-times branching programs
• On multi-partition communication complexity
• Poly-logarithmic Frege depth lower bounds via an expander switching lemma
• Ramanujan graphs
• Search Problems in the Decision Tree Model

Cited in

(8)

• 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
• 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
• No small nondeterministic read-once branching programs for CNFs of bounded treewidth
• 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)