The Complexity of Poor Man’s Logic

Edith Hemaspaandra

Abstract

Motivated by description logics, we investigate what happens to the complexity of modal satisfiability problems if we only allow formulas built from literals, ∧, ◇, and □. Previously, the only known result was that the complexity of the satisfiability problem for K dropped from PSPACE-complete to coNP-complete (Schmidt-Schauss and Smolka [5] and Donini et al. [2]). In this paper we show that not all logics behave like K. In particular, we show that the complexity of the satisfiability problem with respect to frames in which each world has at least one successor drops from PSPACEcomplete to P, but that in contrast the satisfiability problem with respect to the class of frames in which each world has at most two successors remains PSPACE-complete. As a corollary of the latter result, we also solve the one missing case from Donini et al.’s complexity classification of description logics [1].

Contents

1 Introduction 2

2 Poor Man’s Versions of NP-complete Satisfiability Problems 3

3 Poor Man’s Versions of PSPACE-complete Satisfiability Problems 4

4 ALEN Satisfiability is PSPACE-complete 9

1 Introduction

Since consistent normal modal logics contain propositional logic, the satisfiability problems for all these logics are automatically NP-hard. In fact, as shown by Ladner [4], many of them are even PSPACE-hard.

But we don’t always need all of propositional logic. For example, in some applications we may be able to bound the number of propositional variables. Propositional satisfiability thus restricted is in P, and, as shown by Halpern [3], the complexity of satisfiability problems for some modal logics restricted in the same way also decreases. For example, the complexity of S5 satisfiability drops from NP-complete to P. On the other hand, K satisfiability remains PSPACEcomplete.

Restricting the number of propositional variables is not the only propositional restriction on modal logics that occurs in the literature. For example, the description logic ALE can be viewed as multi-modal K where the only allowed propositional operators are ¬ on propositional variables and ∧. Both modal operators □ and ◇ are allowed.

As in the case of a fixed number of propositional variables, satisfiability for propositional logic with only ¬ on propositional variables and ∧ as operators is in P. After all, in that case every propositional formula is the conjunction of literals. Such a formula is satisfiable if and only if there is no propositional variable p such that both p and ¬p are conjuncts of the formula.

Satisfiability for modal logics whose operators are restricted in this way is not automatically NP-hard. Of course, it does not necessarily follow that the complexity of modal satisfiability problems will drop significantly. The only result that was previously known is that the complexity of K satisfiability drops from PSPACE-complete to coNP-complete. The upper bound was shown by Schmidt-Schauss and Smolka [5], and the lower bound by Donini et al. [2]. It should be noted that these results were shown in the context of description logics, so that the notation in these papers is quite different from ours.

In this paper we investigate if it is always the case that the complexity of the satisfiability problem decreases if we only look at formulas that are built from literals, ∧, ◇, and □, and if so, if there are upper or lower bounds on the amount that the complexity drops.

We will show that not all logics behave like K. Far from it, by looking at simple restrictions on the number of successors that are allowed for each world, we obtain many different behaviors. In particular, we will show that

1. The complexity of the satisfiability problem with respect to linear frames drops from NP-complete to P.

2. The complexity of the satisfiability problem with respect to [figure]remains NP-complete.

3. The complexity of the satisfiability problem with respect to frames in which every world has at least one successor drops from PSPACE-complete to P.

4. The complexity of the satisfiability problem with respect to frames in which every world has at most two successors remains PSPACE-complete.

As a corollary of the last result, we also solve the one missing case from Donini et al.’s complexity classification of description logics [1].

Definitions

Poor man’s formulas are built from literals (propositional variables and their negations), ∧, □, and ◇. We will view ∧ as a multi-arity operator, and we will assume that all conjunctions are “flattened,” that is, a conjunct will not be a conjunction. Thus, a formula ϕ in this language is of the following form: ϕ = □ψ_{1} ∧ ⋯ ∧ □ψ_{k} ∧ ◇ξ_{1} ∧ ⋯ ∧ ◇ξ_{m} ∧ ℓ_{1} ∧ ⋯ ∧ ℓ_{s}, where the ℓ_{i}s are literals.

