 Seven-clause gadget for MAX-2SAT

A three-literal disjunction can be represented by ten unit or two-literal clause occurrences with one fresh auxiliary variable. If the number $r$ of true input literals is zero, the best auxiliary choice satisfies six; for $r=1,2,3$, the best count is seven. Applying separate gadgets to all clauses of a 3-SAT instance gives target seven times the original clause count, proving NP-completeness of the decision form of MAX-2SAT. The local counting argument is essential: no gadget may exceed seven and compensate for an unsatisfied input clause.