A CNF formula $F$ with $N$ literal occurrences over variables below $V$ is turned into a (3,4) formula in two steps.

Splitting. The occurrence at position $p$ is replaced by a fresh variable $w_{v,p}$, where $v$ is the variable occurring there. A clause becomes a chain through link variables $z_p$: the clause $(l_0 \vee \dots \vee l_{L-1})$ becomes $(l_0 \vee z_0), (\bar z_0 \vee l_1 \vee z_1), \dots, (\bar z_{L-2} \vee l_{L-1})$, and an empty clause stays empty. For every $v$ the implications $w_{v,p+1} \to w_{v,p}$, taken cyclically over all positions, force the copies of $v$ to agree. Clauses now have at most three literals and every variable occurs at most three times.

Padding. Every clause with fewer than three literals is filled with literals $\bar y$, each on a fresh variable $y$ that a private copy of Tovey's gadget forces to be true. The gadget has thirteen clauses on $y$ and nine further variables; $y$ occurs three times in it and every other variable four times.

The reduction on words decodes a formula, applies the two steps and encodes the result; a word that encodes no formula is treated as the formula with one empty clause.