As is usual, we will look at satisfiability with respect to classes of frames. In this paper, we are interested in simple restrictions on the number of successor worlds that are allowed. Let F_{≤1}, F_{≤2}, F_{≥1} be the classes of frames in which every world has at most one, at most two, and at least one successor, respectively.

2 Poor Man’s Versions of NP-complete Satisfiability Problems

We already know that the poor man’s version of an NP-complete modal satisfiability problem can be in P. Look for example at satisfiability with respect to the class of frames where no world has a successor. This is plain propositional logic in disguise, and it inherits the complexity behavior of propositional logic.

In this section, we will give an example of a non-trivial modal logic with the same behavior. We will show that the poor man’s version of satisfiability with respect to linear frames is in P. In contrast, we will also give a very simple example of a modal logic where the complexity of poor man’s satisfiability remains NP-complete.

Theorem 2.1 Satisfiability with respect to F_{≤1} is NP-complete and poor man’s satisfiability with respect to F_{≤1} is in P.

Proof. Clearly, F_{≤1} satisfiability is in NP (and thus NP-complete), since every satisfiable formula is satisfiable on a linear frame with ≤ md(ϕ) worlds, where md(ϕ) is the modal depth of ϕ. This immediately gives the following NP algorithm for F_{≤1} satisfiability: Guess a linear frame of size ≤ md(ϕ), and for every world in the frame, guess a valuation on the propositional variables that occur in ϕ. Accept if and only if the guessed model satisfies ϕ.

It is easy to prove that the following polynomial-time algorithm decides poor man’s satisfiability with respect to F_{≤1}. Let ϕ = □ψ_{1} ∧ ⋯ ∧ □ψ_{k} ∧ ◇ξ_{1} ∧ ⋯ ∧ ◇ξ_{m} ∧ ℓ_{1} ∧ ⋯ ∧ ℓ_{s}, where the ℓ_{i}s are literals. ϕ is F_{≤1} satisfiable if and only if

• ℓ_{1} ∧ ⋯ ∧ ℓ_{s} is satisfiable (that is, for all i and j, ℓ_{i} ≠ ¬ℓ_{j}), and

• – m = 0, (that is, ϕ does not contain conjuncts of the form ◇ξ, in which

case the formula is satisfied in a world with no successors), or

– ⋀_{i=1}^{k} ψ_{i} ∧ ⋀_{i=1}^{m} ξ_{i} is F_{≤1} satisfiable. □

From the previous example, you might think that the poor man’s versions of logics with the poly-size frame property are in P, or even that the poor man’s versions of all NP-complete satisfiability problems are in P. Not so. The following theorem gives a very simple counterexample.

Theorem 2.2 Satisfiability and poor man’s satisfiability with respect to the

frame [figure] are NP-complete.

Proof. Because the frame is finite, its satisfiability problem is NP-complete.

Thus it suffices to show that poor man’s satisfiability with respect to [figure] is NP-hard.

Since we are working with a fragment of propositional modal logic, it is extremely tempting to try to reduce from an NP-complete propositional satisfiability problem. However, because poor man’s logics contain only a fragment of propositional logic, these logics don’t behave like propositional logic at all. Because of this, propositional satisfiability problems are not the best choice of problems to reduce from. In fact, they are particularly confusing.

It turns out that it is much easier to reduce a partitioning problem to our poor man’s satisfiability problem. We will reduce from the following well-known NP-complete problem.

GRAPH 3-COLORABILITY: Given an undirected graph G, can you color every vertex of the graph using only three colors in such a way that vertices connected by an edge have different colors?

Suppose G = (V, E) where V = {1, 2, …, n}. We introduce a propositional

variable p_{e} for every edge e. The three leaves of [figure] will correspond to the three colors. To ensure that adjacent vertices in the graph end up in different leaves, we will make sure that the smaller endpoint of e satisfies p_{e} and that the larger endpoint of e satisfies ¬p_{e}.

The requirements for vertex i are given by the following formula:

