G. Audemard, G. Katsirelos, and L. Simon, A restriction of extended resolution for clause learning sat solvers, AAAI, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00543638

G. Audemard and L. Simon, Gunsat : A greedy local search algorithm for unsatisfiability, IJCAI, pp.2256-2261, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00438054

E. Ben-sasson and A. Wigderson, Short proofs are narrow---resolution made simple, Journal of the ACM, vol.48, issue.2, pp.149-169, 2001.
DOI : 10.1145/375827.375835
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.8383

V. Chvátal and E. Szemerédi, Many hard examples for resolution, Journal of the ACM, vol.35, issue.4, pp.759-768, 1988.
DOI : 10.1145/48014.48016

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

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

A. Haken, The intractability of resolution, Theoretical Computer Science, vol.39, pp.297-308, 1985.
DOI : 10.1016/0304-3975(85)90144-6

J. Huang, Extended clause learning, Artificial Intelligence, vol.174, issue.15, pp.1277-1284, 2010.
DOI : 10.1016/j.artint.2010.07.008
URL : http://doi.org/10.1016/j.artint.2010.07.008

M. Jarvisalo, On the Relative Efficiency of DPLL and OBDDs with Axiom and Join, CP 2011, pp.429-437, 2011.
DOI : 10.1007/978-3-642-23786-7_33

A. Robert, D. Kowalski, and . Kuehner, Linear resolution with selection function, Artif. Intell, vol.2, issue.34, pp.227-260, 1971.

J. Krajicek, Speed-up for propositional frege systems via generalizations of proofs, pp.137-140, 1989.

C. M. Li and A. , Heuristics based on unit propagation for satisfiability problems, IJCAI (1), pp.366-371, 1997.

N. Prcovic, RésolutionRésolutionétendue et largeur de réfutation de formules sat, InSeptì emes Journées Francophones de Programmation par Contraintes, pp.271-280, 2011.

G. S. Tseitin, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logics, pp.115-125, 1968.

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