|  | |||||||||
Decomposable structures, Boolean function
representations, and optimization.
Stefan Arnborg
Kungliga Tekniska Hogskolan
NADA, S-100 44 Stockholm, Sverige
stefan@nada.kth.se
Abstract. We show the connection between the theory of bounded treewidth graphs, monadic second order definable structures and sets, and boolean decision diagrams. We survey recent results in algorithms for bounded treewidth, symbolic model checking and representation schemes for Boolean functions. Some practical applications are indicated.
1 Introduction
This is a survey of a theory of tree-like graphs and other structures. Many aspects of the corresponding method have been known and practised in operations research, reliability engineering, artificial intelligence, and as special applications of dynamic programming. Problems amenable to solution by the methods are discrete optimization, reliability and dependability problems for complex systems, verification of digital designs and software and reasoning with uncertainty. I want to relate the theory of decomposability or tree-likeness to the BDD and symbolic model checking methods used in circuit and program verification and also to methods designed for reasoning in various applied logics in knowledge systems. In these areas, particularly where unstructured problems are solved, it is difficult to formulate a model and to prepare corresponding inputs to optimization programs. One solution to this problem could be the adoption by practitioners of relatively simple logical notations based on second order logic and high-level definition facilities. Similar developments have already taken place in circuit verification.
Since a complete exposition of this problem area will not fit into the present page allowance, we emphasize those aspects that fit in nicely with the presentation strategy and those that seem the most useful in applications. For a very careful and complete exposition, see the series of papers and surveys on the monadic second order logic of graphs by Bruno Courcelle. A recent bibliography is [16].
1.1 Signatures and structures
Graphs and other combinatorial objects will be represented as structures. A signature F is a set of sorts and a collection of relation and function constants. A symbol is recognized as either of these. Every relation and function constant
has a profile, which is a finite sequence of sorts. A relation constant with empty profile is called a propositional constant. A function constant with singleton profile is called an object constant. We will write a signature by listing its sorts, a semicolon, its relation constants, each followed by its profile in parentheses, another semicolon, and its function constants in a similar way. Thus, a one-sorted signature with the unary relation constant P and a binary function constant f is written (u; P (u); f(u; u) : u). A structure over a signature F is a set of disjoint domains Ds, one for each sort s, and, for each relation constant in F of profile s1; : : : ; sn, an n-ary relation table over Ds1 ? ? ? ? ? Dsn , and, for every function constant, a function table compatible with its profile. We consider only finite domains, but also infinite families of structures with unbounded domain.
Objects easily defined using structures are various types of graphs (directed, undirected, multi-), oriented and unoriented matroids, trees (ordered and unordered) etc. Another example:
Example 1. A propositional formula is representable as a structure relating formulas
and subformulas. Each logical operator used binds a formula together with
its operands. There are a number of possible signatures representing propositional
formulas. If the objects are formulas and subformulas, then one can have
unary relations to represent the operator of a formula, and a number of incidence
relations for pointing out the operator-operand relations. For propositional logic
one can thus have the signature
F = (u; P:(u); P^(u); P_(u); Op1(u; u); Op2(u; u); Root() : u). As an example,
the formula p ^ (q _:p) is represented in signature F with domain fa; b; c; p; qg
as
Root : a
P: : fcg
P_ : fbg
P^ : fag
Op1 : f(a; p); (b; q); (c; p)g
Op2 : f(a; b); (b; c)g:
Many applications deal with propositional formulas and depend on solving their satisfiability and related problems. Note that not all structures over F correspond to well formed propositional formulas.
We assume known the concept of first-order formula and satisfaction of a formula by a structure, using the intermediate concept of variable assignment[28]. Thus, if a formula is satisfied by structure I under variable assignment V we write I j= OE[V ].
A structure that satisfies a formula OE for all variable assignments V is called a model for OE, written I j= OE. If a set of structures is exactly the set of models of a first order formula OE, then the set is said to be a (first-order) definable set of structures (and defined by OE).
Example 2. The class of simple graphs is the class of structures over G1 =
(u; Adj(u; u); ) defined by: 8x8y Adj(x; y) $ Adj(y; x). This formula says that
the adjacency relation Adj must be symmetric in a graph. Similarly, the class of
directed multi-graphs can be defined in a two-sorted signature,
G2 = (u; v; It(u; v); Ih(u; v); ) with sort 'edge' u and 'vertex' v, using the head
and tail incidence relations Ih(u; v) and It(u; v) and the conditions: "Every edge
is the tail of exactly one vertex and the head of exactly one vertex". This condition
can, somewhat tediously, be defined in first-order logic with equality. But
the condition could also be built into the signature by regarding tail and head
as two functions from edge to vertex.
The second order logic is obtained from first order logic by adding variables of a new kind denoting relations or functions of a known profile and quantification over such variables. These variables can be used as the corresponding constants in atoms and terms. The satisfaction relation of first order logic is augmented so that in an assignment, a relation or function table of the right profile is assigned to a second order variable. It turns out that full second order logic is too general for our main purpose here. The monadic second order logic is the restricted logic where second order variables can only be unary relation variables, which naturally denote sets from the domain. In monadic second order logic we use set variables for unary relation variables and the set inclusion operator ae and the membership operator 2. Thus, x 2 Y is used for what in second order logic would be Y (x). We define a monadic second order definable set of structures L to be the set of structures satisfying some monadic second order formula OE, L = fI j I j= OEg.
For a formula with free variables, and for a compatible structure, satisfaction depends on a variable assignment. The set of satisfying assignments of a formula ' with respect to a structure I is the set of variable assignments for which I satisfies ', fV j I j= '[V ]g. If we have ordered the m free variables, we can represent the satisfying assignments as m-tuples, with one component for each free variable of ' (it is not difficult to see that satisfaction depends only on the assignment to the free variables). Such a set of m-tuples is called a monadic second order definable set of tuples in a structure.
It was shown by Courcelle[13] that it is not possible to 'do counting' in
monadic second order logic, i.e., it is not possible to express conditions like: 'set
X has more elements than set Y ' or 'set X has an odd number of elements'.
Following Courcelle we add to monadic second order logic the modular counting
relation constants Modr;p for p = 2; 3; : : : and r = ; : : : ; p ? 1. The meaning of
Modr;p(X) is: 'the size of X modulo p is r'. This extended logic is called S logic.
Similarly, S-definable families of structures and S definable sets of tuples are
obtained by just adding modular counting to the corresponding definitions for
monadic second order logic.
1.2 Interpretation of structures in structures.
Interpretation is a method for defining a map from structures over one signature F to structures over another signature F . We present here an extension
of Rabins interpretation concept[25]. An interpretation from signature F to signature
F is a set of MS formulas and terms over signature F . First, we have
a closed formula and a formula with one free individual variable. The map
is only defined for structures satisfying and for those structures only objects
satisfying will correspond to objects in the target structure. For every relation
constant Rn in F of profile p with jpj = n, we have in the interpretation an
MS formula OERn over F with free individual variables x1; : : : ; xn, and for every
function constant fm of profile p with jpj = m + 1 we have a formula 'fm with
the free variables x1; : : : ; xm+1. From a structure over F we can now produce
a structure over F using the following method: The domain of is the set
of objects in satisfying . The relation table for a relation constant Rn is the
set of tuples (a1; : : : ; an) such that j= OERn [x1 = a1; : : : xn = an]. The function
table for a function constant fm is a similar table with rows (a1; : : : ; am+1),
where j= OERn [x1 = a1; : : : xm+1 = am+1]. Note that it is not significant how a
structure not satisfying is mapped, and that we assume that the construction
method gives only relation and function tables over the set of objects satisfying
. If we have two classes of structures, 1 and 2, and 2 is contained in the image,
by an MS-interpretation map, of 1, then we say that 2 is S interpretable
in 1. It is important to note that the interpretability relation is transitive[5].
Example 3. A co-graph is either a single vertex graph, or the disjoint union of two co-graphs, or the edge complement of a co-graph[12]. We can represent a co-graph in the signature (u; Adj(u; u); ) and interpret it in a family of labeled binary trees so that a particular graph is represented by a tree showing the construction of the graph. Thus, a leaf of the construction tree represents a vertex of the co-graph. An internal node represents either disjoint union or disjoint union followed by edge complementation. Thus, the family of co-graphs can be interpreted in the family of binary trees with one label: (u; R(u; u); L(u; u); Pc(u); Root() : u). We express the interpretation in terms of predicates which are easy to define: The condition Term(x) means that x has neither a left nor a right son, i.e., x is a leaf; Bintree() means that the whole structure is a binary tree; and Path(x; ; y) means that the nodes in form an upward path from x to y inclusive. We define two vertices of the interpreted graph to be adjacent if the path to the root from their lowest common ancestor in the construction tree contains an odd number of nodes representing edge complementation:
? Bintree()
(x) ? Term(x)
Adj(x; y) ? 9zXY c Path(x; X; z) ^ Path(y; Y; z) ^ Path(z; ; Root()) ^
8v v 2 c $ (v 2 ^ Pc(v)) ^ Mod1;2( c) ^
8v (v 2 X ^ v 2 Y ) ! (v = z)
The following facts are well known from the classical studies of monadic logic on strings and trees:
{ The family of binary trees labeled over a finite alphabet is interpretable
in the family of unlabeled binary trees.
{ Every family of finitely labeled trees is interpretable in the family of finitely
labeled binary trees.
Moreover, every graph family of bounded treewidth, represented in signature G2, is interpretable in the family of labelled trees[5]. The corresponding proposition for graphs represented in signature G1 is less intuitive.
The related concept MS definable transduction introduced by Courcelle[14] is slightly more powerful than interpretation: the formulas of a transduction can have free variables, and one object in the domain structure can represent several, but only a uniformly bounded number of, objects in the image structure.
1.3 Structure lgebras.
A closely related way of defining structures, advocated by Courcelle, uses techniques of universal algebra. We will now use the terms sort and signature in a di erent way from before, since the algebraic view focuses on functions and values of terms.
Let be a finite set of sorts. A set F is a finite -sorted signature if F is a finite set of operator symbols and every f in F has a profile s1 ? ? ? ? ? s ! s, where is nonnegative and finite (it may be zero, which corresponds to a constant, i.e., nullary operator), and s1; : : : ; s ; s are sorts in .
An F -algebra , where F is a signature, is an association of a (not necessarily finite) domain s to each sort s and a total mapping to each operator symbol, so that f with profile s1 ? ? ? ??s ! s is associated with a map fM : s1 ? ? ? ?? s ! s. The union of the domains is the carrier of F . We write j j for the carrier of as customary. A finite algebra is an algebra with a finite carrier. A structure algebra is an algebra where the domains are structures, usually each with a di erent signature.
We denote by (F ) the initial F -algebra (term algebra over F ), and write hM : j (F )j ! j j for the unique homomorphism associated with . A context is a mapping defined with a sort-compatible term t with sort s0 that contains a variable x of some sort s. The context defines the map from s to s0 : m 7! x:t(m). We shall write f [ ] for a general context.
The equivalence relation is finite if it has a finite number of equivalence
classes. The class that includes an element is denoted [ ] when the intended
equivalence is clear from the context. A congruence on is an equivalence
relation on j j such that (i) any two elements equivalent under are of the
same sort and (ii) the relation is stable under the operations of , i.e., if
vi ui for i , then fM (v1; : : : ; v ) fM (u1; : : : ; u ). As a consequence,
is stable under the contexts of .
Let L ae j j. We denote by ?L the congruence on defined by: m ?L m0
if and only if, for every context f [ ], f [m] 2 L if and only if f [m0] 2 L. We say that L is generated by F if L ae hM (j (F )j), i.e., if every member of L can be
written as an expression over F . We say that L is -recognizable if L is a union of classes of a finite congruence on , all of the same sort.
roposition1 ourcelle . et be an F -algebra and L ae s for some s 2 . he following conditions are equivalent:
1 L is -recognizable.
2 ?L is finite.
3 L = h?1( ) where h is an F-homomorphism onto a finite algebra and
ae s.
Structure algebras are too general to be useful. In an S definable structure algebra, the value hM(t) of a term t is obtained by an MS interpretation of the term t represented as a tree. Even more useful is the concept if the objects of hM (t), t = fM (t1; : : : ; tn) are easily obtained from the objects of hM (ti), as in the following examples:
Example . The classical construction method of a two-terminal series parallel graphs can be described in this framework, in an algebra with the nullary operator creating an edge, and two binary operations for series and parallel composition. The domain consists of structures in G2 augmented with two object constants pointing to the two terminals. This was generalized to -terminal graphs by Wimer[33]. Also, the interpretation for co-graphs described above can be interpreted as a structure algebra in signature G1, whose operations are: an object constant v for a vertex, a unary operation Pc for edge complementation, and a binary operation for disjoint union.
1. ecogni abilit of S-de nable sets of binar trees
A linear time algorithm for satisfaction of a fixed formula OE by a tree follows immediately from:
eore 2 [3 ]. or every S definable set of binary trees, the congruence ? is finite.
ia transitivity of the interpretability relation, we get a linear time algorithm to decide membership in any MS-definable set of graphs of bounded treewidth, if the graph is given with its interpretation.
An interesting consequence of the finiteness of the congruence relation is that any family interpretable in the family of binary trees must have certain restrictions. Specifically, if a binary relation is interpreted, the number of di erent objects in a subtree of node n, seen from outside the subtree, is uniformly bounded by the number of congruence classes. If the relation is the Adj relation of a graph represented in signature G1, the restriction is that the graph family must have uniformly bounded clique-width. If the relation is the incidence relation of a graph represented in signature G2, the restriction is that the graph family must have uniformly bounded tree-width. This follows, e.g., from an analysis of the restrictions (functional dependence of tail and head vertex of edge) on the incidence relations.
1. o erset algebras and e uational sets
For an F -algebra , the powerset algebra ( ) is an algebra with domains 2Ms and for every operator f of F there is an operator f of ( ) such that
f (M)( 1; : : : ; ) = ffM (a1; : : : ; a ) j a1 2 1; : : : ; a 2 )g. As a special
case of this, nullary operators in evaluate to singleton sets in ( ). Moreover, the powerset algebra of has a union operator +s for every sort s.
A formal language grammar can be seen as a simple example of an equation system over a the powerset algebra over a structure algebra generating strings. This algebra has a binary concatenation operator and nullary operators for the letters of the alphabet. The non-terminals can be seen as set variables (for sets of strings) and the alternative productions for a non-terminal as a (usually recursive) definition of a set as a union of sets. This view easily extends to structure grammars in general[6]:
e nition 3. An equational set over a structure algebra is the least solution to a system of equations over ( ). Such a system consists of a number of structure set symbols, each with an associated sort of , and a number of set equations, one for each set symbol. The left side of the equation is the associated set symbol, the right side is a well-sorted expression over ( ). As the solution of such a system we shall mean the unique minimal solution, obtained by (infinite)iteration of the equations starting with the empty set for each set variable.
Example . Let the parallel and series composition operators of a ttsp graph construction be denoted as operators and ? of a structure algebra, and let e be the nullary operator evaluating to an edge. The set of ttsp graphs is the equational set defined by the system of a single equation:
= e + ( ) + ( ? )
The iteration mentioned in Definition 3 for the set starts with (0) = , (1) = feg ( (0) (0)) ( (0) ? (0)) = feg, (2) = fe; e e; e ? eg, : : :. ltimately, every expression over the algebra will become included in some (i). Thus, the set S above is the whole set of graphs generated by the structure algebra. The set of ttsp graphs consisting of two parallel edges with a path of length n on both sides, for any n, would be generated by the equation system:
= (e e) + (e ? ( ? e))
The latter set is not MS definable since it is not possible to do unbounded counting in MS logic, like saying that two paths have equal but unbounded length. owever, the 'syntax tree', or rather, the term evaluating to a member of the set, is MS definable as a structure:
roposition ourcelle . Every equational set is the image under S interpretation of an S definable set of trees.
Equational sets over the signatures G1 and G2 are important in relation to graph grammars. Essentially, hyperedge replacement systems can generate equational sets over G2 , and node label controlled replacement systems can generate the equational sets over G1.
orit
In this section we review algorithms for solving problems on binary trees defined in MS-logic. These algorithms also work on structures interpreted in binary trees in the following sense: The problems we define here are the computation of characteristics of a set of m-tuples of a tree defined by an MS formula over the signature of binary trees. If instead we ask for a characteristic of the set of m-tuples defined by a formula OE over a structure I defined by interpretation from a binary tree , then it is possible, simply by substitution of the interpretation formulas into the formula OE, to obtain an isomorphic set of m-tuples of defined by an MS formula OE0. A similar technique works for decision problems over families of structures obtained as the image by interpretation of an MS definable set of trees. Note that we are not investigating the 'parsing problem' here; that is the problem of finding, given an MS interpretation, the tree with a given image. This problem has been satisfactorily solved (linear time) for graphs represented in signature G2, by means of tree-decompositions, but in general the problem is not well understood.
2.1 S proble s and t eir solution
Let an MS-problem be the problem of deciding membership in a MS-definable class L of structures. The finiteness of ?L for every MS-definable class of structures of binary trees implies not only that MS problems are linear time a large number of MS-problems on graphs from Garey and ohnson[1 ]. The concept of an MS problem is useful also for other combinatorial objects than graphs. Consider a propositional formula P represented as in Section 1.1 in signature F = (u; P:(u); P^(u); Op1(u; u); Op2(u; u); Root() : u). An interpretation is a subset of its propositional variables (the ones that are true in the interpretation) and its standard extension to include all subformulas of P that are true in the interpretation. So an interpretation is any set satisfying:
Interp( ) = 8xyz Op1(x; y) ^ P:(x) ! (x 2 $ y 2 )
Op1(x; y) ^ Op2(x; z) ^ P^(x) !
(x 2 $ (y 2 ^ z 2 ))
alidity of a propositional logic formula can now easily be expressed as the property that every interpretation makes the formula true:
alid() = 8 Interp( ) ! Root 2
In most applications it will be necessary to know not only if a formula OE(x1; : : : ; xn) has a satisfying set of m-tuples, but also if there is such an set consistent with a partial assignment that includes some elements Ii and excludes other, i, from tuple i. Such problems are easily solved using standard dynamic programming techniques[5]. EMS-problems are defined in [5] as problems involving MS definable sets in structures. A closely related development was presented by Courcelle and Mosbah[15]. We also use some ideas of Bodlaender[ ]. Let a structure I and an MS-formula with m free variables X1; : : : ; Xm be given. This formula defines a set of m-tuples of subsets of I. The set is of exponential size in general, so we cannot hope to list it efficiently. There may still be a number of things we want to know about the set, without actually listing it: we may consider its size (particularly whether it is non-empty), its largest smallest members size, the sum of all members sizes, the lexicographically (given some ordering of the domain of I) first element, the first element after a given one. We may want to answer the same questions for a derived set of tuples, like the maximal members the members consistent with a partial assignment, or the set of members in closures under various substructure operations like a quotient structure of a given structure, or related structures corresponding to the graph concepts induced graph, partial graph or minor. These problems are solvable by either systematic transformations of the formulas involved[ , 1] or standard variations of the dynamic programming paradigm[5]. Most of these problem remain solv-
able if the problem has valuations (i), where i ranges over the variable indices and ranges over the elements of the corresponding domain. These weights give rise to a weighted problem, where each defined tuple ( 1; : : : ; m) has weight
i xi2 i (i)
xi . Analysis of well known computational problems on graphs lead
us to the observation in [5] that dozens of well known optimization problems
on graphs are largest tuple or weighted largest tuple problems. Counting sets of
solutions has its most important applications in probability problems, which can
be seen as weighted counting problems. In [5] we describe how network and systems
reliability problems can be handled by assigning probabilities to sets and
finding the relative weight of sets with a systems property such as disconnecting
a communication network. In [1] we describe the use of counting for Bayesian statistical
inference in expert systems. The technique is used in several commercial
systems, and, with a small variation, for possibilistic logic analyses[18, 26, 2 ].
The congruence relation for an MS formula with m free variables developed in
the proof of Theorem 2 can be seen as a transition function : ? ? m ! ,
where = f0; 1g. The set of states that correspond to the satisfying assignments
is called the accepting set . For a node n with subnodes n1 and n2 having states
s1 and s2 with respect to the current variable assignment, the class assigned to n
will be (s1; s2; c), where c is an m-bit string describing the memberships of node
n in the sets assigned to X1; : : : ; Xm, i.e., bit i of c is if n 2 Xi, otherwise it is
1. The assignment is satisfying if the root is assigned a class in . The function
is often the key to solving EMS problems involving the MS formula OE. Some
recent extensions of the methodology follow:
e icograp icall rst and le icograp ic successor. Assume we have an ordering f 1; 2; : : : ; g of the nodes of a binary tree, and an MS formula OE with one free variable X. The lexicographically first set of nodes satisfying OE is obtained by first building a maximal initial segment 1 = f 1; : : : ; lg that can be put in the 'out' set of a partial assignment (with non-empty solution set), then putting l+1 in the 'in' set I, building a maximal segment 2 = f l+2; : : : ; pg such that = 1 2 and I = f l+1g is a partial assignment consistent with OE, etc. This procedure forces us to solve partial assignment problems, each in time ( ). The lexicographically first set of nodes satisfying OE can thus be obtained in time quadratic in the size of the binary tree. The lexicographic successor of a set in an MS definable family is similarly computed in quadratic time. It is helpful to consider a set of elements represented as an -string over f0; 1g. A partial assignment likewise corresponds to an -string over f0; 1; ?g. The total number of lexicographic successors is easily obtained. For example, the number of lexicographic successors of (0011001100) in the set defined by ' is p(00110011 ? ?) + p(001101 ? ? ? ?) + p(00111 ? ? ? ??) + p(01 ? ? ? ? ? ? ? ?) + p(1 ? ? ? ? ? ? ? ??) ? p(0011001100), where p(s) is the number of sets satisfying ' and consistent with the partial assignment s. It is easy to compute p(s) using a combination of the techniques of the previous subsections. This problem is also studied, using di erent methods, in[15].
eig ted sets and linear si e ine ualities. Assume again that a set of sets of nodes is defined with an MS-formula OE. We want to assign weights on these sets and ask about the induced weights on some nodes given weights or weight bounds on other nodes. The induced weight of a node is of course the sum of weights of sets containing the node. We can generalize our problem to MS definable sets of tuples: Each m-tuple is assigned an m-component weight vector and the induced weight of a node becomes an m-vector. For each node we allow an equality or inequality to be specified for each of the components of its induced weight vector. We can also allow arbitrary linear inequalities and equalities involving the components of induced weight vectors of any number of nodes. We want to find out the possible values of one component of an induced weight vector or any linear combination of such components.
At first sight, this problem appears to call for a linear program containing the full incidence matrix between the tuples of sets defined by OE and the nodes of the tree, and a variable for each such tuple. The number of satisfying tuples can be exponential in the size of the tree, so the problem is not feasibly solvable in this way. owever, it is possible to introduce variables re ecting the structure of the tree automaton, giving a polynomial size linear program and thus, using armarkars linear programming algorithm, a polynomial time algorithm for a family of structures MS-interpretable into the set of binary trees. We introduce a family of indexed variables describing the ' ow' of weight through the binary tree:
xnc weight of tuples with membership vector c of node n
yne weight of tuples assigning state e to node n
zne1e2c weight of tuples assigning states e1 and e2 to sons of n
and membership vector c in n
Constraints on weights of nodes can now be added, as linear conditions on the xnc, to the following set of ow equations:
yne =
n(e1;e2;c)=e
zne1e2c , n non-leaf,
xnc =
n(e1;e2;c)=e
zne1e2c , n non-leaf,
yn1e =
e2c
znee2c , n1 right son of n,
yn2e =
e1c
zne1ec , n2 left son of n,
yre = , e 2
Example . In Nilssons probabilistic logic[22] it is possible to define a set of propositional logic formulas and to give bounds on probabilities of some of these. It is asked what the probability of some other formula can be. This is a problem of the above type where the set of tuple sets is the set of interpretations of the propositional formulas (cf the predicate Interp of Section 2.1).
tended partitioning, pac ing and co ering proble s The following family (approximately) was shown solvable by Borie[8]: Consider a number of members of an MS-definable set of node sets in a binary tree. For every node, a number of incidence conditions are given: the node participates in exactly, at most, or at least m of these sets, where m is a member of a finite set of integers. We may want to maximize or minimize the number of sets, or their total size. What we have here is a linear optimization problem that can be arranged as in the previous section. owever, it is an integer programming problem since we count sets. Normally, an integer programming problem is NP-complete and not known to be solvable in polynomial time. owever, in this problem one can get a polynomial time algorithm by careful analysis of the problem. First, note that the number of sets in an optimal solution is less than m , where m is the largest member of and is the number of nodes of the tree. If more than m sets can be packed, then the maximization problem has no solution (the number of sets is unbounded). If there is no solution with m or fewer members, then there is no feasible solution at all. Now, look at the system of the previous section, with m = 1. The sum of xn;c over c, of yne over e, and of zne1e2c over e1, e2 and c is less than m , since each of the sums, for each n, is equal to the number of sets. But each of those sums are taken over a constant number of variables, independent of the size of the tree (but it is of course dependent on
the formula and its number of free variables). Thus, the number of possibilities for each of the groups of variables is polynomial (a polynomial number of items can be distributed over a constant number of bags in a polynomial number of ways). Going from the leaves upwards we can find the sets of assignments of the variables ( xn;c, yne and zne1e2c) for each node that can be extended downwards in the tree and is consistent with all equations involving nodes of the subtree. Those solutions for the root with only accepting states are the real solutions. We can examine them and see which one involves the smallest number of sets. Alternatively, we can propagate the smallest (or largest) possible total sets size for each solution and find the largest or smallest total set size satisfying the partitioning packing covering conditions.
Example . Borie[8] mentions the following examples of graph problems solvable with this method, if the graph is represented in signature G2 where both vertices and edges are objects:
1. Cycle packing (maximizing the number of disjoint cycles in a graph),
2. generalized matching (maximizing the number of disjoint vertex sets such
that each set induces a given fixed graph ),
3. m-multichromatic number (minimizing the number of independent vertex
sets such that each vertex is in exactly m sets),
4. chromatic index (minimize the number of matchings into which the edge set
can be partitioned),
5. induced tree cover (minimize the number of vertex sets such that each set
induces a tree and each vertex is in at least one set).
Some of these problems might be solvable in linear time, because of special combinatorial theorems that do not fit into the general picture. As an example, hou, Nakano and Nishizeki[34] show how the chromatic index problem for graphs interpretable in binary trees can be solved efficiently (with small constants) in linear time.
artial e aluation and structures. The problems above involve a fixed tree into which a structure is interpreted. Instead of computing the tree automaton for MS formula OE by a recursion over the formula, it is often advantageous to compute a partial evaluation n of the transition function to a node n. Consider also these node transition functions as being represented by matrices, row indexed by left subnode state and column indexed by right subnode state. This has the advantage that state set minimization can be performed 'on the y' in the recursion over the formula structure. Thus, when n has been produced for node n and formula ' by combination of the transition tables for the subformulas of ' for the subnodes of n, a construction that goes bottom-up in the interpretation tree, it is possible to fuse states top-down in the tree by joining two states in the left subnode of n if the corresponding rows are equal, and joining states in the right subnode when the corresponding row of n are equal. The resulting data structure is a slight generalization of the
popular OBDD structure[ ]. Whereas the OBDD is a slight generalization of the minimal DFA accepting the satisfying assignments of a formula, represented as strings over f0; 1g, our structure accepts satisfying assignments represented as trees labeled by f0; 1gm. The relations between these views were explained in [11, 21]. One can note that if the size of the tree is n and the range of n is bounded by (uniformly over n), then the size of the OBDD is (in the worst case) (n log n ).
On closer examination we find that it is not necessary to find an explicit interpretation on an MS problem on a structure in order to compute the tree automaton. There is a straightforward way to translate a problem involving second order logic formula OE and a given set of domains into a problem of propositional logic. An individual (first-order) variable is translated to a set of one boolean variable for each element of its domain, and a second-order relation variable is translated to one boolean variable for each domain tuple that it could contain (given the profile of the variable). Set operators have an obvious translation to disjunctions and quantification over a relation variable is translated to a quantification over the corresponding set of boolean variables. If there is no universal quantifier in OE, the second order logic problem will be translated to a satisfiability problem, and one of the many practical satisfyability checkers can be applied (although it is true that this problem is infeasible in the worst case). Otherwise, we get a quantified boolean formula. We can compute its OBDD or tree representation by guessing either an ordering of its variables, or a tree labelled with its variables. If our guess corresponds to a path or tree into which the problems relational structure can be efficiently interpreted (i.e., with formulas that compile to transition functions over small state sets), then we can also solve related EMS problems. The theory of tree- and path decompositions tell us that if our guess corresponds to a decomposition of small width, then the transition tables will be small. But the opposite is not necessarily true, since there are other possible reasons for the state space to collapse, such as symmetries in the represented functions [10].
The outlined method is applicable to model-checking full second order logic, since a finite propositional formula obtained from the structure will generate finite node state sets. In general, this method will yield exponentially large state sets (in the size of the structure). owever, there are problems like validity in intuitionistic and modal logics which are easily expressed in full second order logic (on a structure representing the formula) and where where there are indirect proofs of recognizability for bounded treewidth[1]. For such problem families this method will be polynomial.
o ro rti o d n t o tructur .
In this section we will investigate various ways of defining structures using MS definitions and interpretations. We will relate our methods to the area of graph grammars. The problems investigated will be decision problems, i.e., we want to know if every or some member of an infinite family has a certain property.
The problems we study were investigated by Wanke[31], in the context of graph grammars.
By a semilinear set we mean the union of a finite number of linear sets.
A linear set is the set of -vectors o + cibi where i ranges over a finite
set, the ci range over the set of natural numbers ; 1; : : :, and o and bi are -
vectors called the basis of the set. For an e ectively presented semilinear set we
have the participating linear sets given with their basis systems. It is clear by
application of linear integer programming that both emptiness and finiteness of
the intersection of an e ectively presented semilinear set and a polytope can be
decided.
For a binary tree , an MS formula OE with p congruence classes and a satisfying assignment V of sets of nodes of to the m free variables of OE, we define the ari h map ( ; V ) as a vector in p2m such that a component corresponds to a pair of a class and membership vector c 2 f0; 1gm and is the number of nodes in assigned congruence class and with membership vector c. Let ( ) be the union of ( ; V ) over all assignments V giving an accepting state to the root of . Define to be the union of ( ) over a set f j j= 'g.
eore an e . or every S-definable family F of binary trees defined by formula ', and S definable family of tuples defined by formula OE, is a semi-linear set.
roof. The following proof is adapted from Parikh[23]. Assume that the formula
OE has congruence classes , the formula ' has classes and m free variables.
Let = ? ? f0; 1gm and consider the family of trees labeled as
defined by the transition functions of OE and ': For a node n of label (s ; s ; c)
with subnode states (s 1; s 1; c1) and (s 2; s 2; c2) we have s = (s 1; s 2)
and s = (s 1; s 2; c). The empty tree is considered labeled with (s ; s ; 0).
Clearly, is the Parikh map of the subset of these trees whose root is labeled
with two accepting states. We will prove that the set of such trees having label
set exactly ae has a semilinear set as its Parikh map. The theorem follows
from this since a finite union (over the subsets of ) of semilinear sets is itself
semilinear. So consider , the set of such trees containing exactly label set and with no unnecessary label repetition along a root-leaf path. An unnecessary
label repetition is one where contraction of the path between the repeated labels
does not change the label set of the tree. There are finitely many such trees.
Also, for every 2 , form the finite set oe of -labeled trees with root and
one leaf labeled , and with no other label repetition along a top-down path.
The Parikh map of the accepted trees with label set exactly is obviously the
union over b 2 of a linear set whose o set vector is (b) and whose basis set
is f (t) j 2 ; t 2 oe g
Example . Wanke gives the following example of an application where this technique is useful: A LSI cell generator can sometimes be described as the interpretation image of an MS definable tree family. One correctness condition is that signal path lengths between two given vertices must not straddle a signal
path length between two other vertices . This condition is a problem of the kind above: If Path(f; P; t) is a MS formula saying that P is a path from f to t, the condition says that there is no graph in the family satisfying
Path(f1; P1; t1) ^ Path(f2; P2; t2) ^ Path(f1; P 1; t1)
and with jP1j jP2j jP 1j. Since (jP1j; jP2j; jP 1j) over the satisfying tuples
over the family of graphs is a linear map of a semi-linear set, the condition is
decidable with integer linear programming.
onc u ion.
Discrete optimization and decision methods based on efficient handling of large state spaces used to be delicate and error-prone. With the emergence of efficient tools based on BDD-related technology and comprehensible logical definition methods[3, 20], applications will multiply. Among interesting application possibilities, besides those already mentioned, are image and geometry codings[2 ] as used e.g., in geographic information systems, and intelligent systems.
r nc
1. S. A NB , raph decompositions and tree automata in reasoning with uncertainty,
o o o
-
. S. A NB , Decomposability helps for logics of knowledge and belief.
o o o {
. S. A NB , A general purpose S model checker and optimi er based on
Boolean function representations. presented at the ifth nternational Workshop
on raph rammars and Their Application to omputer Science, Williamsburg,
Nov 1 4. htt .nada.kth.se ~ stefan
4. S. A NB , B. A. SK WSK AND D. S S , An Algebraic
Theory of raph eduction, o . - .
. S. A NB , . A N AND D. S S , asy roblems for Treedecomposable
graphs . o o - .
. . BA D NAND B. , raph e pressions and graph rewritings,
o 1 , -1
. H. . B D A ND , mproved self-reduction algorithms for graphs with bounded
treewidth. - .
. . B. B , eneration of polynomial time algorithms for some optimi ation
problems on tree-decomposable graphs.
. . B ANT, raph Based Algorithms for Boolean unction anipulation
. o - - .
10. . B ANT, Symbolic Boolean anipulation with rdered Bolean-Decision Diagrams.
o - .
11. . . B H, . . A K , K. . c AN, D. . D AND . . HWAN ,
Symbolic odel hecking 10 states and beyond o o o o
- .
1 . D. . N , H. HS AND . ST WA T B N HA , omplement
educible raphs, . . - .
1 . B. , The monadic second order logic of graphs ecogni able sets
of finite graphs, o o o o 1 arch 1 0, 1 -
14. B. , onadic second order definable graph transductions a survey,
o o 1 4 , -
1 . B. AND . SBAH, onadic second order evaluations on treedecomposable
graphs, o o 1 , 4 -
1 . - .
1 . . . D N , Decidability of the Weak Second- rder theory of two Successors,
- o . . o . .
1 . D. D B S AND H. AD nference in possibilistic hypergraphs. o . .
o . o o o o o
.
1 . . . A AND D.S. HNS N, omputers and ntractability, . .
o o .
0. . . H N KS N, . . . NS N, . . NS N, N. K A ND, .
A , T. A H AND A.B. SANDH , NA onadic Second- rder
ogic in ractice. o - -
1. K. . c AN, Hierarchical representations of discrete functions, with applications
to model checking o o o o -
o 1 4 41- 4,
. N. N SS N, robabilistic logic, 1 1- ,
. . A KH, n conte t-free languages, 1 0- 1,
4. . A , robabilistic reasoning in intelligent systems Networks of plausible
inference. o . o
. . . AB N, Decidable theories, oo o o . . .
o - o o - .
. . SH N , A valuation-based language for e pert systems. . o o -
o o 1 -411.
. . SH N , . SHA , A ioms for probability and belief function propagation,
in .D. Shachter, T.S. evitt, .N. Kanal,
. . emmer, ds. lsevier Science ublishers B. . 1 0.
. . . SH N D, athematical ogic, o - .
. . STA K AND . B ANT, sing rdered Binary-Decision Diagrams for
ompressing mages and mage Se uences , o - -
-
0. .W.THAT H , .B.W HT, enerali ed inite Automata Theory with an
Application to a Decision roblem in Second{ rder ogic,
o - .
1. . WANK n the decidability of certain integer subgraph problems on conte tfree
graph languages, o o o o -
. . WANK -N graphs and polynomial algorithms -
- .
. T. . W , inear algorithms on -terminal graphs, hD. Thesis, lemson
niversity 1 .
4. . H , S. NAKAN AND T. N SH K , A inear Algorithm for edgecoloring
partial k-trees, - .
This article was processed using the T macro package with N S style