ψ_{i} = ⋀{p_{e} | e = (i, j) and i < j} ∧ ⋀{¬p_{e} | e = (i, j) and i > j}.

Define f(G) = ⋀_{i=1}^{n} ◇ψ_{i}. It is not hard to prove that f is a reduction from

GRAPH 3-COLORABILITY to poor man’s satisfiability with respect to [figure]. □

3 Poor Man’s Versions of PSPACE-complete Satisfiability Problems

It is well-known that the satisfiability problems for many modal logics including K are PSPACE-complete [4]. We also know that poor man’s satisfiability for K is coNP-complete [5, 2]. That is, in that particular case the complexity of the satisfiability problem drops from PSPACE-complete to coNP-complete. Is this the general pattern? We will show that this is not the case. We will give an example of a logic where the complexity of the satisfiability problem drops from PSPACE-complete all the way down to P, and another example in which the complexity of both the satisfiability and the poor man’s satisfiability problems are PSPACE-complete. Both examples are really close to K; they are satisfiability with respect to F_{≥1} and F_{≤2}, respectively.

We will first consider F_{≥1}. This logic is very close to K and it should come as no surprise that the complexity of F_{≥1} satisfiability and K satisfiability are the same. It may come as a surprise to learn that poor man’s satisfiability with respect to F_{≥1} is in P. It is easy to show that poor man’s satisfiability with respect to F_{≥1} is in coNP, because the following function f reduces the poor man’s satisfiability problem with respect to F_{≥1} to the poor man’s satisfiability problem for K.

f(ϕ) = ϕ ∧ □^{≤md(ϕ)}◇q,

where q is a propositional variable not in ϕ. The formula ensures that every world in the relevant part of the K frame has at least one successor.

It is very surprising that poor man’s satisfiability with respect to F_{≥1} is in P, because the relevant part of the F_{≥1} frame may require an exponential number of worlds to satisfy a formula in poor man’s language.

For example, consider the following formula:

◇□□p_{1} ∧ ◇□□¬p_{1} ∧ □(◇□p_{2} ∧ ◇□¬p_{2}) ∧ □□(◇p_{3} ∧ ◇¬p_{3}).

If this formula is satisfiable in world w, then for every assignment to p_{1}, p_{2}, and p_{3}, there exists a world at distance 3 from w that satisfies that assignment. It is also clear that the formula is satisfiable on a frame if and only the frame contains a depth 3 binary tree as a subframe.

In its general version, the formula becomes

ϕtree = ⋀_{i=1}^{n} □^{i−1}(◇□^{n−i}p_{i} ∧ ◇□^{n−i}¬p_{i}).

This formula is satisfiable on a frame if and only if the frame contains a depth n binary tree as a subframe. The formula is of length polynomial in n and forces the relevant part of the model to be of exponential size.

Now that we have seen how surprising it is that poor man’s satisfiability with respect to F_{≥1} is in P, let’s prove it.

Theorem 3.1 Satisfiability with respect to F_{≥1} is PSPACE-complete and poor man’s satisfiability with respect to F_{≥1} is in P.

Proof. The proof that satisfiability with respect to F_{≥1} is PSPACE-complete is very close to the proof that K satisfiability is PSPACE-complete [4] and therefore omitted.

For the poor man’s satisfiability problem, note that a simplified version of Ladner’s PSPACE upper bound construction for K can be used to show the following.

Let ϕ = □ψ_{1} ∧ ⋯ ∧ □ψ_{k} ∧ ◇ξ_{1} ∧ ⋯ ∧ ◇ξ_{m} ∧ ℓ_{1} ∧ ⋯ ∧ ℓ_{s}, where the ℓ_{i}s are literals. ϕ is F_{≥1} satisfiable if and only if 1. ℓ_{1} ∧ ⋯ ∧ ℓ_{s} is satisfiable,

2. for all 1 ≤ j ≤ m, ψ_{1} ∧ ⋯ ∧ ψ_{k} ∧ ξ_{j} is F_{≥1} satisfiable, and

3. ψ_{1} ∧ ⋯ ∧ ψ_{k} is F_{≥1} satisfiable. (only relevant when m = 0.)

