Complexity of SAT in First-order logic

[complexity9]

I have been thinking about this question for weeks and can't figure it out! I reckon it's decidable and in EXPTIME, but not sure how to prove this! Any help would be reallllly appreciated!

(Note: the question is in the attachment)

-Peter

 

[Citan Uzuki]

Yes, it is possible to decide whether such a formula is satisfiable in EXPTIME, and in fact this problem admits an easy reduction to SAT. We can proceed as follows -- first begin by Skolemizing the formula. Since the formula is existentially bounded, the prenex normal form will contain only existential quantifiers, so the Skolem normal form will be quantifier-free and contain no function symbols. Hence it suffices to show that deciding whether a quantifier-free sentence with no function symbols is satisfiable is reducible to SAT. But this is now easy -- we being by defining two atomic predicates to be equal if they consist of the same predicate symbol applied to the same constants in the same order. Then we replace the atomic predicates with propositional variables in such a way that two atomic predicates are replaced with the same propositional variable if and only if they are equal. The resulting propositional formula is satisfiable iff the original quantifier-free sentence is.

 

[complexity9]

defining two atomic predicates to be equal if they consist of the same predicate symbol applied to the same constants in the same order.

Can you elaborate on this? What if we have P(x,y) and P(y,z) and Q(x,y) and Q(z,x,y). What do you say about their equality? Do you just assign different predicate variables to each of them? But are they not "related" somewhat to one another (since they share x,y or z)?

