No, not really. A SAT solver checks if there's a model in which a formula is true, while this program checks if the formula is true in every model. It's believed that there's no efficient reduction from one to the other, because otherwise NP=coNP.
So I guess you could say that a theorem prover for propositional logic, like Logic Theorist, is "half" of a modern solver like Z3, it can produce proofs but not counterexamples. :)
Then what is the model theoretic problem? Is it, if f(a,b)=((a and not b) or (b and not a)) is satisfied by e.g. (a=1,b=0), then we want to know all configs that satisfy it? The way I understand your post, you are saying we want to know if all combinations of a and b over {0, 1} satisfy the formula. I'm not sure that's not the same thing from a different perspective.
I started a course on abstract algebra once, but actually I am still limited to boolean logic. while they mentioned Galois Theory, functions as points in a metric space, graph coloring problems and many things that sound interesting but quickly have me getting lost in details. It's the same effect as with other machine learning ... coff coff.