(3,4)-SAT is satisfiability restricted to formulas in which every clause has exactly three literals and every variable occurs at most four times. Tovey (1984, Theorem 2.3) proved that it is NP-hard. This submission proves that theorem: every language in NP has a polynomial-time many-one reduction to (3,4)-SAT, on the CNF encoding and the Turing machines of the archive's Cook–Levin theorem.

The reduction starts from unrestricted satisfiability. Every literal occurrence gets a fresh variable, and a cycle of implications forces the copies of one variable to take the same value. Each clause is then broken up through link variables into a chain of clauses of at most three literals. Finally every clause with fewer than three literals is filled up with the negation of a fresh variable, which a private copy of Tovey's thirteen-clause gadget forces to be true.

Following the archive's convention for reductions, the concepts state the construction as definitions, then its correctness, then its running time. The reduction is proved correct and proved to run in polynomial time: it is a program for the archive's word RAM, and polynomial time on the word RAM transfers to Turing machines.

The submission also proves the variant that the scheduling reductions start from, [2,3]-bounded 3-SAT: every clause has two or three literals and every literal occurs at most twice. It is NP-hard on the self-delimiting binary encoding of formulas that the scheduling submissions read. The reduction is from (3,4)-SAT. Every literal position of the formula gets its own variable, so no variable occurs more than once among the clauses of three literals, and the copies of an original variable are tied together by a cycle of two-literal implications, in which every copy occurs once positively and once negatively. This second step is proved correct on formulas whose clauses all have three literals, which is what the first reduction produces, and its word RAM program is proved to run in polynomial time. Neither reduction has a parameter, so there is no parameter bound to prove.