I've been reading the "Inapproximability of Combinatorial Optimization Problems" by Luca Trevisan (see: link). On pages 3-4 it mentions that a polynomial time algorithm for 3SAT would exist if there were a 2-approximate algorithm for the independent set problem and also a reduction from 3SAT to IS such that for some k: if the optimal solution to the reduced IS graph is greater than or equal to k, then the 3SAT instance is satisfiable and if the 3SAT instance is not satisfiable, then the optimal solution to the reduced IS graph is less than k/2.
I'm not interested in whether or not a 2-approximate algorithm for IS exists or is even possible. Rather, I'm wondering if there exists such a reduction from 3SAT to IS as described. If not, what sort of non-trivial properties would need to hold in such a reduction? That is to say, does there exist any literature regarding the approach one would take towards developing such a reduction?