N. Alon and F. R. Chung, Explicit construction of linear sized tolerant networks, Discrete Mathematics, vol.306, issue.10-11, pp.1068-1071, 2006.

A. Atserias, P. G. Kolaitis, and M. Y. Vardi, Constraint Propagation as a Proof System, Principles and Practice of Constraint Programming ? CP 2004, 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 Journal on Computing, vol.37, issue.3, pp.845-869, 2007.

S. Buss, D. Itsykson, A. Knop, and D. Sokolov, Reordering rule makes OBDD proof systems stronger, 33rd Computational Complexity Conference, CCC 2018, vol.16, p.24, 2018.

J. Cheeger, A Lower Bound for the Smallest Eigenvalue of the Laplacian, Problems in Analysis: A Symposium in Honor of Salomon Bochner (PMS-31), pp.195-200, 2015.

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.

A. Stephen, R. A. Cook, and . Reckhow, The relative efficiency of propositional proof systems, The Journal of Symbolic Logic, vol.44, issue.1, pp.36-50, 1979.

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, Computer Science ? Theory and Applications, vol.7913, pp.127-138, 2013.

G. Robert and . Gallager, Low-density parity-check codes, Information Theory, IRE Transactions on, vol.8, issue.1, 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, IEEE Transactions on Information Theory, vol.49, issue.11, pp.2826-2833, 2003.

S. Hoory, N. Linial, and A. Wigderson, Expander graphs and their applications, Bulletin of the American Mathematical Society, vol.43, issue.04, pp.439-562, 2006.

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, 1996.

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

C. Meinel and A. Slobodová, On the complexity of constructing optimal ordered binary decision diagrams, Mathematical Foundations of Computer Science 1994, vol.841, pp.515-524, 1994.

C. Meinel and T. Theobald, Algorithms and Data Structures in VLSI Design, 1998.

G. Pan and M. Y. Vardi, Search vs. Symbolic Techniques in Satisfiability Solving, Theory and Applications of Satisfiability Testing, vol.3542, pp.235-250, 2005.

N. Segerlind, Nearly-exponential size lower bounds for symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability, 2007.

N. Segerlind, On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs, 2008 23rd Annual IEEE Conference on Computational Complexity, 2008.

O. Tveretina, C. Sinz, and H. Zantema, An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas, Electronic Proceedings in Theoretical Computer Science, vol.4, pp.13-21, 2009.

A. Urquhart, Hard examples for resolution, Journal of the ACM, vol.34, issue.1, pp.209-219, 1987.

I. Wegener, Branching Programs and Binary Decision Diagrams, 2000.

G. Zémor, On expander codes, IEEE Transactions on Information Theory, vol.47, issue.2, pp.835-837, 2001.