SAT in finite model theory without order
The standard method for showing inexpressibility results for FO(PFP) (and for FO(LFP), by the way) is by using the fact that FO(PFP) is embedded in the finite-variable infinitary logic $\mathrm{L}^\omega_{\infty\omega}$. Here $\mathrm{L}^\omega_{\infty\omega}$ is the finite-variable fragment of $\mathrm{L}_{\infty\omega}$, where the latter is the class of (infinitary) formulas build from the atoms by means of negations, finitary or infinitary disjunctions and conjunctions of the type $\bigvee_i \phi_i$ and $\bigwedge_i \phi_i$, and existential and universal quantification. The logic $\mathrm{L}^k_{\infty\omega}$ is the collection of all formulas in $\mathrm{L}_{\infty\omega}$ that involve at most $k$ variables (quantified or not), and $\mathrm{L}^\omega_{\infty\omega} = \bigcup_k \mathrm{L}^k_{\infty\omega}$.

It is known that FO(PFP) $\subseteq \mathrm{L}^\omega_{\infty\omega}$ (see Theorem 7.4.2 in Ebbinghaus and Flum book "Finite Model Theory"). Thus, if you prove that something is not expressible in $\mathrm{L}^k_{\infty\omega}$ for any $k$, then you also prove that it is not expressible in FO(PFP).

Now, how does one prove inexpressibility results for $\mathrm{L}^k_{\infty\omega}$? By playing the $k$-pebble games. These are Ehrenfeucht-Fraissé-type of games where the number of rounds is unbounded but each player has at most $k$ pebbles that he can re-use (see Ebbinghaus and Flum book again for details).

After all this background, now we can show that CNF-SAT is not expressible in $\mathrm{L}^k_{\infty\omega}$ for any $k$. For every fixed $k$, we need to find a satisfiable CNF formula $F_k$ and an unsatisfiable CNF formula $G_k$ such that $F_k \equiv^k_{\infty\omega} G_k$, where $A \equiv^k_{\infty\omega} B$ means that the Duplicator has a winning strategy for winning the $k$-pebble game on the structures $A$ and $B$ (here we need to fix some sensible way of encoding CNF formulas as finite structures: let's say we encode them as their bipartite incidence graph with elements representing clauses on one side, elements representing variables on the other, and 2 types of binary relations indicating which variables appear in which clauses and under what sign). I claim that an explicit choice of $F_k$ and $G_k$ is possible. But instead I will give you an indirect proof.

It is trivial to see that $K_k \equiv^k_{\infty\omega} K_{k+1}$, where $K_a$ denotes the clique-graph on $a$ vertices. In particular EVENNESS is not definable in $\mathrm{L}^\omega_{\infty\omega}$. It is also known that CNF-SAT is NP-complete under first-order reductions (see Theorem 7.16 in Immerman's "Descriptive Complexity" book). Since trivially EVENNESS is in NP, this means that there is a first-order reduction from EVENNESS to CNF-SAT. Since first-order reductions (in pure first-order logic, without built-in linear-order or anything as it is the case in Theorem 7.16 from Immerman's book) preserve expressibility in $\mathrm{L}^\omega_{\infty\omega}$ backwards, the result follows: if CNF-SAT were expressible, EVENNESS would also be; a contradiction.