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 ?

  • 1
    $\begingroup$ Your comment on LTL synthesis is misleading: Synthesis of LTL formulas usually refers to reactive systems, in which case you synthesize a transducer that, when composed with any environment, satisfies the formula. This problem is 2-EXPTIME-complete. I would call the problem you suggest "satisfiability witness". $\endgroup$ – Shaull Aug 9 '13 at 12:08
  • 2
    $\begingroup$ Any logic with the existential quantifier (or functions, or the universal quantifier and negation) can have models that are infinite. Actually, e.g. $\forall x. person(x) \rightarrow parent(x,y), person(y). \\ person('Adam').$. $\endgroup$ – Trylks Aug 9 '13 at 15:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.