P. Beame, H. A. Kautz, and A. Sabharwal, Understanding the power of clause learning, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI'03), pp.1194-1201, 2003.

B. Benhamou and L. Sa¨?ssa¨?s, Tractability through symmetries in propositional calculus, Journal of Automated Reasoning, vol.8, issue.1, pp.89-102, 1994.
DOI : 10.1007/BF00881844
URL : https://hal.archives-ouvertes.fr/hal-01479609

A. Stephen and . Cook, A short proof of the pigeon hole principle using extended resolution, pp.28-32, 1976.

J. Crawford, M. L. Ginsberg, E. Luck, and A. Roy, Symmetrybreaking predicates for search problems, Principles of Knowledge Representation and Reasoning (KR'96), pp.148-159, 1996.

M. Davis, G. Logemann, and D. W. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

N. Eén and A. Biere, Effective preprocessing in SAT through variable and clause elimination, Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT'05), pp.61-75, 2005.

N. Eén and N. Sörensson, An extensible sat-solver, Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03), pp.502-518, 2002.

P. Flener, J. Pearson, M. Sellmann, P. Van-hentenryck, and M. Magnusågren, Dynamic structural symmetry breaking for constraint satisfaction problems, Constraints, vol.14, issue.4, pp.506-538, 2009.
DOI : 10.1007/s10601-008-9059-7

P. Ian, B. Gent, and . Smith, Symmetry breaking in constraint programming, Proceedings of the Thirteenth European Conference on Artificial Intelligence(ECAI'00), pp.599-603, 2000.

C. P. Gomes, B. Selman, H. Kautz, ´. E. Grégoire, R. Ostrowski et al., Boosting combinatorial search through randomization Automatic extraction of functional dependencies, Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI'97) Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04), pp.431-437, 1998.

A. Haken-]-h, E. Kautz, Y. Horvitz, C. Ruan, B. Gomes et al., The intractability of resolution, Proceedings of the Eighteenth National Conference on Artificial Intelligence (AAAI'02), pp.297-308, 1985.
DOI : 10.1016/0304-3975(85)90144-6

B. Krishnamurthy, Short proofs for tricky formulas, Acta Informatica, vol.22, issue.3, pp.253-275, 1985.
DOI : 10.1007/BF00265682

. Moll, Examples of hard tautologies in the propositional calculus, Proceedings of the 13th Annual ACM Symposium on Theory of Computing (STOC'81), pp.28-37, 1981.

P. Joao, K. A. Marques-silva, and . Sakallah, GRASP -A New Search Algorithm for Satisfiability, Proceedings of IEEE/ACM International Conference on Computer-Aided Design, pp.220-227, 1996.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

]. R. Ostrowski, ´. E. Grégoire, B. Mazure, and L. Sa¨?ssa¨?s, Recovering and Exploiting Structural Knowledge from CNF Formulas, Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming(CP'02), pp.185-199, 2002.
DOI : 10.1007/3-540-46135-3_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.130.8117

K. Pipatsrisawat and A. Darwiche, On the Power of Clause-Learning SAT Solvers with Restarts, CP, pp.654-668, 2009.
DOI : 10.1007/11591191_40

J. Puget, On the satisfiability of symmetrical constrained satisfaction problems, Proceedings of the 7th International Symposium on Methodologies for Intelligent Systems (ISMIS'93), pp.350-361, 1993.
DOI : 10.1007/3-540-56804-2_33

G. S. Tseitin, On the complexity of derivations in the propositional calculus, Structures in Constructives Mathematics and Mathematical Logic, Part II, pp.115-125, 1968.