M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

N. Eén and N. Sörensson, An Extensible SAT-solver, Lecture Notes in Computer Science, vol.2919, pp.502-518, 2003.
DOI : 10.1007/978-3-540-24605-3_37

S. Lescuyer and S. Conchon, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Lecture Notes in Computer Science, vol.7, issue.3, pp.287-303, 2009.
DOI : 10.1016/j.jal.2007.07.003
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.1488

S. Yogesh, Z. Mahajan, S. Fu, and . Malik, Zchaff2004: An efficient sat solver, SAT (Selected Papers, pp.360-375, 2004.

T. Weber and H. Amjad, Efficiently checking propositional refutations in HOL theorem provers, Journal of Applied Logic, vol.7, issue.1, pp.26-40, 2009.
DOI : 10.1016/j.jal.2007.07.003