An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
From MaRDI portal
Publication:5387310
DOI10.2178/jsl/1208358751zbMath1141.03028OpenAlexW2062310247MaRDI QIDQ5387310
Publication date: 8 May 2008
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://projecteuclid.org/euclid.jsl/1208358751
ordered binary decision diagramslower boundconstraint propagationcommunication complexityproof complexitypropositional proof systemfeasible interpolation
Related Items
Dag-like communication and its applications ⋮ Characterizing Propositional Proofs as Noncommutative Formulas ⋮ Towards NP-P via proof complexity and search ⋮ A note on SAT algorithms and proof complexity ⋮ Algebraic proofs over noncommutative formulas ⋮ ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES ⋮ Resolution over linear equations and multilinear proofs ⋮ A form of feasible interpolation for constant depth Frege systems ⋮ The complexity of the Hajós calculus for planar graphs ⋮ A direct construction of polynomial-size OBDD proof of pigeon hole problem ⋮ Unnamed Item ⋮ Resolution over linear equations modulo two
Cites Work
- The monotone circuit complexity of Boolean functions
- On the weak pigeonhole principle
- The relative efficiency of propositional proof systems
- Lower bounds to the size of constant-depth propositional proofs
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Branching Programs and Binary Decision Diagrams
This page was built for publication: An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams