A Krom clause over a vocabulary $L$, a block of second-order relation variables and $k$ first-order variables $\bar x$ is an implication $\gamma(\bar x) \to \ell_1 \vee \ell_2$, where the guard $\gamma$ is an arbitrary first-order formula over $L$ and each $\ell_i$ is an atom in the relation variables or the negation of one; either literal may be absent, so a clause may be a unit clause or the goal clause $\gamma(\bar x) \to \bot$. A Krom program is a finite list of such clauses, and an assignment of relations to the block satisfies it on a structure when every clause holds at every valuation of $\bar x$.

A decision problem $P$ over $L$ is SO-Krom definable when there are a block, a number $k$ and a Krom program over $L \cup \{\le\}$ such that, for every nonempty finite $L$-structure $A$ and every linear order on $A$, $A$ is a yes-instance of $P$ if and only if some assignment satisfies the program on $A$ with that order. The guards may thus use the order, while the problem does not depend on it. This is the fragment SO-Krom of Grädel, existential second-order logic whose first-order kernel is universal with at most two second-order literals per clause.