GEORGIAN MATHEMATICAL JOURNAL: Vol. 3, No. 1, 1996, 97-100

COMPLEXITY OF THE DECIDABILITY OF ONE CLASS OF FORMULAS IN QUANTIFIER-FREE SET THEORY

WITH A SET-UNION OPERATOR

M. TETRUASHVILI

Abstract. We consider the quantifier-free set theory MLSUn containing the symbols U, \, =, ∈, Un. Un(p) is interpreted as the union of all members of the set p. It is proved that there exists an algorithm which for any formula Q of the MLSUn theory containing at most one occurrence of the symbol Un decides whether Q is true or not using the space cn^{3} log_{2} n (n is the length of Q).

Let MLSUn (MLS) be a quantifier-free set theory whose language contains the symbols U, \, =, ∈, Un (U, \, =, ∈), where Un is a unary functional symbol (Un(p) is understood as a union of all members of the set p). Let MLSUn^{(1)} be the class of formulas of the language MLSUn containing at most one occurrence of the symbol Un. The decidability problem for a class of formulas consists in finding an algorithm which decides whether an arbitrary formula of this class is true or not. For the class MLSUn^{(1)} the problem of decidability can be easily reduced to testing the satisfiability of conjunctions of literals of the following types:

(=) x = y ∪ z, x = y \ z, (∈) x ∈ y, (Un) u = Un(p),

where the conjunctions contain the (Un)-type literal not more than once.

Let Q be the formula of the MLSUn^{(1)}. If Q contains literals u = Un(p) and u = ∅, then Q has a model if and only if Q_{0} has a model, where Q_{0} denotes the result of removing the clause u = Un(p) from Q and adding either the literal p = ∅ or the clauses ∅ ∈ p, ∅ = x∩p∨∅ = x∩p∨∅ = p\x for every variable x of Q. The obtained Q_{0} is a formula of the decidable theory MLS [1]. Therefore we can assume Q to contain the literal u ≠ ∅.

Let x, z_{1}, …, z_{m}, y be variables. By P^{+}(x, z_{1}, …, z_{m}, y) we denote the

disjunction ∨_{⟨,i_{1},...,i_{k}⟩∈I_{m}^{+}}(x ∈ z_{i_{1}}&z_{i_{1}} ∈ z_{i_{2}}& ⋯ &z_{i_{k−1}} ∈ z_{i_{k}}&z_{i_{k}} ∈ y) where

I_{m}^{+} is the set of all non-empty ordered subsets of the set {1, …, m}. 97

1991 Mathematics Subject Classification. 03D15.

Key words and phrases. Complexity of decidability, set theory, set-union operator.

1072-947X/96/0100-0097$09.50/0 \begin{matrix}c \\ ◯ \end{matrix} 1996 Plenum Publishing Corporation

Let x_{1}, …, x_{m} be all variables occurring in Q. It is proved in [2] that given a finite family z_{1}, …, z_{m} of sets and the set p such that Un(p) ≠ ∅, there exists a non-empty set t ∈ p such that P^{+}(t, z_{1}, …, z_{m}, Un(p)) is false. Therefore we can add the statements t ∈ p, t ≠ ∅ and ¬P^{+}(t, x_{1}, …, x_{m}, u) to the formula Q not modifying its satisfiability (t is a new variable).

Finally, Q can be assumed to contain one full conjunct C of the disjunc-

tive normal form (d.n.f.) of the statement &^{m}_{i=1}(x_{i} ∉ p ∨ x_{i} \ u = ∅) which is true in any model of Q.

Let Q_{−} denote the result of removing the literal u = Un(p) from Q. The obtained Q_{−} is a formula of MLS. It has been proved in [2] that Q has a model if and only if Q_{−} has a model. Therefore this theorem solves the problem of decidability for the class MLSUn^{(1)}. However, the formula P^{+}(x, z_{1}, …, z_{m}, y) playing an important part in the investigation of satisfiability of Q is awkward: 2^{m} ≤ Card(I_{m}^{+}) ≤ m^{m}, and the d.n.f. of this formula contains a large number of summands (exponential with respect to m).

