<p>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.</p>

<p>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.</p>

<p>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 ?</p>

CC BY-SA 3.0
2013-08-09T12:08:31.357Z
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".
Shaull
CC BY-SA 3.0
2013-08-09T15:47:45.640Z
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').$.
Trylks
<cc.complexity-theory><lo.logic>
Satisfaction and synthesis of models in logics
Gzorg
# Satisfaction and synthesis of models in logics

(Asked by: username_0 on 2013-08-09)

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 ?

**Tags:** cc.complexity-theory, lo.logic
> **Comments:**
> **username_1**: 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".  
> **username_2**: 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').$.  

---

## 0 answers

