It is well known that for propositional logic, the problem of constructing a model of a given formula is equivalent to deciding whether the formula has a model. Satisfiability is NP-complete, and finding a model can be done by instanciating the variables one after another and checking each time whether the formula is still satisfiable, and this problem has the same complexity.
The satisfiability problem for LTL is PSPACE-complete, but he proof involves constructing an automaton that represents the set of all models, and from this, generating a model is easy, so synthesis in this case is also PSPACE-complete.
My question is: does this relation hold for any logic ? I.e. given some logic L, if the satisfiabiliy problem for L has complexity class C, is the problem of constructing a model always also in C ? Are there logics for which the model synthesis problem is significantly more difficult than satisfiability ?