. Boros, Maximum renamable Horn sub-CNFs, Discrete Applied Mathematics, vol.96, issue.97, p.96, 1999.
DOI : 10.1016/S0166-218X(99)00031-1

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

E. Giunchiglia, M. , and A. Tacchella, Dependent and independent variables in propositional satisfiability Automatic extraction of functional dependencies, JELIA'2002 proc. of SAT, pp.296-307, 2002.

A. Edward and . Hirsch, A new algorithm for MAX- 2-SAT, Lecture Notes in Computer Science, vol.1770, pp.65-73, 2000.

H. Kautz, D. Mcallester, and B. Selman, Exploiting the variable dependency in local search, International Joint Conference on Artificial Intelligence (IJCAI'1997, 1997.

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

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, 2004.

. H. Ch and . Papadimitriou, Computational complexity, 1994.

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.