Expressing associativity as a Boolean SAT problem

Question

Suppose we have a binary operation $B: S \times S \to S$ on a finite set $S$. We can encode $B$ as an array of $|S|^3$ Boolean values by setting $$ B_{ijk} \equiv \text{True} \quad \text{ iff } \quad B(i,j) = k $$ for all $i,j,k \in S$. Using this representation, how can we encode the proposition "$B$ is associative" as a Boolean satisfiability problem? One simple way is to require $$ \bigwedge_{i,j,k} \bigvee_{m,n,p} [B_{ijm} \wedge B_{mkp} \wedge B_{inp} \wedge B_{jkn}] $$ where all variables range over $S$. This effectively says "for each $i,j,k \in S$, set $m = B(i,j)$ and $n = B(j,k)$, and require the existence of $p \in S$ such that $B(m,k) = p = B(i,n)$." However, this is terribly inefficient, requiring $O(|S|^6)$ propositional statements, and I suspect that a simpler encoding should exist.