R. I. Brafman, A Simplifier for Propositional Formulas With Many Binary Clauses, 17th International Joint Conference on Artificial Intelligence (IJCAI'01), pp.515-522, 2001.
DOI : 10.1109/TSMCB.2002.805807

A. Stephen, D. G. Cook, and . Mitchell, Finding hard instances of the satisfiability problem : A survey, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.35, 1997.

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

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

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

O. Fourdrinoy, E. Grégoire, B. Mazure, and L. Sais, Eliminating Redundant Clauses in SAT Instances, Proceedings of The Fourth International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CP-AI-OR'07), pp.71-83, 2007.
DOI : 10.1007/978-3-540-72397-4_6

URL : https://hal.archives-ouvertes.fr/hal-00199309

A. Hertel, P. Hertel, and A. Urquhart, Formalizing Dangerous SAT Encodings, 10th International Conference on Theory and Applications of Satisfiability Testing (SAT'07), pp.159-172, 2007.
DOI : 10.1007/978-3-540-72788-0_18

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

G. Robert, J. Jeroslow, and . Wang, Solving propositional satisfiability problems, Annals of mathematics and artificial intelligence, vol.1, pp.167-187, 1990.

C. Li and A. , Look-ahead versus look-back for satisfiability problems, Proceedings of the Third International Conference of Principles and Practice of Constraint Programming (CP'97), pp.341-355, 1997.
DOI : 10.1007/BFb0017450

P. Liberatore, Redundancy in logic I: CNF propositional formulae, Artificial Intelligence, vol.163, issue.2, pp.203-232, 2005.
DOI : 10.1016/j.artint.2004.11.002

K. Pipatsrisawat and A. Darwiche, RSAT 2.0 : SAT solver description, 2007.

S. Subbarayan and D. Pradhan, NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances, 7th International Conference on Theory and Applications of Satisfiability Testing Conference (SAT'04), pp.276-291, 2004.
DOI : 10.1007/11527695_22