An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams

DOI10.2178/jsl/1208358751zbMath1141.03028OpenAlexW2062310247MaRDI QIDQ5387310

Jan Krajíček

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

zbMATH Keywords

ordered binary decision diagramslower boundconstraint propagationcommunication complexityproof complexitypropositional proof systemfeasible interpolation

Mathematics Subject Classification ID

Complexity of proofs (03F20)

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