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

DOI10.1016/J.IPL.2009.01.006MaRDI QIDQ987797zbMATH OpenOpenAlexFDO

Authors Wei Chen, Wenhui Zhang

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 complexityproof complexitybinary decision diagramspropositional proof systemspigeonhole problem

Mathematics Subject Classification ID

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

Recommendations

• Ordered binary decision diagrams, pigeonhole formulas and beyond
• scientific article; zbMATH DE number 7250156
• Lower Bounds on OBDD Proofs with Several Orders
• On OBDD-based algorithms and proof systems that dynamically change order of variables
• ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES

Cites work

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

Cited in

(3)

• Ordered binary decision diagrams, pigeonhole formulas and beyond
• ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
• scientific article; zbMATH DE number 7250156 (Why is no real title available?)

Describes a project that uses

Uses Software

• CUDD

This page was built for publication: A direct construction of polynomial-size OBDD proof of pigeon hole problem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q987797)