Note that this algorithm takes exponential time and polynomial space. Of course, we already know that poor man’s satisfiability with respect to F_{≥1} is in PSPACE, since satisfiability with respect to F_{≥1} is in PSPACE. How can this PSPACE algorithm help to prove that poor man’s satisfiability with respect to F_{≥1} is in P?

Something really surprising happens here. We will prove that for every poor man’s formula ϕ, ϕ is F_{≥1} satisfiable if and only if (the conjunction of) every pair of (not necessary different) conjuncts of ϕ is F_{≥1} satisfiable. Using dynamic programming, we can compute all pairs of subformulas of ϕ that are F_{≥1} satisfiable in polynomial-time. This proves the theorem. It remains to show that for every poor man’s formula ϕ, ϕ is F_{≥1} satisfiable if and only if every pair of conjuncts of ϕ is F_{≥1} satisfiable. We will prove this claim by induction on md(ϕ), the modal depth of ϕ.

If md(ϕ) = 0, ϕ is a conjunction of literals. In that case ϕ is not satisfiable if and only if there exist i and j such that ℓ_{i} = ¬ℓ_{j}. This immediately implies our claim.

For the induction step, suppose ϕ = □ψ_{1} ∧ ⋯ ∧ □ψ_{k} ∧ ◇ξ_{1} ∧ ⋯ ∧ ◇ξ_{m} ∧ ℓ_{1} ∧ ⋯∧ℓ_{s} (where the ℓ_{i}s are literals), md(ϕ) ≥ 1, and suppose that our claim holds for all formulas of modal depth < md(ϕ). Suppose for a contradiction that ϕ is not satisfiable, though every pair of conjuncts of ϕ is satisfiable. Then, by the Ladner-like construction given above, we are in one of the following three cases:

1. ℓ_{1} ∧ ⋯ ∧ ℓ_{s} is not satisfiable,

2. for some 1 ≤ j ≤ m, or ψ_{1} ∧ ⋯ ∧ ψ_{k} ∧ ξ_{j} is not satisfiable, or

3. ψ_{1} ∧ ⋯ ∧ ψ_{k} is not satisfiable.

By induction, it follows immediately that we are in one of the following four cases:

1. There exist i, i′ such that ℓ_{i} ∧ ℓ_{i′} is not satisfiable,

2. there exist i, i′ such that ψ_{i} ∧ ψ_{i′} is not satisfiable,

3. there exists an i such that ψ_{i} ∧ ξ_{j} is not satisfiable, or

4. ξ_{j} ∧ ξ_{j} is not satisfiable.

If we are in case 2, □ψ_{i} ∧ □ψ_{i′} is not satisfiable. In case 3, □ψ_{i} ∧ ◇ξ_{j} is not satisfiable. In case 4, ◇ξ_{j} ∧◇ξ_{j} is not satisfiable. So in each case we have found a pair of conjuncts of ϕ that is not satisfiable, which contradicts the assumption. □

Why doesn’t the same construction work for K? It is easy enough to come up with a counterexample. For example, {□p, □¬p, ◇q} is not satisfiable, even though every pair is satisfiable. The deeper reason is that you have some choice in K that you don’t have in F_{≥1}. Namely, on a K frame a world can have successors, or no successors. This little bit of extra choice is enough to encode coNP in poor man’s language.

Theorem 2.2 showed that the poor man’s version can be as difficult as general satisfiability for NP-complete logics. In light of the fact that poor man’s satisfiability for K is coNP-complete and poor man’s satisfiability with respect to F_{≥1} is even in P, you might wonder if the complexity of PSPACE-complete logics always decreases.

To try to keep the complexity as high as possible, it makes sense to look at frames in which each world has a restricted number of successors, as in the construction of Theorem 2.2. Because we want the logic to be PSPACEcomplete, we also need to make sure that the frames can simulate binary trees. The obvious class of frames to look at is F_{≤2} – the class of frames in which each world has at most two successors. This gives us the desired example.

