R. J. Bayardo and R. C. Schrag, Using csp lookback techniques to solve real-world sat instances, Proceedings of the Fourteenth National Conference on Artificial Intelligence, pp.203-207, 1997.
DOI : 10.1007/3-540-61551-2_65
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.9830

P. Beame, H. Kautz, and A. Sabharwal, Towards understanding and harnessing the potential of clause learning, Journal of Artificial Intelligence Research, vol.22, pp.319-351, 2004.

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

P. Chatalic and L. Simon, MULTIRESOLUTION FOR SAT CHECKING, International Journal on Artificial Intelligence Tools, vol.10, issue.04, pp.451-481, 2001.
DOI : 10.1142/S0218213001000611

A. Stephen and . Cook, A short proof of the pigeon hole principle using extended resolution, SIGACT News, vol.8, issue.4, pp.28-32, 1976.

M. Davis, G. Logemann, and D. 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 N. Sörensson, An extensible SAT-solver, proceedings of SAT, pp.502-518, 2003.

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

P. Hertel, F. Bacchus, T. Pitassi, and A. Van-gelder, Clause learning can effectively psimulate general propositional resolution, Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI-2008), pp.283-290, 2008.

J. Huang, The effect of restarts on the efficiency of clause learning, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, pp.2318-2323, 2007.

J. P. Silva and K. A. Sakallah, GRASP: a search algorithm for propositional satisfiability, IEEE Transactions on Computers, vol.48, issue.5, pp.506-521, 1999.
DOI : 10.1109/12.769433

M. Moskewicz, C. 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

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

M. Prasad, A. Biere, and A. Gupta, A survey of recent advances in SAT-based formal verification, International Journal on Software Tools for Technology Transfer, vol.35, issue.2, pp.156-173, 2005.
DOI : 10.1007/s10009-004-0183-4

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

B. Schaafsma, M. Heule, and H. Van-maaren, Dynamic Symmetry Breaking by Simulating Zykov Contraction, Theory and Applications of Satisfiability Testing -SAT 2009, pp.223-236, 2009.
DOI : 10.1016/j.dam.2006.07.016
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.9222

C. Sinz and A. Biere, Extended Resolution Proofs for Conjoining BDDs, Lecture Notes in Computer Science, vol.3967, pp.600-611, 2006.
DOI : 10.1007/11753728_60
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.331.1175

G. Tseitin, On the complexity of proofs in propositional logics Automation of Reasoning : Classical Papers in Computational Logic, 1967.

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

A. Urquhart, The complexity of propositional proofs, pp.332-342, 2001.

A. Van-gelder, Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning, Logic for Programming, Artificial Intelligence , and Reasoning, pp.580-594, 2005.
DOI : 10.1007/11591191_40

L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of IEEE/ACM International Conference on Computer Design (ICCAD), pp.279-285, 2001.