(3,4)-SAT is satisfiability restricted to formulas in which every clause contains exactly three literals and every variable occurs at most four times. Tovey proved that it is NP-hard: every language in NP has a polynomial-time many-one reduction to it.

[2,3]-bounded 3-SAT asks whether a formula is satisfiable, where every clause has two or three literals and every literal, a variable together with a sign, occurs at most twice. A variable therefore occurs at most twice positively and at most twice negatively, so in at most four clauses. The problem is NP-hard: every language in NP has a polynomial-time many-one reduction to it.

Tovey's paper states its theorem for (3,4)-SAT ($ThreeFourSat$). This is the variant that the scheduling reductions start from, and it follows from the (3,4) case by one more reduction, given in $Copies$.

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$ of a variable $v$ is replaced by a fresh variable $w_{v,p}$. A clause is chained 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. Afterwards every clause has at most three literals and every variable occurs at most three times.

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

On words, the reduction decodes a formula, applies the two steps and encodes the result. A word that encodes no formula is treated as the formula consisting of one empty clause.

A (3,4) formula with $C$ clauses has $3C$ literal positions; position $p = 3c + t$ holds the $t$-th literal of clause $c$. Let $V$ be a strict bound on its variables. The construction gives every position $p$ its own variable $x_p = v + pV$, where $v$ is the variable at that position, and produces two kinds of clauses.

• The clauses of three literals are the original clauses, with each literal replaced by the copy for its position and keeping its sign.
• The clauses of two literals are the implications $x_{v,p+1} \to x_{v,p}$, that is $(x_{v,p} \vee \neg x_{v,p+1})$, for every variable $v < V$ and every position $p$, with positions taken cyclically. These chain the copies of $v$ around a cycle, so they all take the same value. They are the cycle clauses of the first reduction.

Every literal of the result occurs at most twice. A copy belongs to one position only, so it appears in at most one clause of three literals, and with one sign. In the cycle of its variable it is the consequent of one implication and the antecedent of another, which gives it one positive and one negative occurrence there.

On words, the reduction is the first reduction followed by this construction: a word is sent to the encoding of a (3,4) formula, that formula is decoded, and the construction is applied to it and written in the self-delimiting code.