G. Audemard, B. Benhamou, and P. Siegel, AVAL: An Enumerative Method for SAT, Proceedings of first international conference on computational logic CL00, pp.373-383, 2000.
DOI : 10.1007/3-540-44957-4_25

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.8188

E. Benoist and J. Hébrard, Ordered formulas, 1999.

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

O. Dubois and G. Dequen, A backbonesearch heuristic for efficient solving of hard 3? sat formulae, Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI?01), 2001.

´. E. Grégoire, B. Mazure, R. Ostrowski, and L. Sa¨?ssa¨?s, Automatic Extraction of Functional Dependencies, proc. of SAT, pp.122-132, 2005.
DOI : 10.1007/11527695_10

P. Kilby, J. Slaney, S. Thiebaux, and T. Walsh, Backbones and backdoors in satisfiability, AAAI'2005, 2005.

I. Lynce and J. P. Marques-silva, Hidden structure in unsatisfiable random 3-SAT: an empirical study, 16th IEEE International Conference on Tools with Artificial Intelligence, 2004.
DOI : 10.1109/ICTAI.2004.68

H. Van-maaren and L. Van-norden, Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances, Annals of Mathematics and Artificial Intelligence, vol.37, issue.4, pp.157-177, 2005.
DOI : 10.1007/s10472-005-2369-1

B. Mazure and L. Sa¨?ssa¨?s, Tabu search for SAT, Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI-97/IAAI-97), pp.281-285, 1997.

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

N. Nishimura, P. Ragde, and S. Szieder, Detecting backdoor sets with respect to horn and binary clauses, 7th International Conference on theory and Application of Satisfiability Testing (SAT'04), 2004.

L. Paris, R. Ostrowski, P. Siegel, and L. Sa¨?ssa¨?s, Computing and exploiting horn strong backdoor sets thanks to local search, Proceedings of the 18th International Conference on Tools with Artificial Intelligence (IC- TAI'2006), pp.139-143, 2006.
DOI : 10.1109/ictai.2006.43

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.2542

B. Selman and H. A. Kautz, An empirical study of greedy local search for satisfiability testing, 1993.

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.

R. Williams, C. Gomes, and B. Selman, Backdoors to typical case complexity, Procceding of Intenrational Joint Conference on Artificial Intelligence (IJCAI'2003), 2003.

R. Williams, C. Gomes, and B. Selman, On the connections between heavy-tails, backdoors , and restarts in combinatorial search, International Conference on Theory and Applications of Satisfiability Testing (SAT'2003), 2003.