$p-WD_φ ≤fpt p-WSat(d-CNF)$ for every $Π_1$-sentence $φ = ∀ xs ψ$ (Flum–Grohe, Lemma 6.37), with $d = 2 + (the total length of the clauses of a CNF of ψ)$. The formula has a variable for each $s$-tuple of the elements $U$ (the elements $0, …, L-1$, $L = min(|A|, |x| + s·k + r)$, and every element occurring in a relation), a clause per assignment of elements of $U$ to the variables and clause of the CNF (its $X$-literals, or $Y₀ ∨ ¬Y₀$ when a literal without $X$ holds), and the clauses $Y ∨ ¬Y$; $k$ stays $k$. Elements outside $U$ are isolated and interchangeable, so a witness exists iff one exists within $U$. The map is computed in fixed-parameter time by an IMP+ program.