Given a term \(t\) (a conjunction of literals) and a restriction \(\rho \), this is the list of literals of \(t\) whose underlying variable is still free under \(\rho \), i.e. the sublist of \(t\) obtained by keeping those literals \(l\) with \(l.\mathrm{var} \in \rho .\mathrm{freeVars}\).

Consumes the free literals of a single clause (each paired with its position index) against the canonical decision-tree path, one path entry per literal. For each free literal it fixes the literal’s variable to its satisfying direction in \(\sigma \), records the path direction in \(\rho _0\) (mirroring the canonical decision-tree branching), and appends the pair (literal position in clause, path direction) to the auxiliary data. It returns the remaining path together with the updated \(\rho _0\), \(\sigma \), and the accumulated clause auxiliary data.

The Razborov encoding of a DNF \(f\) and a restriction \(\rho \) with parameters \(w, d\). It takes the first \(d\) steps of the deepest path of the canonical decision tree for \(f|_\rho \), then repeatedly selects the first clause of \(f\) not killed by the current restriction, processes all of that clause’s free literals against the path, and emits a termination marker \((w, \mathrm{false})\). The result is a pair \((\gamma , \mathrm{aux})\), where \(\gamma \) extends \(\rho \) by fixing \(d\) variables to their satisfying directions and \(\mathrm{aux}\) consists of per-clause blocks separated by the termination markers.

The inverse of the Razborov encoding: given the DNF \(f\), parameter \(w\), and a pair \((\gamma , \mathrm{aux})\) produced by the encoder, it recovers the original restriction \(\rho \). It repeatedly finds the first clause not killed by the current restriction, processes that clause’s auxiliary block (unfixing each recorded variable in \(\sigma \) and recording its path direction in \(\rho _0\) until a termination marker is reached), and returns the resulting restriction.