Theorem 3.2 Satisfiability and poor man’s satisfiability with respect to F_{≤2} are PSPACE-complete.

Proof. Satisfiability with respect to F_{≤2} is PSPACE-complete by pretty much the same proof as the PSPACE-completeness proof for K [4]. To show that the poor man’s version remains PSPACE-complete, we will reduce the following well-known PSPACE-complete problem to poor man’s satisfiability with respect to F_{≤2}.

QUANTIFIED 3SAT: Given a Quantified Boolean formula ∃p_{1}∀p_{2}∃p_{3} ⋯ ∃p_{n−1}∀p_{n}ϕ, where ϕ is a propositional formula over p_{1}, …, p_{n} in 3CNF (that is, a formula in conjunctive normal form with exactly 3 literals per clause), is the formula true?

To simulate the quantifiers, we need to go back to the formula that forces models to simulate binary trees.

ϕtree = ⋀_{i=1}^{n} □^{i−1}(◇□^{n−i}p_{i} ∧ ◇□^{n−i}¬p_{i}).

This formula forces every assignment to p_{1}, …, p_{n} to be true in a world at distance n. We will call the worlds at distance n from the root the assignmentworlds. If ϕtree is satisfied on a F_{≤2} frame, the worlds of depth ≤ n form a complete binary tree of depth n and every assignment to p_{1}, … p_{n} occurs exactly once in an assignment-world. Also, the assignment-worlds in a subtree rooted at a world at distance i ≤ n from the root are constant with respect to the value of p_{i}.

It is easy to see that ∃p_{1}∀p_{2}∃p_{3} ⋯ ∃p_{n−1}∀p_{n}ϕ ∈ QUANTIFIED 3SAT if and only if ϕtree ∧ (◇□)^{n/2}ϕ is F_{≤2} satisfiable.

This proves that satisfiability for F_{≤2} is PSPACE-hard, but it does not prove that the poor man’s version is PSPACE-hard. Remember that ϕ is in 3CNF and thus not in the poor man’s language.

Below, we will show how to label all assignment-worlds where ϕ does not hold by f (for false). It then suffices to add the conjunct (◇□)^{n/2}¬f to obtain a reduction.

How can we label all assignment-worlds where ϕ does not hold by f? Let k be such that ϕ = ψ_{1} ∧ ψ_{2} ∧ ⋯ ∧ ψ_{k}, where each ψ_{i} is the disjunction of exactly 3 literals, ψ_{i} = ℓ_{i1} ∨ ℓ_{i2} ∨ ℓ_{i3}.

For every i, we will label all assignment-worlds where ψ_{i} does not hold by f. Since ψ_{i} = ℓ_{i1} ∨ℓ_{i2} ∨ℓ_{i3}, this implies that we have to label all assignment-worlds where ¬ℓ_{i1} ∧ ¬ℓ_{i2} ∧ ¬ℓ_{i3} holds by f. In general, this cannot be done in poor man’s logic, but in this special case we are able to do it, because the relevant part of the model is completely fixed by ϕtree.

As a warm-up, first consider how you would label all assignment-worlds where ¬p_{3} holds by f. This is easy; add the conjunct

□□◇□^{n−3}(¬p_{3} ∧ f).

You can label all assignment-worlds where ¬p_{3} ∧ p_{5} holds as follows:

□□◇□◇□^{n−5}(¬p_{3} ∧ p_{5} ∧ f).

This can easily be generalized to a labeling for ¬p_{3} ∧ p_{5} ∧ ¬p_{8}:

□□◇□◇□□◇□^{n−8}(¬p_{3} ∧ p_{5} ∧ ¬p_{8} ∧ f).

Note that we can write the previous formula in the following suggestive way:

□^{3−1}◇□^{5−3−1}◇□^{8−5−1}◇□^{n−8}(¬p_{3} ∧ p_{5} ∧ ¬p_{8} ∧ f).

