Apologies for the somewhat cryptic title.
For any first-order formula X, let ssm(X) be the size of the smallest finite model of X. By size I mean number of individuals. So, for example, ssm('Fa & ~Fb') = 2 because the smallest models of 'Fa & ~Fb' have two individuals. If X has no model, or only infinite models, f(X) is undefined.
Now, for any number n, let lssm(n) be the maximum of ssm(X) among all formulas X with length n. That is, lssm(n) is the largest size among the smallest finite models for formulas with length n. The specifics obviously depend on details of the relevant language: whether we have function symbols, identity, redundant Boolean operators, etc. So there are in fact several different functions here.
What is known about these functions? Are they computable? Can we say approximately what value they take for, say, n=30?
In general, because of Trakhtenbrot's theorem [0], these functions are not computable. Since with one binary relation symbol you can encode Turing machines with a logical sentence, your problem reduces to the busy beaver functions [1]. It is known that these functions grow ridiculously fast, and that they are not computable.
[0] https://en.wikipedia.org/wiki/Trakhtenbrot's_theorem
[1] https://en.wikipedia.org/wiki/Busy_beaver