What is Q is defined to be \not P. Then if you assign different predicate variables to them they can both be true at the same time (but we don't want this!)

 

[complexity9]

Okay ignore the above. I had misunderstood of the problem to begin with, but I now understand. The "satisfiability" problem asks if there is a model that satisfies our existentially bounded sentence; if we have for example P(x,y) and P(y,z), we just simply define them to be different in our model, to get satisfiability.

Now please consider an extension of this problem, described in the picture below. This problem can't be reduced to SAT (as far as I know). But my intuition still tells me that its still decidable (and also in EXPTIME), but don't know how to show this. Please help!

 

[Citan Uzuki]

Hmm... not sure about this one. Sorry. Hopefully one of the other posters will have some insight.

 

[complexity9]

By the way, can equality be written from function variables and predicate variables? For example, if you have a FO logic vocabulary with everything but equality, is this equavalent to the normal FO logic vocabulary?

 

[complexity9]

Citan Uzuki,

Do you mind helping me with another question. It is based on an extension of the first question in this thread. Basically, what happens when you take a boolean combination of the existentially-bounded sentence (without equality or function symbols)?

Please see the image for the full description, if needed.

Thanks! Please help!

 

[Citan Uzuki]

Sorry for the delayed reply, I have been very busy with finals. If we take a boolean combination of existentially bounded sentences with no function symbols, then the skolem normal form of that sentence can be written with no function symbols. So it suffices to show we can decide the satisfiablity of a sentence in skolem normal form that has no function symbols. Now, if there is a model of such a sentence, then there is a finite model, and in fact one with at most as many elements as there are constant symbols appearing in the sentence (specifically, if some model satisfies a universally quantified sentence with no function symbols, then the submodel consisting of all the elements assigned to a constant symbol will also satisfy the same sentence). Since we can enumerate every possible structure with up to as many elements as there are constants appearing in the sentence, the truth of such sentences is decidable. Moreover, if the arity of the predicates is bounded (say, you're considering only sentences from a language fixed in advance), this naive algorithm runs in EXPTIME. For a model of size n, there are 2^(n^k) possible values for a predicate of arity k, and if there are m such predicates, this means you ultimately have to test only 2^(mn^k) models. Impractical, but still EXPTIME if k is fixed.

The same trick of bounding the size of a possible model works with second-order sentences as well, only in this case the decision algorithm of enumerating all possible models will not run in EXPTIME, and I suspect the problem is outside that complexity class.

 

[complexity9]

Thank you for that! Your argument is very nice and simple (compared to the one I came up with earlier, which proved that it is PSPACE, but took two pages in latex). Anyway, it seems like this idea can be applied to the boolean combination of existentially-bounded L^P sentences as welll; since we can just "enumerate" all possible predicate variables as well and this will be in EXPTIME. Can you confirm that this is correct as well?

Also, what do you mean about Second-order logic; all of the logic I posted above are subclasses of First-order logic, aren't they? Or does first-order logic not consist of predicate/function variables?

And what is "constants". Should you not use "variable" instead?

 

[Citan Uzuki]

Thank you for that! Your argument is very nice and simple (compared to the one I came up with earlier, which proved that it is PSPACE, but took two pages in latex). Anyway, it seems like this idea can be applied to the boolean combination of existentially-bounded L^P sentences as welll; since we can just "enumerate" all possible predicate variables as well and this will be in EXPTIME. Can you confirm that this is correct as well?

You can enumerate all the possible predicate values as well, but it won't happen in EXPTIME. Remember that the number of possible assignments for each predicate is 2^(n^k), where k is the arity of the predicate, and you need to bound k to get it in EXPTIME. But with L^p sentences, k is unbounded.

Also, what do you mean about Second-order logic; all of the logic I posted above are subclasses of First-order logic, aren't they? Or does first-order logic not consist of predicate/function variables?

First order logic consists of quantifying over object variables only. Quantifying over predicate and/or function variables is second-order logic.

And what is "constants". Should you not use "variable" instead?

When converting a sentence to Skolem normal form, each existentially quantified variable is replaced with a function of all the other variables on which it depends. If there are no variables on which it depends, it is replaced with a function of zero variables, which is a constant.

 

[complexity9]

You can enumerate all the possible predicate values as well, but it won't happen in EXPTIME. Remember that the number of possible assignments for each predicate is 2^(n^k), where k is the arity of the predicate, and you need to bound k to get it in EXPTIME. But with L^p sentences, k is unbounded.

But you only need to consider those predicate variables that are "written down" in the sentence. In order for it to be written down, it must have some finite arity. What I'm saying is, if a predicate variable P is written down such as P(x,y,z,z,x,w) or however many arity you want (as long as its finite), then would its arity not have to be bounded, in order to be "written down" in the sentence? And whenever you have something like (there exists) S, but S is actually not used anywhere in the sentence, then you don't have to enumerate a model for S because you know that there exists an infinite number of different predicate variables of each arity. Furthermore, I'm not sure which parameter we could use to show its complexity (you used n,m,k, etc.). Perhaps if we use the parameter that is the "length" of the sentence (i.e. the amount of characters used to write the sentence), then surely its arity has to be bounded right?

Even in the example in the attachment, S has arity 2. Can you think of an example where the arity of a predicate variable is not bounded, and yet we still need to enumerate a model for it?

Anyway, what happens if we extend it further to get L^P,F where this logic has function variables? Obviously this is not in EXPTIME if the previous one (L^P) is not in EXPTIME. But I assume that it is still decidable, since we can enumerate through all the possible function variables as well. Is this correct? Is the arity of the function variables bounded as well? For more detail please see the attached picture. Again, thanks so much for helping, you have clarified a lot of stuff that I misunderstood already. Thanks!

 

[Citan Uzuki]

You are correct, k is bounded by the length of the input. What I mean is, k is not bounded by a constant, so if you permit very long predicates, you could have growth as fast as 2^(n^n), where n is the length of the input.

Anyway, what happens if we extend it further to get L^P,F where this logic has function variables? Obviously this is not in EXPTIME if the previous one (L^P) is not in EXPTIME. But I assume that it is still decidable, since we can enumerate through all the possible function variables as well. Is this correct? Is the arity of the function variables bounded as well? For more detail please see the attached picture. Again, thanks so much for helping, you have clarified a lot of stuff that I misunderstood already. Thanks!

Yes, it is still decidable. The central intuition is still that if there is a model, then there is a finite model. Basically this is because in the prenex normal form of the sentence, if a function variable is existentially quantified, then all the terms it applies to are also existentially quantified (since they come from the same existentially bounded sentence, and the quantifiers from that sentence were not negated when you pulled them out in front). So if the Skolem normal form of the sentence can be satisfied in some model, you can change the values of any function in the satisfying assignment on any element not corresponding to a term in the sentence to any other value and still have a satisfying assignment. Hence there is a satisfying assignment where all the function predicates are assigned to functions with a finite range, and then passing to the Skolem hull yields a finite model.

 

[complexity9]

You are correct, k is bounded by the length of the input. What I mean is, k is not bounded by a constant, so if you permit very long predicates, you could have growth as fast as 2^(n^n), where n is the length of the input.

But how come k is bounded by a constant in the first two cases (with no predicate/function variables), then when you allow for predicate/function variables, k suddenly becomes unbounded (by a constant). What I mean is, why can't predicate symbols have growth as fast as 2^(n^n), if it has arity n? Why does this only happen to predicate variable but not predicate symbol?

It seems likely that L^P and L^P,F are not in EXPTIME, but how would one prove this? I suppose we would have to give a reduction from a non-EXPTIME problem to those two. Any ideas?

Thanks again! =)

 

[Citan Uzuki]

What I mean is, why can't predicate symbols have growth as fast as 2^(n^n), if it has arity n? Why does this only happen to predicate variable but not predicate symbol?

In my original post, I said the following:

Moreover, if the arity of the predicates is bounded (say, you're considering only sentences from a language fixed in advance), this naive algorithm runs in EXPTIME. For a model of size n, there are 2^(n^k) possible values for a predicate of arity k, and if there are m such predicates, this means you ultimately have to test only 2^(mn^k) models. Impractical, but still EXPTIME if k is fixed.

If the arity of the predicates is not bounded, then you do in fact run into the same problem. Which doesn't mean the problem isn't EXPTIME, just that the algorithm based on enumerating every possible model won't run that fast.

 

[complexity9]

Okay let me summarize what I think you have said, just to make sure we are on the same page (I am a bit confused at this point, lol):

So the first problem was reducible to SAT, that's fine. The problems 2-4 are all decidable. The 2nd problem (boolean combination of existentially-bounded sentences, with no predicate/function symbols) will definitely be in EXPTIME if k is bounded, but even if k is unbounded, it may still be in EXPTIME (just that our naiive algorithm may not run in exponential time). How do I show that it is in EXPTIME then if k is unbounded?

As for problems 3 and 4, the naiive algorithm does not run in EXPTIME since k cannot be bounded (but somehow k can be bounded in the case of problem 2?). We do not know if they are in EXPTIME at all, but how do I show whether they are NOT in EXPTIME?

 

[Citan Uzuki]

So the first problem was reducible to SAT, that's fine. The problems 2-4 are all decidable. The 2nd problem (boolean combination of existentially-bounded sentences, with no predicate/function symbols) will definitely be in EXPTIME if k is bounded, but even if k is unbounded, it may still be in EXPTIME (just that our naiive algorithm may not run in exponential time).

Yep, you got it. Just to answer the question in your next paragraph, the reason we might be able to bound k is that we might be talking about deciding the truth of existentially bounded sentences from some specific language with no function symbols, and if that specific language has only finitely many predicates, then k is bounded by the arity of the largest predicate. If we want the algorithm to run on any language, then we are in the same situation as we are on the third and fourth problems.

How do I show that it is in EXPTIME then if k is unbounded?

As for problems 3 and 4, the naiive algorithm does not run in EXPTIME since k cannot be bounded (but somehow k can be bounded in the case of problem 2?). We do not know if they are in EXPTIME at all, but how do I show whether they are NOT in EXPTIME?

Not sure on any of these. I'd have to think about it some more, and I'll be busy this weekend, so I might not be able to give you much more help. But if I do come up with something, I'll let you know.

 

[complexity9]

Please do think about it and let me know! This question is so hard, took me so long just to get anywhere.

EDIT: I think I may have found an algorithm for satisfiability for ALL of them in PSPACE. Let me describe it and see what you think. The algorithm go as follows:

Since we have a boolean combination of existentially quantified sentences (in all cases), we think of each sentence in the boolean combination as a propositional variable and enumerate through the {0,1} assignments of those propositional variables. This can be done in PSPACE.

For each (enumerate through all of them) propositional variable assigned to 1, we use the same technique we did for the first question and reduce the existentially-quantified sentence to SAT. This can also be done in PSPACE.

For each satisfying assignment of that EB sentence when reduced to SAT as above, we "construct" our model so that the EB sentence is satisfied. This takes linear time, and hence also PSPACE.

After we are done with the propositional variables assigned to 1, we look at those EB sentences assigned to 0 and make sure that our "constructed" model does not satisfy any of those EB sentences. If all that EB sentences assigned to 0 does not satisfy our model, then we are done (and return accept). If not, backtrack and go to next enumeration.

If after all the enumerations and we have not yet accepted, then reject.

END.

So... the above looks like its PSPACE, but I may not have explained it well enough. Please let me know if you understand it, and what you think... I may just be completely confused and the above might make no sense =P