Therefore the corresponding decidability procedure has an exponential computational complexity (by space).

Below we shall find an algorithm which solves the decidability problem for the class MLSUn^{(1)} with a polynomial computational complexity (by space).

The formula ¬P^{+}(x, z_{1}, …, z_{m}, y) is equivalent to the formula

&_{⟨,i_{1},...,i_{k}⟩∈I_{m}^{+}}(x ∉ z_{i_{1}} ∨ z_{i_{1}} ∉ z_{i_{2}} ∨ ⋯ ∨ z_{i_{k−1}} ∉ z_{i_{k}} ∨ z_{i_{k}} ∉ y).

Its d.n.f. Δ^{+}(x, z_{1}, …, z_{m}, y) ≡ Δ^{+} contains at most m^{m^{2}} summands.

Let K be an arbitrary summand of the above d.n.f. Δ^{+}. This K is a conjunction of literals of the following forms: x ∉ z_{i}, z_{i} ∉ z_{j}, z_{j} ∉ y. The number of various ordered pairs composed of all variables of the formula Δ^{+} is less than (m + 2)^{2}. Therefore, although the number of factors in K is greater than 2^{m}, the number of different factors in it is less than (m + 2)^{2}. Consequently, K contains the majority of recurring factors.

In the sequel, the disjunction will be assumed to be a well-ordered set of its summands. The set I_{m}^{+} is naturally well ordered with respect to the number k of elements in the system ⟨i_{k}, …, i_{k}⟩ and lexicographically for a given number k of elements in the system. Let M_{ν} denote the disjunction x ∉ z_{1} ∨ ⋯ ∨ z_{i_{k}} ∉ y, where ν is a number of the system ⟨i_{1}, …, i_{k}⟩ in the set I_{m}^{+} and let m_{ν} be the last element of the set M_{ν}. The conjunction K is composed as follows: the number of all factors is equal to Card(I_{m}^{+}) and the νth member of the conjunction is an element of the set M_{ν}.

It can be easily seen that the formula Q_{−} is equivalent to the disjunction

QUANTIFIER-FREE SET THEORY WITH A SET-UNION OPERATOR 99

D of the formulas of the form

H&Δ^{+}(x, z_{1}, …, z_{m}, y),  (1)

where H is Q_{0}&(t ∈ p)&(t ≠ ∅)&C, and Q_{0} denotes the result of removing the literal u = Un(p) from Q, length(H) ≤ c_{0} · length(Q) with a constant c_{0} and the number of summands in the disjunction is equal to 2^{m}. The formula Q is satisfiable if and only if one of the summands of D is satisfiable. In this case the passage from one summand to the next one is realized easily and mechanically. Therefore, having investigated one summand for satisfiability we can write out the next one H′ and cancel the previous H.

The satisfiability test for the given summand of D of the type (1) requires that for all summands of the d.n.f. of the formula (1). We test the satisfiability of each such conjunction with the linear space [3].

Obviously, an arbitrary summand of the d.n.f. of the formula of the type (1) has the form H&K, where K is a conjunction of literals. Hence, to construct an algorithm testing the satisfiability of the formula Q_{−}, it suffices to construct an algorithm 𝔄 which for an arbitrary conjunction K′ of the d.n.f. Δ^{+} gives immediately the next conjunction K. The formula Δ^{+} can be regarded as a direct product of the well-known number of well-ordered finite sets M_{ν} and hence as a well-ordered set of conjunctions. Therefore, writing down the given conjunction K of the d.n.f. Δ^{+} along with all its recurring factors (their number is greater than 2^{m}), we can easily write out the next conjunction immediately following it.

When constructing an algorithm 𝔄 it is natural to operate with reduced conjunctions K of the d.n.f. Δ^{+}. However, in order to reset all conjunctions of the d.n.f. Δ^{+}, it is necessary to keep some information about implicit recurring factors of the reduced conjunctions in the case where the conjunction K is reduced.

