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

Viewing OBDD from the explicit perspective of a propositional proof system is first proposed and studied in A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77-91]. It has been shown that OBDD proof system defined in A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77-91] is strictly stronger than resolution and can polynomially simulate cutting plane proof system with small coefficients CP^∗. It is already shown in W. Cook, C.R. Coullard, G. Turán, On the complexity of cutting-plane proofs, Discrete Appl. Math. 18 (1) (1987) 25-38] that there exists polynomial-size proof for pigeon hole problem of cutting plane proof system. Then it follows directly that there exists polynomial-size proof for of OBDD proof system. However, this is an indirect result. Atserias et al. A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77-91] call for the need of a direct construction. Hereby we present such construction. Moreover, in this construction we do not need the weakening rule introduced in A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77-91]. We believe this may shed some light on the understanding of the role of the weakening rule.