A direct construction of polynomial-size OBDD proof of pigeon hole problem

DOI10.1016/j.ipl.2009.01.006zbMath1217.03044OpenAlexW2035447984MaRDI QIDQ987797

Wen-Hui Zhang, Wei Chen

Publication date: 16 August 2010

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2009.01.006

zbMATH Keywords

computational complexitypropositional proof systemsbinary decision diagramsproof complexitypigeonhole problem

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of proofs (03F20)

Related Items

ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES, Unnamed Item

Uses Software

• CUDD

Cites Work

• On the complexity of cutting-plane proofs
• Symbolic techniques in satisfiability solving
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Graph-Based Algorithms for Boolean Function Manipulation
• The relative efficiency of propositional proof systems
• Branching Programs and Binary Decision Diagrams
• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
• Principles and Practice of Constraint Programming – CP 2004