I know that there are implementations of first-order (finite) satisfiability checking that, given a finite set of axioms, searches for a finite model that satisfies them all.
I would like to ask whether there is a second-order logic (finite) satisfiability checker. Although, we can always write a (naive) algorithm that enumerates all possible finite interpretations and check whether they are a model or not, I would like to know if there is some implementation/research doing something more intelligent (instead of a blind search).