Is there a natural Karp reduction from Independent Set to SAT ? That is, a reduction that does not rely on the Turing machine (as the case in proof of Cook's theorem) but the combinatorial structure.
Yes, just think how you would use a SAT solver to solve the independent set problem.
If you have one variable per node, it should be clear how to write constraints that guarantee that variables that are true indeed form an independent set. I think the only non-trivial part is counting: how to make sure that your independent set is sufficiently large. For that you can use BDD-based techniques; see e.g. Section 5.3 of this paper.