S. A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing , STOC '71, pp.151-158, 1971.
DOI : 10.1145/800157.805047

S. Darras, G. Dequen, L. Devendeville, B. Mazure, R. Ostrowski et al., Using Boolean Constraint Propagation for Sub-clauses Deduction, Proceedings of the Eleventh International Conference on Principles and Practice of Constraint Programming (CP'05), pp.757-761, 2005.
DOI : 10.1007/11564751_59

M. Davis, G. Logemann, and D. W. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

W. H. Dowling and J. H. Gallier, Linear-time algorithms for testing the satisfiability of propositional horn formulae, The Journal of Logic Programming, vol.1, issue.3, pp.267-284, 1984.
DOI : 10.1016/0743-1066(84)90014-1

O. Dubois, P. André, Y. Boufkhad, and J. Carlier, Second DIMACS implementation challenge : cliques, coloring and satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, chapter SAT vs. UNSAT, pp.415-436, 1996.

O. Dubois and G. Dequen, A backbone-search heuristic for efficient solving of hard 3-SAT formulae, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01), pp.248-253, 2001.

S. Even, A. Itai, and A. Shamir, On the Complexity of Timetable and Multicommodity Flow Problems, SIAM Journal on Computing, vol.5, issue.4, pp.691-703, 1976.
DOI : 10.1137/0205048

N. Eén and A. Biere, Effective preprocessing in SAT through variable and clause elimination, Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT'05), pp.61-75, 2005.

N. Eén, N. Sörensson12, ´. E. Grégoire, B. Mazure, C. Piette et al., An extensible SATsolver Extracting MUSes Automatic extraction of functional dependencies, Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03) Proceedings of the 17th European Conference on Artificial Intelligence (ECAI'06) Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04), pp.502-518, 2003.

D. and L. Berre, Exploiting the real power of unit propagation lookahead, Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT'01), 2001.
DOI : 10.1016/S1571-0653(04)00314-2

C. M. Li and A. , Heuristics based on unit propagation for satisfiability problems, Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), pp.366-371, 1997.

P. Liberatore, The complexity of checking redundancy of CNF propositional formulae [17] P. Liberatore. Redundancy in logic i : CNF propositional formulae, Proceedings of the 15th European Conference on Artificial Intelligence (ECAI'02), pp.262-266203, 2002.

P. Marquis, Knowledge compilation using theory prime implicates, Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI'95), pp.837-843, 1995.

B. Mazure and P. Marquis, Theory reasoning within implicant cover compilations, Proceedings of the ECAI-96 Workshop on Advances in Propositional Deduction, pp.65-69, 1996.

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

R. Ostrowski, B. Mazure, L. Sa¨?ssa¨?s, and . Grégoire, Eliminating redundancies in SAT search trees, Proceedings. 15th IEEE International Conference on Tools with Artificial Intelligence, pp.100-104, 2003.
DOI : 10.1109/TAI.2003.1250176

S. Sathiamoorthy, K. P. Dhiraj, and . Niver, Nonincreasing variable elimination resolution for preprocessing SAT instances, Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04), pp.276-291, 2004.

B. Selman and H. A. Kautz, Knowledge compilation using horn approximations, Proceedings of the Ninth National Conference on Artificial Intelligence (AAAI'91), pp.904-909, 1991.

B. Selman, H. J. Levesque, and D. G. Mitchell, A new method for solving hard satisfiability problems, Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI'92), pp.440-446, 1992.

R. E. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

R. Williams, C. P. Gomes, and B. Selman, Backdoors to typical case complexity, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI'03), pp.1173-1178, 2003.

W. Zhang, Configuration landscape analysis and backbone guided local search., Artificial Intelligence, vol.158, issue.1, pp.1-26, 2004.
DOI : 10.1016/j.artint.2004.04.001
URL : http://doi.org/10.1016/j.artint.2004.04.001