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

K. Iwama, Complexity of finding short resolution proofs, MFCS, pp.309-318, 1997.
DOI : 10.1007/BFb0029974

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

D. W. Loveland, A linear format for resolution, Symposium on Automatic Demonstration, pp.143-163, 1970.

S. David, P. , and I. Lynce, Local search for unsatisfiability, SAT, pp.283-296, 2006.

B. Selman, H. A. Kautz, and D. A. Mcallester, Ten challenges in propositional reasoning and search, IJCAI (1), pp.50-54, 1997.