Let us remove from the conjunction K the recurring literals from the left to the right and keep the number of the removed literals. The obtained conjunction λ_{1}& ⋯ &λ_{k} of literals we write as follows:

λ_{1}𝔟_{1}λ_{2}𝔟_{2} ⋯ λ_{k}𝔟_{k},  (2)

where 𝔟_{i} is a binary notation of the number of those literals of K which iterate the literals λ_{1}, …, λ_{i}. Since k ≤ 2m^{2} and Card(I_{m}^{+}) ≤ m^{m}, the length of the whole writing (2) does not exceed 2m^{3} log_{2} m. Our aim can be achieved by proving the following

Lemma. There exists an algorithm 𝔄 which for the variables x, z_{1}, …, z_{m}, y and an arbitrary number μ (in binary notation) of the conjunction of the d.n.f. Δ^{+} with the space cm^{3} log_{2} m gives this conjunction K_{μ} in the form (2) and also determines in a non-last conjunction K_{μ} the first from the right number ν_{0} (in binary notation) of its literal which is different from m_{ν_{0}}.

Proof. The binary notation length of the number μ of the conjunction of Δ^{+} does not exceed m^{2} log_{2} m. For μ = 1 the validity of assertions of the lemma is obvious. Let for μ the conjunction K_{μ} be already written out in the form (2) and let the first from the right number ν_{0} of the literal λ from K_{μ}, which is different from m_{ν_{0}}, be also determined. We replace in K_{μ} the literal λ with the number ν_{0} by the next literal λ′ of M_{ν_{0}}. Furthermore we replace all literals of K_{μ} with the numbers ν > ν_{0} by the first elements of M_{ν} and leave unchanged all literals with the numbers ν < ν_{0}. If λ′ ≠ m_{ν_{0}}, then the required conjunction K_{μ+1} and the number ν_{0} are found for μ + 1. Let λ′ = m_{ν_{0}}. Then we can determine the first, to the left of ν_{0}, number ν_{1} of the literal of the complete conjunction K_{μ+1} which is different from m_{ν_{1}}. To this end, starting with μ = 1 we successively write out the conjunctions K_{1}, …, K_{μ}, K_{μ+1} and survey constantly the literal with the number ν_{0} − 1. This literal is included (temporarily) in the reduced writing of the conjunction, while when passing from K_{i} to K_{i+1} the previous writing relating to K_{i} is canceled. Thus, having reached K_{μ+1}, we can determine the literal λ̃ of the conjunction K_{μ+1} with the number ν_{0}−1. If λ̃ ≠ m_{ν_{0}−1}, then our task is fulfilled for μ + 1. If λ̃ = m_{ν_{0}−1}, then the same can be repeated for the number ν_{0} − 2 of the literal, and in this case the previous writing for ν_{0} − 1 is canceled. If μ + 1 is the number of the non-last conjunction, then there exists the unknown number ν_{1} which can be found.

It is easy to see that in computations with the use of the algorithm 𝔄 the length of the writing does not exceed the length of the writing of the conjunction from Δ^{+} multiplied by a constant c, i.e., cm^{3} log_{2} m. The main lemma and the reasonings preceding this lemma result in the validity of the following

Theorem. There exists an algorithm which for any formula Q from the class MLSUn^{(1)} determines the validity of Q and needs the space cn^{3} log_{2} n, where n is the length of Q.

References

1. A. Ferro et al., Decision procedures for elementary sublanguages of set theory. I. Comm. Pure Appl. Math. 33(1980), 599–608.

2. M. Breban and A. Ferro, Decision procedures for elementary sublanguages of set theory. III. Advances Appl. Math. 5(1984), 147–215.

3. M. R. Tetruashvili, The complexity of decision of the validity problem for an elementary sublanguage of quantifier-free set theory. (Russian) Bull. Acad. Sci. Georgian SSR 126(1987), 245–247.

(Received 23.12.1993)

Author’s address:

I. Vekua Institute of Applied Mathematics, Tbilisi State University 2, University St., Tbilisi 380043, Republic of Georgia