BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1352
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: The Complexity of Set Constraints
AUTHOR:: Aiken, Alexander
AUTHOR:: Kozen, Dexter
AUTHOR:: Vardi, Moshe 
AUTHOR:: Wimmers, Ed
DATE:: May 1993
PAGES:: 26
ABSTRACT::
Set constraints are relations between sets of terms. They have been used 
extensively in various applications in program analysis and type inference. We 
present several results on the computational complexity of solving systems of 
set constraints. The systems we study form a natural complexity hierarchy 
depending on the form of the language.
END:: CORNELLCS//TR93-1352
BODY::
The Complexity of
Set Constraints
Alexander Aiken*
Dexter Kozen**
Moshe Vardi*
Ed Wimmers*
TR 93-1352
May 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*IBM Almaden Research Center, 650 Harry Road, San Jose, CA 95120.
**Computer Science Department, Cornell University, Ithaca, NY 14853.
The Complexity of Set Constraiiits
Alexander Aiken*			Dexter Kozent
aiken?alrnaden. ibm. corn			kozen?cs cornell .edu
Moslie Vardi*			Ed Wimmers*
vardi?alrnaden. ibm. corn			wimmers?almaden Ibm. corn
May 10,1993
Abstract
Set constraints are relations between sets of terms. They have been
used extensively in various appllcations in program analysis and type
inference. We present several results on the computational complexity
of solving systems of set constraints. The systems we study form a
natural complexity hierarchy depending on the form of the constraint
language.
1 Introduction
Systems of set constraints have received considerable attention as a formal-
ism for expressing algorithms in program analysis and type inference. Many
algorithms based on set constraints have been proposed and implemented,
but very little is known about the computational complexity of solving sys-
tems of set constraints. In this paper we present complexity results for a
natural hierarchy of decision problems involving set constraints.
Set constraints are formal inclusions between expressions representing
subsets of T?, the set of ground terms over a finite ranked alphabet ?. A
*IBM Almaden Research Center, 650 Barry Road, San Jose, CA 95120
tComputer Science Department, Cornell University, Ithaca, NY 14853
positive set constraint is an inclusion E C F, where E and F are expressions
built from a set X = [r, ?,...] of variables ranging over subsets of T?, a
constant 0 denoting the empty set, a constant 1 denoting the set T?, the usual
set-theoretic operators U (set union), fl (set intersection), and ?(complement
in T?), and an n-ary set constructor f for each n-ary symbol f c ? with
semantics
f(Ai,...,An) = [fli...tn Ii E Aj, 1 <i ?
Any valuation
a : X H 2T?
assigning a subset of T? to each variable extends uniquely to a map
a : [set expressions] 2Th
A valuation a satisfies the constraint E C F if a(E) C a(F). A set 8 of
constraints is satisfiable if there is a valuation that satisfies all constraints in
8 simultaneously.
An algorithm for determining the satisfiability of general systems of pos-
itive set constraints was first presented in [4]. In this paper, we extend the
results of [4] in two ways. In Section 5, we give a new characterization of
the satisfiability problem that may be of independent interest. We show
that deciding whether 8 is satisfiable is equivalent to deciding whether or
not a certain finite hypergraph constructed from 8 has an induced subhy-
pergraph that is closed (see Section 4). This characterization is simpler than
the one in [4] and has the additional advantage for complexity analysis that
the hypergraphs can be specified using short Boolean formulas.
In Section 6, we exploit the hypergraph characterization of the satisfia-
bility problem to obtain a family of complexity results for the satisfiability
problem. We obtain an exhaustive hierarchy of completeness results for var-
ious complexity classes depending on the number of elements of ? of each
arity. To the best of our knowledge, these are the first upper and lower bound
results for set constraint problems other than the NEXPTL4iE-completeness
result for the general problem, which has been obtained independently by
[5]. Our complexity results are summarized in the following table.
2
number of elements int?0f complexity of the
arity			0			arity			1			arity			2?			satisfiability problem
0			0+			0+			trivial
1+			0			0			NP-complete
1+			1			0			PSPACE-complete
1+			2+			0			EXPTIME-complete
1+			0+			1+			NEXPTIME-complete
Intuitively, these results can be explained as follows. lf Z has only nullary
symbols, then the problem is essentially Boolean satisfiability. A system with
one unary symbol has the power to connt in unary, which is sufficient to simu-
late a PSPA CE computation. A system with at least two unary symbols can
encode alternation, which gives alternating P5PA CE or EXPTIME. Finally,
in a system with at least one symbol of arity two or greater, there can be
constraints such as fxy C 0 which is satisliable iff either x C 0 or y C 0.
This allows the system to encode nondeterministic choices, which raises the
complexity to NEXPTIME.
In a companion paper [1], we consider systems with negative set con-
straints E ? P. Negative constraints considerably increase the power of the
constraint language. With negative constraints, the complement of the set of
solutions of a system of positive constraints can be expressed as a disjunction
of a set of negative constraints: 0 does not satisfy the system S iff a satisfies
? E?F
EC FES
Generalizing this observation, any Boolean combination of positive and neg-
ative constraints can be expressed as the disiunction of systems of positive
and negative constraints. We show in [1j that it is decidable whether a sys-
tem of positive and negative constraints is satisfiable. This result is proved
by means of a reduction to a number-theoretic problem which may be of
independent interest.
2 Applications and Related Work
The greatest interest in set constraints stems from the area of program anal-
ysis, where set constraints have been used for a number of years in many
3
different settings [16,12, 14,15,17,10, 2, 3]. In these applications, set con-
straints are generated from the program text and then solved to obtain useful
information about the program (e.g., whether it is well-typed). Representing
basic data structures such as lists requires binary symbols; our results show
that in this general case, solving set constraints is NEXPTIME-complete. In
practice, implementations of set constraint solvers introduce restrictions or
heuristics specific to the problem domain to achieve better worst-case time
complexity. Our results show that such techniques are in fact necessary to
achieve more efficient implementations.
Most of the systems for program analysis cited above deal with only
positive set constraints. In [2, 3], opportunities for program optimization are
identified by an ad hoc technique for checking the satisfiability of negative set
constraints; the results of [1] show that satisfiability of negative constraints
is decidable in general.
Special cases of set constraints have also arisen naturally in the study of
finite automata. An example is an algorithm for solving equations between
regular languages with free variables [6]. In [6], no complexity analysis is
given. There is a simple linear-time reduction of regular expressions to sys-
tems of set constraints over unary and nullary symbols. Thus, our results
show that deciding the satisfiability of equations between regular languages
with free variables is in EXPTIME.
Set constraints with only nullary symbols correspond to Boolean algebras
over a finite set of atoms. See [13] for more general results on solving negative
constraints in arbitrary Boolean algebras.
Finally, set constraints have been studied for their own sake and several
algorithms for solving set constraints have been proposed [9, 4, 8]. Our results
differ from these in that we are interested primarily in the complexity of the
satisfiability problem for set constraints.
3 Set Expressions and Set Constraints
Let ? be a finite ranked alphabet consisting of symbols J, each with an
associated arity arity(f) ? N. Symbols in ? of arity 0,1, 2, 3, 4, and n are
called nullary, unary, binary, ternary, quaternary, and n-ary, respectively.
Nullary elements of ? are often called constants. The set of elements of Z of
arity n is denoted ??.
4
The set of ground terms over Z is denoted T?. This is the smallest set such
that if tj,...,tn Ei T? and f E Zn, then f11...tn c T?. If X fx,y,...t
is a set of variables, then T?(X) denotes the set of terms over ?? and X,
considering the elements of X as symbols of arity 0.
Let B = (u, n, N? 0, 1) be the usual signature of naive set theory. Let
? + B denote the signature consisting of the disjoint union of ? and B. A
set expression over X is any element of T?+B(X). The following is a typical
set expression:
f(g(xUy),?g(xfly)) U a
where f E ?2, g E ?i, a E ?o, and x,y ? X. Set expressions are denoted
E,F
A constraint is a formal inclusion  C F, where E and F are set expres-
sions. We might also allow equational constraints E = F, although inclusions
and equations are interdefinable.
We interpret set expressions over the powerset 2Th of T?. This forms
an algebra of signature ? + B where the Boolean operators have their usual
set-theoretic interpretations and elements f E ?? are interpreted as functions
f: (2T?)n H
f(Ai,...,An) = ffti...tn Ii C Aj, 1 ? i ?
A set assignment is a map
a : X H 2T?
assigning a subset of T? to each variable in X. Any set assignment a extends
uniquely to a (? + B)-homomorphism
a: T?+B(X) H 2T?
by induction on the structure of the set expression in the usual way. The set
assignment a satisfies the constraint E C F if a(E) C a(F). A family 8 of
set constraints is satisfiable if there is a set assignment that satisfies all the
constraints in 8 simultaneously. The satisfiability problem is to determine
whether a given finite system 8 of set constraints over ? is satisfiable.
5
A Bootean expression over X is any element of TB(X) (i.e., a set expres-
sion with no symbols from ?). A truth assignment is a map
u:X H 2
where 2 = fO, 1? is the two-element Boolean algebra. Any truth assignment
u extends uniquely to a B-homomorphism
u : TB(X) H 2
inductively according to the rules of Boolean algebra. If X = ....... , Xm?,
we use the notation
B[x? :=
to denote the truth value of the Boolean formula B under the truth assign-
ment Xj I" ?, 1 <i ?
3.1 Normal Form
We show in this section how to transform a given system 8 of set constraints
into an equivalent system in a special normal form. This step simplifies the
proof of correspondence between set constraints and hypergraphs, because
the normal form is actually quite close to the hypergraphs defined in Sec-
tion 4. The transformation to normal form does not significantly increase
the size of the system.
1.
For every subexpression ..... . En of some set expression in 8, where
f E ??, let Yo,Yi,... , y? be new variables, replace all occurrences of the
subexpression ..... . En by Yo, and add new constraints Yo = ..... yn
and yj = Ej, 1 ? i <n. Continue until all constraints are either purely
Boolean constraints (i.e., do not contain any occurrence of f ? or
are of the form
Yo = ..... . yn
where f ? ?? and YO,Yl,...,Yn are variables. Let X = fxi,...,xml
be the set of all variables occurring in 8 at this point.
6
2. For each f Ei ??, introduce a new set of variables
=			0 < i < n, 1 ? j < ml
and add the constraints
J
Z0j = f $H..1 fl .j
= f?1x5?1
i--Hi
for all 1 <i < n and 1 ? 5 ?
3. Each constraint
Xj0 = fxj1 . . . Xj?
obtained in step 1 is equivalent to the constraint
3?? flflrj2l...1 n n fi.__1x
Xj0 = fx' 1			1			____			..
fl--Hi			n--H2			fl--Hi
which in turn is equivalent to the conjunction of constraints
f?1flxj0 = frji$H..1 flflrj2$H..1 n . n f?1xj
fl--Hi			n--H2			fl--Hi
g 1... 1 n x50 = 0			g # f, m = arity(g)
Replace the constraint (1) with the constraints
(1)
m?j0 = fl zt??:
i=1
z&0 = 0 ,			$ f
Because of the constraints introduced in step 2, the resulting system is
equivalent.
4. At this point we have
o+ purely Boolean constraints formed in step 1 involving only the
variables X
7
o+ for each f E ?, purely Boolean constraints formed in step 3 in-
volving only the variables Zj
o+ the mixed constraints formed in step 2.
Replace each purely Boolean constraint E C F involving the variables
X by the equivalent constraint
NEUF = 1
Let B be the conjunction of all the left hand sides of such constraints,
and replace all these constraints in 8 with the single constraint B = 1.
Do the same for the purely Boolean constraints involving the variables
Zj to get a single constraint Cj = 1 for each f ?
After this translation, 8 contains
o+ a constraint B = 1, where B ? TB(X)
o+ for each f Ei ?, a constraint Cj = 1, where Cj c TB(ZJ)
o+ constraints
4			=			f4:H.1 n r?
4			=			f Q*..1 Xj 1...1
for each f ? ?? and each 1 ? i <n 1 ? j < m.
This is the desired normal form.
4 Hypergraphs
For our purposes, a hyperyraph is a structure
H = (U, Ej i c I)
consisting of a finite set U of verlices and an indexed family of relations Ej
of various arities on U called hyperedge relations. An element of an n-ary
8
hyperedgerelation is called an n-ary hyperedge. (In our application, the index
set I is the ranked alphabet ?, and for f c ?, arity(j) is arity(f) t 1.)
If H is a hypergraph on vertices U and if U' C U, the induced subhy-
pergraph of H on U' is the hypergraph H' on vertices L'?, whose hyperedge
relations are the hyperedge relations of H restricted to U'. That is, if
then
where if Fj is n-ary then
H = (U, Et i C I),
= (U', Et' I i ? I)
= Ej fl (U')?.
An (n + 1)-ary hyperedge relation E of the hypergraph H is closed if for
each n-tuple ..... . , E U?, there exists uo E U such that (u0,u1,... , Un) E
E. In the case n = 0, this definition just says E fl U # ?. Abusing notation,
we can think of E as a function
where
E:U? ??
E(u1,.. . ,un) = fuo I (u0,u1,. .. ,un) E E?
In this view the hyperedge relation E is closed iff E(u1,... `Un) # ? for each
n-tuple ..... . , Un ? U?. The hypergraph H is closed if all its hyperedge
relations are closed.
The hypergraph closure problem is the problem of determining whether a
given hypergraph has a closed induced subhypergraph.
Example 1 Consider the hypergraph consisting of vertices Z?, the field of
integers modulo a prime p, and a single ternary hyperedge relation
E = f(a, b, ab) a, bE Zp?
This hypergraph is not closed because there is no a E Zp such that (a, 0,1) E
E. However, the induced subhypergraph on the nouzero elements of Zp is
closed, since for all b, c E Zp --H tot there exists an a E Zp --H tot such that
(a, b, c) E E, namely a = c/b. E
9
4.1 Succinct Specification of Hypergraphs
We work with a particular class of hypergraphs whose vertices and hyperedge
relations are specified succinctly by Boolean formulas in the following way.
Let
X = txi,. .,Xmt
Zi = fz4 0 ? i ? arity(f), 1 ? 5 ? rnJ , f E V?
be pairwise disjoint sets of variables. Suppose we are given Boolean formulas
B			c			TB(X)
Cj			c			TB(ZJ),			f E ?
These formulas determine a			hypergraph
H			=			(U, Ej			f E Z)
as follows. The vertex set U is the set of all truth assignments u : X			2
satisfying B. Each such truth assignment corresponds to a conjunction of
literals (also denoted u) in which each variable in X occurs exactly once,
either positively or negatively, such that u C B tautologically. The variable
x occurs positively iff u(x) = 1. AVe occasionally call the elements of U aloms
because they represent atoms of the free Boolean algebra on generators X
modulo B = 1. Each Boolean expression over X is equivalent modulo B = 1
to a disjunction of atoms.
For each f c ??, the hyperedge relation Ef of H is defined to be the set
of all (n t 1)-tuples ....... ,tin) E U?+1 such that
Ci[zt?j := ui(xj)1 = 1			(2)
Intuitively, we think of the formula Cj as a Boolean valued mapping on
+ 1)-tuples of truth assignments to X To emphasize this intuition, we
abbreviate the left hand side of (2) by
Thus
Cj[uo,.. ,Un]
,Un) E Ej iff Cj[uo,. . ,un] = 1
In general, the size of the hypergraph can be exponential in the size of
its specification.
10
5 Set Constraints and Hypergraph Closure
In this section we give an efficiently computable correspondence between
systems of set constraints in normal form as described in Section 3.1 and
hypergraphs specified by systems of Boolean formulas as described in Section
4.1. A system of set constraints is satisfiable iff the corresponding hypergraph
has a closed induced subhypergraph. Let
x =
= tztIi O<i?arity(f), 1?j<?mt, fC?
be pairwise disjoint sets of variables. The system 3 in normal form consisting
of constraints
B = 1, B?i??(X)
Cj = 1 , Cf E TB(ZJ), f C
and for each f E ??, 1 < i ? n and 1 < j ? rn
Zod = f 1...1 fl Xj			(3)
f
Zjj = f 1... lXjl.. .1			(4)
t--H1
corresponds to the hypergraph H specified by the formulas B and Cf, f E ?.
Theorem 2 The hypergraph H has a ctosed induced subhypergraph j and
onty f the system 8 of set constraints is satisfiabte.
Proof. (?) Let
= (U', E11 f ?
be a closed induced subhypergraph of H. De?ue 0 : T? H U, inductively
such that for all f? ?? and t1,...,tn c T?,
0(f11...tn) ? Ef'(()(t1),...,()(tn))
11
This is possible since H' is closed. Each 0(1) is a truth assignment to X
satisfying B. For each term 1o of the form fli. . In, extend 0(10) to a truth
assignment to X u Z1 as follows:
0(1o)(z$5) = 0(1?)(r?) , zt!j E Z1			(5)
Define a set assignment a as follows.
= tI I O(I)(xj) = it
= a(f1...1x?1...1)
i--Hi			n--Ht
a(z45) = a(J1...1 flxj)
for f ? ??, 1 < i <n and 1 ? j <rn. We show that a satisfies s.
It is immediate from the definition of a that the constraints (3) and (4) are
satisfied. We now show that a satisfies B = 1. For 1 ? T?, let %t : 2T? H 2
be the characteristic function
By definition of a,
= ol: 1lfft1E?j?
xt(a(x?)) = 1 ? I E a(x?)
? 0(I)(x5) = 1
(6)
so xtoa and 0(1) agree on X. Since both are B-bomomorphisms (?.e., preserve
Boolean operations), they agree on all elements of T?(X); in particular, they
agree on B. Since O(I)(B) = 1 for all I by definition of LJ, we have that
xt(a(B)) = 1 for all I. Thus a(B) = =
Finally, we show that a satisfies Cj = 1. Recall that Cj is a conjunction of
constraints of the form NE u F, where E and F are either 0 or a conjunction
of elements of Zf. Since a satisfies (3) and (4), it also satisfies E C f $H..1.
By Boolean reasoning it follows that a also satisfies
Nf 1...1 C NE C NEUF
n
12
therefore
Nf 1...1 C Cj
Thus it remains to show that a satisfies
f $H..1 C Cj,
or in other words, for all terms 1o of the form .....
1o E a(Cj)
As above, we argue that Xt0 0 a and 0(1o) agree on Zj:
O(t0)(%!5) =
by (5)
Ii			? a(x,)			by (6)
toCa(f1...1x51...1)			by definition ofa
i--Hi
= x?(a(%))			since a satisfies (4)
for 0 < i ? n and 1 < j ? rn. Since both Xt0 o a and 0(to) are
homomorphisms, they agree on all elements of T?(Zj); in particular, they
agree on Cj. Since
we have
(0(to),0(h),			,0(m)) ? E1,,
CJ[Z$) := O(l?)(?)] = 1
Cj[z4 := O(to)(z$.5)] = 1
O(to)(Cj) = 1
?t0(a(Cj))
to E a(Cj)
Cj[O(t0),...,O(tn)i = 1 ?
=1
(?) Suppose a satisfies S. Regarding ti E U as a conjunction of literals,
Ul = fu ? LJ a(ti) # ??
let
13
We claim that the induced subhypergraph
= (U', Ej' f E ?)
of H is closed. For f ? Zn and for all u1,U? E U', let I? ? a(ti?),
1 < i < n. The tj exist by definition of U'. There is a unique atom u0 such
that to = ..... . ? a(uo), and ?o Ei U'.
Extend u0 to domain X u Zj by defining uo(%-) = ui(xj), 0 < i < n
1 < j <rn. Then
ui(xj)
0 ,			otherwise
1,			if? = 0 and 1o ? a(x5)
1			if? >1 and toE a(fl...1xj?1)
t--H1			fl--Hi
0,			otherwise
1			if? --H 0 and to E a(z01?)
--H			1			if? > 1 and to E
0,			otherwise
Since u0 and Xt0 0 a agree on Zj and both are I3-homomorphisms, they agree
on Cj. Thus
uo(Cj) = ?t0(a(Cj)) = 1,
since a satisfies C1 = 1. Then
uo(Cj) = 1 ? Cjkt!3 := Uo(Z$j)j = 1
?			:= ui(xj)] = 1
?			Cj[uo,u1,.. .,unj = 1
=i			(U0,Ui,...,Un)EEj.
Since the Uj are in U', we also have
(u0,u1,.. . ,un) E Fj'
E
Thus H' is closed.
14
Corollary 3 The following Iwo decision problems are efficiently interreduc-
ible:
(i) Given a system S of set constraints, is it satisfiable?
(ii) Given a hypergraph H spec?ed by Boolean formulas, does it have a
closed induced subhypergraph?
6 Complexity Bounds
In this section we give complexity bounds for a hierarchy of satisfiability
problems for systems of set constraints based on the arities of the elements
of ?. By Theorem 2, we are free to work with either the constraints S directly
or the hypergraph H. It is usually easier to deal with H because it is a finite
object, whereas in general S involves infinitely many terms and can have
infinitely many solutions.
The results of this section are summarized in the following table.
numberofelementsin?of complexity of the
artly			0			arity			11			arity			2+			satisfiability problem
0			0+			0+			trivial
1+			0			0			NP-complete
1+			1			0			P5PACE-complete
1+			2+			0			EXPTIME-complete
1+			0+			1+			NEXPTIME-complete
The first line of the above table is really a triviality, because with no constants
in ?, the set of ground terms T? is empty. We handle each of the other cases
separately.
6.1 Nullary Symbols
With at least one constant in Z but no symbol of higher arity, we have
= = ?o. In this case the satisfiability problem is NP-complete. The
hypergraph H has only unary hyperedge relations, and the closure problem
amounts to determining whether for each c E Z there exists a truth assign-
ment u satisfying both B and Cj (in the sense that u(B) = 1 and Cc[u] = 1).
This is essentially Boolean satisfiability.
15
6.2 One Unary Symbol
6.2.1 PSPACE Upper Bound
Suppose ? consists of one unary symbol f, one or more constants, and no
other symbols. Then the hypergraph H is simply a conventional directed
graph with binary edge relation Ej and a distinguised subset Ec for each
constant c. The vertices U are the truth assignments satisfying a Boolean
formula B, the edge retation Ej is the set of pairs (u, v) ? U2 such that
Cj[u, v] = 1, and the distinguished subset Ec of U is the set of u such that
Cc[U] = 1. In this case, the closure problem is to determine whether there is
a subset U' of U such that
o+ each Ec intersects U'
o+ for any v E U' there is a u Ei U' such that (u, v) ? Ej.
This can be determined nondeterministically in linear space as follows. For
each constant c in turn, guess %` C Ec and verify that Ec[v] = u(B) = 1.
Starting from u, guess an Ej-path of length 2? + 1, where n? = xI. At each
step, verify the new vertex v by evaluating v(B) and the new edge (v, w) by
evaluating Cj[v, w]. If such a path is found for all c, accept.
Since U ? 2?, any Ej-path of length 2? + 1 must repeat a vertex.
Thus the procedure accepts ilf for every nullary c ? ? there is an Ej-path
uO,ul,.. .,uk such that u0 E Ec and Uk = Uj for some j < k. The induced
hypergraph on the set of all such Uj for all c is closed. Conversely, any closed
induced subhypergraph must contain an induced subhypergraph of this form.
This procedure requires only linear space to record the current vertex, Tn
bits for a counter, and enough space to evaluate the formulas. Thus the algo-
rithm runs in nondeterministic PSPACE, which is the same as deterministic
P5PACE by Savitch's Theorem [11].
6.2.2 P5PACE Lower Bound
We show that the problem of deciding whether a system with one unary
symbol f and one constant c is satisfiable is PS?A CE-hard by a reduction
from the halting problem for linear-bounded automata (LBA), a well known
P5PA CE-complete problem. Consider an LBA M and input string w of
length n. A configuration of M on input w is an instantaneous description
16
of M's current tape contents, state, and head position. Each legal configura-
tion is represented as a string of symbols of length n over a finite alphabet.
Assume without loss of generality that there is a unique accept configuration
and a unique reject configuration on inputs of length n, that all computa-
tion paths of M halt and either accept or reject (equip M with a binary
exponential-time counter if necessary), that the accept configuration enters
a trivial loop, and that the reject configuration has no successor.
The configurations of Al on w can be encoded as truth assignments to
Boolean variables
Aj = "symbolais written on tape cell j", 1?5?n, acF
Qj = "M is in state q scanning tape cell 5", 1 <5 < n, q E Q
These variables comprise the set X. One can write down short formulas
describing the action of M on input w:
o+ a formula B describing all legal configurations (exactly one symbol
occupying each tape cell, exactly one current state, exactly one tape
cell currently being scanned);
o+ a formula Cc describing the start configuration of ?I on input w (the
symbol occupying tape cell 5 is the 5th symbol of w and M is in state
5 scanning the leftmost tape cell);
o+ a formula C1[u, vj describing legal pairs of configurations such that u
follows from v in one step according to the transition rules of M
The encoding technique is similar to that used in the proof of Cook's The-
orem; see [11] for details. Then M accepts input w if and only if the hy-
pergraph specified by B, Cc, and Cj has a closed induced subhypergraph
consisting of the configurations in the accepting computation path.
6.3 Two or More Unary Symbols
6.3.1 EXPTIME Upper Bound
With two or more unary symbols, one or more constant symbols, and no
other symbols, consider the following deterministic exponential-time algo-
rithm for determining whether the specified hypergraph has a closed induced
17
subhypergraph. Write down all truth assignments to X and delete those not
satisfying B. For each remaining u, check whether it has an Ej-successor for
all unary f and delete it if not (inductively, such a u cannot be contained in
any closed subhypergraph). Repeat until no more vertices are deleted. The
resulting subhypergraph contains all closed subhypergraphs, and is closed
itself if for each nullary c there is a u ? Ec. There are at most 2m truth
assignments, and the tests can be done efficiently by evaluating Cj [u, v] and
Cc[u].
6.3.2 EXPTIME Lower Bound
The exponential time lower bound for two unary symbols is obtained by
generalizing the lower bound construction for one unary symbol. Instead
of a deterministic LBA, we encode an alternating LBA M on input w [7].
We assume without loss of generality that M has no negating transitions,
that there is a unique accept and a unique reject configuration for inputs
of length n, that M alternates strictly between universal and existential
branches, that all branches are at most binary, that the start, accept, and
reject configurations are universal branches, that all computation paths either
accept or reject, that the unique accept configuration enters a trivial loop,
and that the unique reject configuration has no successor. We will construct
a hypergraph that has a closed induced subhypergraph iff ?NI accepts w.
Let a be a universal configuration with successors ?O and ol in lexico-
graphical order. By assumption, oO and al are existential configurations.
Let oOO and cOl be the two successors of aO and let etO and oil be the two
successors of at in lexicographical order. Then aOO, aOt, otO, and ott are
universal configurations.
As in Section 6.2.2, we let B and Cc be Boolean formulas describing the
set of all legal configurations and the start configuration, respectively. In
addition, we let Cj describe the relation consisting of all pairs (a, oOO) and
(a, oOt), and we let C? describe the relation consisting of all pairs (a, atO)
and (a, ott). The idea is that in the semantics of alternat?ng Turing ma-
chines, a leads to acceptance iff both oO and ol lead to acceptance, which
occurs iff at least one of oOO or aOt leads to acceptance and at least one of
olO or ott lead to acceptance. Thus M accepts the input w iff there is a
closed induced subhypergraph consisting of an accepting computation tree
of M
18
6.4 One Binary Symbol
6.4.1 NEXPTIME Upper Bound
With any number of symbols of any arity, we can determine in nondetermin-
istic exponential time whether there exists a closed induced subhypergraph
by guessing a subset U' C U and verifying that the induced subhypergraph
on U' is closed; i.e., for all u E U', u(B) = 1 and for all f ? Zn and
E U', there exists a u0 E Ej(u1,... , Un) fl U'. The set U has at
most 2m elements, where rn is the number of variables, and the predicates
Cj[uo,... , Un] require polynomial time to evaluate. The entire algorithm runs
in nondeterministic exponential time.
6.4.2 NEXPTIME Lower Bound
We show first that with a constant c and one ternary symbol f, we can
encode computations of a nondeterministic exponential-time Turing machine.
In Section 6.5 we show later how to reduce f to binary. Let M be such a
machine with time and space bound N = 20(n). Without loss of generality,
assume that M starts in its start state scanning the left endmarker k, that it
has unique accept and reject configurations on inputs of length n and that all
computation paths lead to acceptance or rejection, that all nondeterministic
branches are at most binary, that once M accepts or rejects it enters a trivial
loop in which it remains in the same state.
Computation histories of M on inputs of length n can be represented as
N x N matrices. Each row i of the matrix encodes a possible configuration of
M at time i. The jjth entry of the matrix records the symbol occupying the
5th tape cell at time i and whether that cell is being scanned by the machine
at time i. If so, the current state of the finite control is also recorded. An
accepting computation history of M on input w is represented by a matrix
whose first row encodes the start configuration of M on input w, whose ? + 1st
row follows from the zth by the transition rules of M, and whose final row
N --H 1 encodes the accept configuration.
Given M and input w = .... . W?, we construct Boolean formulas B, Cc
and Cf specifying a hypergraph
H = (U, Ec, Ej)
where c is nullary and f is ternary (thus Ec is a unary and E1 is quaternary).
19
Each entry of the matrix is represented by a vertex of the hypergraph, which
is a truth assignment satisfying B. The hyperedge relation Ej enforces con-
straints between adjacent entries. The hypergraph has a closed induced
subhypergraph if and only if there exists a matrix representing an accepting
computation history of M.
We first define the set of Boolean variables X. There is a variable Aa for
each symbol a of the tape alphabet, a variable Qa for each machine state q,
m = [log2 Ni variables 1o,???, 1m-1 encoding the time (row number of the
matrix) in binary, m variables .0...., 5m-1 encoding the position of the tape
cell (column of the matrix) in binary, and a variable choice determining the
nondeterministic choice.
The vertices of the hypergraph are the truth assignments to X such that
at most one state and exactly one tape symbol have Boolean value 1. This
is specified by the formula
B = (UAa) A fl(NAaUNA6)
a			a#b
A fl (NQpU NQq)
Each truth assignment u to X corresponds to an index ij into the array,
o < ij < N --H 1, where i and 5 are the numbers encoded in binary by the
truth values u(tk) and u(sk), 0 ? k ? m --H 1. We denote i and 5 by lime(u)
and space(u), respectively. Also, each u satisfying B has exactly one symbol
a with u(Aa) = 1, which we denote by sym(?). Finally, each u satisfying
B has at most one state q with u(Qq) = 1, which we denote by slate(u). If
u(Qq) = 0 for all states q, we write stale(u) = I.
We will need to perform modular addition and comparisons on numbers in
the range 0 < i < N--H1 in terms of their binary representations. For example,
we need formulas expressing conditions such as time(u) = lime(v) + 1 and
time(u) > time(v). These constructions are quite easy and well known, so
we omit the details.
The unary predicate Cc specifies the 00th entry (upper left corner) of
the matrix. It specifies that the machine is in its start state 5 scanning the
leftmost tape cell, which contains the left endmarker k:
Cc[u] = (lime(u) = 0) A (spacc(u) = 0) A Qs A A?
20
There are exactly two truth assignments satisfying B and Cc, one for each
value of choice, and one of these must be contained in any closed subhyper-
graph.
The quarternary predicate Cj[u, v, w, serves several purposes. It is
defined as the conjunction of several formulas describing the format of con-
figurations, the initial configuration (first row of the matrix), the final con-
figuration (last row of the matrix), and the legal transitions.
First we specify that there is at most one truth assignment for every
(time(w) = time(x) A space(w) = space(r)) ? w = x
zj:
(7)
Inclusion of this formula as a conjunct of C![u, v, w, x] guarantees that there
can be no closed induced subhypergraph containing two distinct vertices w
and x such that lime(w) = lime(r) and space(w) = space(x).
We also wish to specify that for every i, the value of the variable choice
at all tape cells in row i of the matrix is the same:
time(w) = lime(x) ? (w(choice) = r(choice)) (8)
To specify the initial configuration, we must ensure that the first n tape
cells after the left endmarker contain the input string w = .... W?, that all
remaining cells to their right except the last contain the blank symbol ?, the
last tape cell contains the right endmarker ?, and no other cell besides the
leftmost contains a state:
(v = w = ? A time(v) = 0 A space(v) ? N --H 1)
? (lime(u) = 0 A space(u) = space(v) t 1 A siatc(u) = ffi
A fl(space(u) = i ? sym(?) = Wi)
i=1
A n < space(u) < N --H 1 ? sym(u) =
A space(u) = N --H 1 ? sym(u) =H)
(9)
If the premise of (9) is true of v, w and x, then there is exactly one choice
of u that satisfies the conclusion. The two truth assignments satisfying Cc
satisfy the premise of (9), and it can be shown inductively that any closed
subhypergraph must contain the entire first row of the matrix representing
the initial configuration.
21
To capture valid transitions of the machine, we write
(time(v) = time(w) = time(x) < N --H 1
n space(x) = space(w) + 1 = space(v) + 2)
? (time(u) = time(w) + 1 n space(u) = space(w) (10)
n (sym(u), state(u)) =
nexl(choice(v), sym(v), slate(v), sym(w), staie(w), sym(x), slate(x)))
where the function next encodes the transition relation of M. The nondeter-
ministic choice is determined by the value of the variable choice. Addition
in this expression is modulo AT. We are using the fact that the state and
symbol at time i + 1 and position j depends only on the state and symbol
at time i and positions j --H 1, j, and j + 1. The function next also encodes
the fact that if the machine is not scanning tape cell ) at time i, then the
symbol on tape cetl j is unchanged at time i + 1.
By (9), any closed subhypergraph contains the start configuration of the
computation. Inductively, assume any closed subhypergraph contains the
first i configurations. By (8), entries in configuration i must agree on the
value of the variable choice. Furthermore, given any v, w, and x satisfying
the premise of (10), there are exactly two u satisfying the conclusion of (10)
with different values of choice but oth&wise identical. One of these must be
in any closed subhypergraph.
Finally, we need to check that the accept state occurs someplace in the
last row of the matrix. Since the machine has either accepted or rejected by
time N --H 1, and since we have already insured that the matrix accurately
encodes a computation history, we need only check that the reject state r
does not occur in the last row. We use the formula
time(x) = N --H 1 ? state(x) # r .			(11)
Finally, we define Cj[u,v,w,x] to be the conjunction of (7), (8), (9), (10),
and (11).
We have argued that the problem of deciding whether a given system of
constraints with one ternary and one nullary symbol is satisfiable is NEX-
PTIME-complete. It will follow from the result of the next section that
the problem with one nullary and one binary symbol is also NEXPTIME-
complete.
22
6.5 Symbols of Greater Arity
In this section we show that any system with symbols of arbitrary arity can
be rednced to a system with a single binary symbol and a single constant.
By the results of Section 6.4, it suffices to prove this result for a signature
with one ternary symbol and one constant. This will establish the NThN'P-
TIME-completeness of the satisfiability problem for systems with at least
one constant and at least one symbol of arity two or greater.
Let F = fy, bJ and let ? = ff, at, where a and 6 are constants, f is binary,
and g is ternary. Let B, Cb, and C9 be formulas describing a hypergraph
H = (U, E6, E9),
where Eb is unary and E9 is quaternary. Define a new hypergraph
H = (U, Fa, Ej)
specified by formulas B, Cj, and Ca, as follows. The vertices of H are
U = UU(UxU)
Elements of U x U are denoted (v, v). If X is the set of variables used in the
definition of H such that elements of U are truth assignments to X, then we
can take U to be a set of truth assignments to X u x' u fzt, where X' is a
disjoint copy of X and z is a new variable whose sole purpose is to distinguish
between U and U x U. We define B, Cj, and Ca such that
= B[uj
B[(u, v]) = B[u] fl B[v]
Ca [v] = Cb[u]
Ca[(u,v)] = 0
Cj[(v,w),v,w] = 1
Cj[u,v,w] = 0
Cj[v,(v,w),x] = C9[v,v,w,x]
C1[(I, v), (v, w), x] = 0
and for q, r E & not covered by any of the preceding cases,
Cj[q,q,r] = 1
Cj[p,q,r] = 0, p#q
23
These formulas are easily derived from B, Cb, and C?. Then
EJ = (((u,v?,u,v)Iu,vEiU1
u f(u,(v,w),x) (u,v,w,x) c E9J
u f(q,q,r) (q,r) not of the form (u,v) or ((v,w),x)t
It is easily shown that the induced subhypergraph of H on vertices U' is closed
if and onty if the induced subhypergraph of H on vertices U, u (U' x LJ') is
closed.
7 Future Work
We would like to extend these techniques to projection functions. For every
symbol f E ?n, one can define a family of projection functions f-l, , f?fl
with semantics
= [ti fli ... In ?
Algorithms for solving special cases are known [16,12, 9], but substantial
restrictions must be placed on the other set operations. Projection functions
subsume negative constraints because the constraint system
sufb c f?'(fby)]
is satisfiable only if 8 is satisfiable with y # 0. The result of [1] on negative
constraints is presumably a step towards solving systems with projections.
Acknowledgement5
Dexter Kozen was supported by the Danish Research Academy, the National
Science Foundation, the John Simon Guggenheim Foundation, the U.S. Army
Research Office through the ACSyAM branch of the Mathematical Sciences
Institute of Cornell University under contract DAAL03-9l-C-0027.
References
[1] A. Aiken, D. Kozen, M. Vardi, and E. Wimmers. Decidability of systems of
set constraints with negative constraints. manuscript, January 1993.
24
[2] A. Aiken and B. Murphy. Implementing regular tree expressions. In Proc.
1991 Conf. Functional Programming Languages and Computer Architecture,
pages 427--H447, August 1991.
[3] A. Aiken and B. Murphy. Static type inference in a dynamically typed lan-
guage. In Proc. 18th Symp. Principles of Programming Languages, pages
279--H290. ACM, January 1991.
[4] A. Aiken and E. Wimmers. Solving systems of set constraints. In Proc. 7th
Symp. Logic in Computer Science, pages 329--H340. IEEE, June 1992.
[5] Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Set constraints are
the monadic class. In Proc. 8th Symp. Logic in Computer Science, page to
appear. IEEE, June 1993.
[6] J. A. Brzozowski and E. Leiss. On equations for regular languages, finite
automata, and sequential networks. Theor. Comput. Sci., 10:19--H35,1980.
[7] A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. J. Assoc. Comput.
Mach., 28(1):114--H133, 1981.
[8] R. Gilleron, 5. Tison, and M. Tommasi. Solving systems of set constraints
using tree automata. manuscript, July 1992.
[9] N. Heintze and J. Jaffar. A decision procedure for a class of set constraints. In
Proc. 5th Symp. Logic in Computer Science, pages 42--H51. IEEE, June 1990.
[10]
N. Heintze and J. Jaffar. A finite presentation theorem for approximating
logic programs. In Proc. 17th Symp. Principles of Programming Languages,
pages 197--H209. ACM, January 1990.
[11] J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Lan-
guages, and Computation. Addison-Wesley, 1979.
[12] N. D. Jones and 5. 5. Muchnick. Flow analysis and optimization of LISP-like
structures. In Proc. (ith Symp. Principles of Programming Languages, pages
244--H256. ACM, January 1979.
[13]
K. Marriott and M. Odersky. Systems of negative boolean constraints. Techni-
cal Report YALEU/DCS/RR-900, Computer Science Department, Yale Uni-
versity, April 1992.
[14] P. Mishra. Towards a theory of types in PROLOG. In Proc. 1st Symp. Logic
Programming, pages 289--H298. IEEE, 1984.
25
[15] P. Mishra and U. Reddy. Declaration-free type checking. In Proc. 12th 5ymp.
Principles of Programming Languages, pages 7--H21. ACM, 1985.
[16] J. C. Reynolds. Automatic computation of data set de?nitions. In Information
Processing 68, pages 456--H461. North-Holland, 1969.
J. Young and P. O'Keefe. Experience with a type evaluator. In D. Th?rner,
A. P. Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Com-
putation, pages 573--H581. North-Holland, 1988.
[17]
26
