Suppose x and y are configurations of an NTM M, where <x> and <y> both
have length m.  (If necessary, "pad" them out to length m with zeros.)
Then we can quickly decide whether x yields y by reading <x> and <y>
and consulting the transition table of M.

The statement that "x yields y" can be translated into a Boolean
expression in 2m variables, b^x_1, b^x_2, ... b^x_m, b^y_1, ... b^y_m.
This Boolean expression, which uses the usual Boolean operators along
with those variables, simply states that there is a valid transition
which changes x to y.  The length of this Boolean expression is O(m),
where the constant depends on M.

Suppose X = (x_0, x_1, ... x_t) is a sequence of configurations of M,
where each <x_i> has length exactly m.  (Pad if necessary.)
Then the statement that "X is an accepting computation of M with input w"
can be written as a Boolean expression (t+1)m variables.  This Boolean
expression consists of clauses stating that x_0 is the start configuration
with input w, that x_{i-1} yields x_i for each i, and that x_t is an
accepting configuration.  The length of this Boolean expression is O(tm).

The Reduction.  Fix an NTM M.  Then there is a function R, actually
a reduction, such that, given any input string w and integers m and t,
returns a Boolean expression R(w,m,t) which is satisfiable if and only
if there is an accepting computation of M with input w where the encoding
of each configuration has length at most m, and the computation takes
at most t steps.  (We can pad the time, as well.)