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

DOI10.1016/J.IPL.2009.01.006zbMATH Open1217.03044OpenAlexW2035447984MaRDI QIDQ987797FDOQ987797

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

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

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)

Cites Work

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

Cited In (3)

• ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
• Title not available (Why is that?)
• Ordered binary decision diagrams, pigeonhole formulas and beyond

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)