A. Atserias, G. Phokion, M. Y. Kolaitis, and . Vardi, Principles and Practice of Constraint Programming -CP, Lecture Notes in Computer Science, vol.3258, pp.77-91, 2004.

P. Beame, T. Pitassi, and N. Segerlind, Lower Bounds for Lovász-Schrijver Systems and Beyond Follow from Multiparty Communication Complexity, SIAM J. Comput, vol.37, issue.3, pp.845-869, 2007.

R. E. Bryant, Symbolic manipulation of boolean functions using a graphical representation, Proceedings of the 22nd ACM/IEEE conference on Design automation, DAC 1985, pp.688-694, 1985.

W. Chén and W. Zhang, A direct construction of polynomial-size OBDD proof of pigeon hole problem, Information Processing Letters, vol.109, issue.10, pp.472-477, 2009.

P. Duris, J. Hromkovic, S. Jukna, M. Sauerhoff, and G. Schnitger, On multi-partition communication complexity, Inf. Comput, vol.194, issue.1, pp.49-75, 2004.

L. Friedman and Y. Xu, Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams, Lecture Notes in Computer Science, vol.7913, pp.127-138, 2013.

. Springer, , 2013.

R. G. Gallager, Low-density parity-check codes. Information Theory, IRE Transactions on, vol.8, pp.21-28, 1962.

J. Friso-groote and H. Zantema, Resolution and binary decision diagrams cannot simulate each other polynomially, Discrete Applied Mathematics, vol.130, issue.2, pp.157-171, 2003.

V. Guruswami, List decoding from erasures: bounds and code constructions. Information Theory, IEEE Transactions on, vol.49, issue.11, pp.2826-2833, 2003.

J. Krají?ek, An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams, Journal of Symbolic Logic, vol.73, issue.1, pp.227-237, 2008.

E. Kushilevitz and N. Nisan, Communication complexity, 1997.

A. Lubotzky, R. Phillips, and P. Sarnak, Ramanujan graphs, Combinatorica, vol.8, issue.3, pp.261-277, 1988.

C. Meinel and A. Slobodova, On the complexity of Constructing Optimal Ordered Binary Decision Diagrams, Proceedings of Mathematical Foundations of Computer Science, vol.841, pp.515-524, 1994.

C. Meinel and T. Theobald, Algorithms and Data Structures in VLSI Design: OBDD -Foundations and Applications, 1998.

G. Pan and M. Y. Vardi, Symbolic Techniques in Satisfiability Solving, 7th International Conference on Theory and Applications of Satisfiability Testing, vol.3542, pp.235-250, 2004.

N. Segerlind, Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability, 2007.

, On OBDD-Based Algorithms and Proof Systems That Change Order of Variables

N. Segerlind, On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs, Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, pp.100-111, 2008.

O. Tveretina, C. Sinz, and H. Zantema, An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas, Proceedings Fourth Athens Colloquium on Algorithms and Complexity, vol.4, pp.13-21, 2009.

A. Urquhart, Hard Examples for Resolution, JACM, vol.34, issue.1, pp.209-219, 1987.