# How to reduce UNSAT problems so that less than $7/8+\epsilon$ of clauses are unsatisfied?

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 ϕ'?