In this question I ask about what use is a solver that can find an assignment that satisfies, say, 90% of the clauses of a known satisfiable 3SAT problem in polynomial time.  The answer seems to be: given a problem  that may or may not be satisfiable, you perform a reduction on an input formula  to another formula  such that  is 90% satisfied iff  is SAT and run my hypothetical algorithm on , which will tell you if  is SAT or not.My question is a follow-up: what is the reduction from  to '?
How to reduce UNSAT problems so that less than $7/8+\epsilon$ of clauses are unsatisfied?
satisfiability
The reference is Hstad's classic paper, Some optimal inapproximability results. It relies on the PCP theorem and on Raz's parallel repetition theorem. The proof is not particularly easy, and even the reduction itself is not so simple to state (if you take into account the PCP component).