In general, suppose your want to label all assignment-worlds where ℓ_{1}∧ℓ_{2}∧ℓ_{3} hold by f, where ℓ_{1}, ℓ_{2}, and ℓ_{3} are literals. Suppose that ℓ_{1}, ℓ_{2}, and ℓ_{3}’s propositional variables are p_{a}, p_{b}, and p_{c}, respectively. Also suppose that a < b < c. The forcing formula label false(ℓ_{1} ∧ ℓ_{2} ∧ ℓ_{3}) is then

□^{a−1}◇□^{b−a−1}◇□^{c−b−1}◇□^{n−c}(ℓ_{a} ∧ ℓ_{b} ∧ ℓ_{c} ∧ f).

The reduction from QUANTIFIED 3SAT to poor man’s satisfiability with respect to F_{≤2} is given by

g(∃p_{1}∀p_{2}∃p_{3} ⋯ ∃p_{n−1}∀p_{n}ϕ) = ϕtree∧ ⋀_{i=1}^{k} label false(¬ℓ_{i1}∧¬ℓ_{i2}∧¬ℓ_{i3})∧(◇□)^{n/2}¬f.

□

Why doesn’t the construction of Theorem 3.2 work for K? Look at ϕtree. If ϕtree is satisfied on a K frame, this frame must contain a subframe that forms a complete binary tree of depth n such that every assignment occurs exactly once on a leaf of the submodel based on this subframe. However, there is no formula that is satisfiable in a world with exactly two successors that isn’t also satisfiable in a world with more than two successors. Because of this, the label false formula will not necessarily label all assignment-worlds where ϕ does not hold by f. For a very simple example, consider the formula

◇p ∧ ◇¬p ∧ ◇(p ∧ f) ∧ ◇(¬p ∧ f) ∧ ◇¬f.

This formula is not F_{≤2} satisfiable, since both the p successor and the ¬p successor are labeled f. However, this formula is satisfiable in a world with three successors, satisfying p ∧ f, ¬p ∧ f, and ¬f, respectively.

4 ALEN Satisfiability is PSPACE-complete

In the introduction, we mentioned that poor man’s logic is closely related to certain description logics. Donini et al. [1] almost completely characterize the complexity of the most common description logics. The only language they couldn’t completely characterize is ALEN. ALEN is ALE (the poor man’s version of multi-modal K) with number restrictions. Number restrictions are of the form (≤n) and (≥n). (≤n) is true if and only if a world has ≤ n successors and (≥n) is true if and only if a world has ≥ n successors.

In [1], it was shown that ALEN satisfiability is in PSPACE, assuming that the number restrictions are given in unary. The best lower bound for satisfiability was the coNP lower bound that is immediate from the fact that this is an extension of ALE.

We will use Theorem 3.2 to prove a PSPACE lower bound for a very restricted version of ALEN.

Theorem 4.1 Satisfiability for the poor man’s version of K extended with the number restriction (≤2) is PSPACE-hard.

Proof. The reduction from poor man’s satisfiability with respect to F_{≤2} is obvious. It suffices to use the number restriction (≤2) to make sure that every world in the relevant part of the model has at most two successors. Let md(ϕ) be the modal depth of ϕ. All worlds that are of importance to the satisfiability of ϕ are at most md(ϕ) steps away from the root. The reduction is as follows:

f(ϕ) = ϕ ∧ □^{≤md(ϕ)}(≤2)

□

Combining this with the PSPACE upper bound from [1] completely characterizes the complexity of ALEN satisfiability.

Corollary 4.2 ALEN satisfiability is PSPACE-complete.

Acknowledgments

I would like to thank Johan van Benthem for suggesting this topic, and Johan van Benthem, Hans de Nivelle, and Maarten de Rijke for helpful conversations and suggestions.

References

[1] F. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages. Information and Computation, 134, pp. 1-58, 1997.

[2] F. Donini, B. Hollunder, M. Lenzerini, D. Nardi, W. Nutt, and A. Spaccamela. The complexity of existential quantification in concept languages. Artificial Intelligence, 53, pp. 309–327, 1992.

[3] J. Y. Halpern. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence, 75(2), pp. 361-372, 1995.

[4] R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3), pp. 467– 480.

[5] M. Schmidt-Schauss and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48, pp. 1–26, 1991.