D. Achlioptas, P. Beame, and M. Molloy, A sharp threshold in proof complexity, 33rd STOC, pp.337-346, 2001.

D. Achlioptas, P. Beame, and M. Molloy, Exponential bounds for DPLL below the satisfiability threshold, 15th SODA, pp.139-140, 2004.

G. Audemard and L. Simon, Predicting learnt clauses quality in modern SAT solvers, 21st IJCAI, pp.399-404, 2009.

A. Balint, A. Belov, M. Järvisalo, and C. Sinz, SAT challenge, 2012.

P. Beame, H. Kautz, and A. Sabharwal, Understanding and harnessing the potential of clause learning, JAIR, vol.22, pp.319-351, 2004.

E. Ben-sasson and J. Nordström, Short proofs may be spacious: An optimal separation of space and length in resolution, FOCS, pp.709-718, 2008.

A. Biere, M. J. Heule, H. Van-maaren, and W. , Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, 2009.

A. Biere, Plingeling: Solver description. SAT Challenge, 2012.

B. Bloom, D. Grove, B. Herta, A. Sabharwal, H. Samulowitz et al., SatX10: A scalable plug&play parallel sat framework -(tool presentation), SAT, pp.463-468, 2012.

S. R. Buss, J. Hoffmann, and J. Johannsen, Resolution trees with lemmas: Resolution renements that characterize DLL-algorithms with clause learning, Logical Methods in Computer Science, vol.4, issue.4, p.13, 2008.

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

D. Gangal and A. G. Ranade, Precedence constrained scheduling in (2 ? 7/(3p + 1)) optimal, J. Comput. and Syst. Sc, vol.74, issue.7, pp.1139-1146, 2008.

M. R. Garey, J. , and D. S. , Computers and Intractability: A Guide to the Theory of NP-Completeness, 1979.

Y. Hamadi and C. M. Wintersteiger, Seven challenges in parallel sat solving, 26th AAAI, 2012.

P. Hertel, F. Bacchus, T. Pitassi, and A. V. Gelder, Clause learning can effectively p-simulate general propositional resolution, 23rd AAAI, pp.283-290, 2008.

M. Järvisalo, A. Matsliah, J. Nordström, and S. Zivny, Relating proof complexity measures and practical hardness of sat, CP, pp.316-331, 2012.

M. Järvisalo, D. Le-berre, and O. Roussel, SAT competition, 2011.

D. Kozen, Lower bounds for natural proof systems, 18th Annual Symposium on, pp.254-266, 1977.

J. K. Lenstra, R. Kan, and A. , Complexity of scheduling under precedence constraints, Operations Research, vol.26, pp.22-35, 1978.

K. Pipatsrisawat and A. Darwiche, On the power of clause-learning SAT solvers as resolution engines, AI J, vol.175, issue.2, pp.512-525, 2011.

J. A. Robinson, A machine oriented logic based on the resolution principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.

O. Roussel, Solver description. SAT Challenge 2012. Soos, M. 2012. CryptoMiniSat 2.9, 2012.

A. Urquhart, The depth of resolution proofs, Studia Logica, vol.99, issue.1-3, pp.349-364, 2011.

A. Wotzlaw, A. Van-der-grinten, E. Speckenmeyer, and S. Porschen, Solver description. SAT Challenge, 2012.