DESIGN AND IMPLEMENTATION OF MULTIPLE-CONTEXTTRUTH MAINTENANCE SYSTEM WITH BINARY DECISION DIAGRAM

Hiroshi G. Okuno,

Osamu Shimokuni, and Hidehiko Tanaka

NTT Basic Research Laboratories

Graduate School of Engineering

Nippon Telegraph and Telephone Corporation

The University of Tokyo

3{1 Morinosato-Wakamiya, Atsugi

7{3{1 Hongo, Bunkyo-ku

Kanagawa 243-01, JAPANTokyo 113, JAPANokuno@nuesun.brl.ntt.jp, osamus@ipl.t.u-tokyo.ac.jp, and tanaka@mtl.t.u-tokyo.ac.jp

ABSTRACTImplicit enumeration of prime implicates in Truth
Maintenance System (TMS) is investigated. CMS(Clause Management System), an extension ofAssumption-based TMS (ATMS), that accepts any
type of justi cation has a burden to compute allprime implicates, since its complexity is NP-complete.
To improve the performance of multiple-context TMS
such compact representation of boolean functions. In
this paper, we propose a BDD-based Multiple-context
TMS (BMTMS) and present the design and implementation of interface between TMS and BDD. Theinterface provides high level speci cations of logicalformulas, and has mechanisms to schedule BDD commands to avoid combinatorial explosions in constructing BDDs. In BMTMS, most TMS operations are carried out without enumerating all prime implicates.

1 INTRODUCTION
The capability of thinking with explicit multiple alternatives is required by sophisticated problem solving systems such as qualitative simulation, multi-fault
diagnosis or non-monotonic reasoning. Since a consistent database (data collection) is referred to as context,
the above requirement can be paraphrased as multiple
context reasoning. Multiple-context reasoning is, ingeneral, superior to single-context reasoning in switching contexts or comparing the results between context[deK86a].
A problem solving system consists of an inferenceengine and a truth maintenance system (TMS). The
inference engine introduces hypotheses and makes inferences, while TMS records hypotheses as assumptions and inferences as justi cations. TMS maintains
the inference process and enables the inference engine
to avoid futile or redundant computations [FdK93].

TMSs are classi ed according to two properties. One
property is whether they provide a single or a multiple context and the other is whether they accept Hornclauses or general clauses as justi cations. This classi cation is summarized in Table 1.
Justi cation-based TMS (JTMS) is a single-context
TMS that accepts only a Horn clauses as a justi cation. JTMS is very popular so far, because JTMS runs
very eciently with backtracking mechanism. The satis ability of a set of Horn clauses, or the assignment ofvariables that satis es the set of clauses, can be solvedin a linear time of the number of variables [Dow84].
However, JTMS cannot perform eciently reasoning
with alternatives.
Logic-based TMS (LTMS) is a single-context TMS
that accepts general clauses including disjunction or
negation. An ecient algorithm for LTMS is a Boolean
constraint Propagation (BCP), a kind of intelligent
backtracking mechanism. First, the conjunction of justi cations is converted to a conjunctive normal form
(CNF, or Product of Sum, POS) and decomposed toa set of clausal forms. BCP takes a set of clausal
forms and labels each node consistently by backtracking. BCP with a set of clausal forms is complete forHorn clauses, but not for general clauses. This incompleteness is caused by being information dropped inconversion of a clause to a set of clausal forms. To
Table 1 Classi cation of TMS
context

singlemultiplejustification

context

context

Horn

Justi cation-based
TMS (JTMS)
Logic-based
TMS (LTMS)

Assumption-based
TMS (ATMS)
Clause Management
System (CMS)

clauses
generalclausesDESIGN AND IMPLEMENTATION OF BMTMS
recover completeness, all prime implicates should be
added to the set of clausal forms, but the whole performance of such a BCP deteriorates because the total
number of prime implicates is generally very large. For
example, the modeling of two containers connected bya valve with seven observation points produces 2,814
prime implicates [FdK93]. In addition, the computational complexity of enumerating prime implicates is
NP-complete.
A multiple-context TMS is, in general, superior
to a single-context TMS in its capabilities and eciency in seeking all solutions [deK86a]. In particular,
Assumption-based TMS (ATMS), a multiple-context
TMS that accepts only Horn clauses as justi cations
can be implemented quite eciently by compiling justi cations into a network [deK86a; Oku90]. A datumof inference engine is represented by a node and its
belief status is maintained by a label. The labels arecomputed incrementally by using the network. However, ATMS has a limited power of expression. Whenthe problem solving system wants to handle a generalclause, it must be encoded to a set of Horn clauses
with special constructs. And some additional routines
are needed to validate the completeness of TMS operations [deK86b]. This type of encoding sometimes
gives rise to the degradation of the total performanceof the system.
Clause management system (CMS) is a multiplecontext TMS that accepts general clauses including
disjunction and negation [RdK87]. In CMS, the labelof a node is computed via minimal support [RdK87].
Let 6 be the set of all the justi cations and P I be aprime implicates of 6. The minimal support for theclause C is computed as follows:
M inSup(C; 6) = fS jS 2 1(C; 6); S is minimalg(1)1(C; 6) = fP I 0 C jP I [ C 6= fgg
Note that the computation of the minimal support requires the enumeration of all prime implicates. This is
the main factor of intrinsic poor performance of CMS.
We have been studying an implicit enumeration ofprime implicates. Recently, a Binary Decision Diagram (BDD) is proposed, which is a compact representation and provides ecient manipulations of booleanfunctions [Bry92]. Recent techniques with BDDs cangenerate more than 1010 prime implicates [LCM92].
Since BDDs can represent all solutions simultaneously,
it is reasonable to use BDDs to implement a multiplecontext TMS. In this paper, we propose a BDD-based
Multiple-context TMS (BMTMS) to exploit two ways:
1) Implementing ecient methods for enumerating
all prime implicates, and
2) Implementing TMS operations without enumerating prime implicates explicitly.

x2
C12 {b c, b d, b e}D2{c, d, e}

x1
C23

D1

{d f, e g}{a, b}x3
D3
C13 {b f, b g}

{f, g}FIGURE 1 A simple constraint satisfaction problem

Madre et al. implemented ATMS by a variant of BDD
called TDG (Typed Decision Graphs), but only the
rst issue was addressed [MC91].
The rest of the paper is organized as follows: In Section 2, the issues of CMS are identi ed. In Section 3,
BDDs are explained and the issues in applying BDDs
to multiple-context TMS is investigated. In Section 4,
the BMTMS is proposed and its details are described.
In Section 5, some capabilities of the BMTMS are
demonstrated. The evaluation results of the BMTMS,
and conclusions are given in Section 6 and Section 7,
respectively.

2 IDENTIFYING THE ISSUES OF CMS
In this section, the drawbacks of the ATMS and the
problems of CMS are demonstrated by using a a simple
problem [deK89] (hereafter, the simple problem) shownin Figure 1. It has three variables, x1 , x2 , and x3 . The
domain of each variable is D1 = fa; bg, D2 = fc; d; eg,
and D3 = ff; gg, respectively. For a pair of variables,x and x , a constraint on them, C, is given as the setof permissible combinations of values. They are C12 =fb c; b d; b eg, C13 = fb f ; b gg, and C23 = fd f ; e gg.
i

j

i;j

2.1 Encoding by ATMSIn ATMS, an inference-engine's datum is represented by a TMS-node, and an assumption is a special kind of TMS-node. A justi cation has a set ofantecedents and a single consequence, all of which are
TMS-nodes. In other words, a justi cation is a propositional Horn clause. An environment is represented
by a set of assumptions. A contradictory environmentis called nogood. Each TMS-node has a label, or a set ofenvironments, under which the node is proved valid.
The simple problem cannot encoded by ATMS itself,
because it contains disjunctions and thus is not a Hornclause. The encoding techniques proposed by de Kleer[deK89] is used for the encoding. The inference engine
gives the following data to ATMS:DESIGN AND IMPLEMENTATION OF BMTMS

 A propositional symbol,

x : .
A symbol x :means that a variable x has a value v. Thus,
x1: , x1: , x2: , x2: , x2: , x3: , x3: .
 A set of justi cations, each of which encodes thedomain of a variable.
x1: _ x1: , x2: _ x2: _ x2: , x3: _ x3: .
Since these clauses are not Horn ones, a disjunction is encoded by using the choose predicate as
follows:
i v

i v

i

a

b

c

a

b

c

d

e

d

f

e

g

f

g

choosefx1:a ; x1:b g, choosefx2:c ; x2:d ; x2:e g,choosefx3:f ; x3:g g.

 A set of justi cations, each of which states thateach variable have only one value.

: 1: _ : 1: , : 2: _ : 2: , : 2: _ : 2: ,: 2: _ : 2: , : 3: _ : 3: .
x

a

x

b

x

c

x

d

x

e

x

f

x

d

x

x

c

x

e

g

These are encoded by using the nogood predicate
as follows:
nogoodfx1:a ; x1:b g, nogoodfx2:c ; x2:d g,nogoodfx2:c ; x2:e g, nogoodfx2:d ; x2:e g,nogoodfx3:e ; x3:f g.

 A set of justi cations, each of which encodes aninhibited pair speci ed by a constraint.
:x1: _ :x2: , :x1: _ :x2: , :x1: _ :x3: ,:x2: _ :x3: , 1 1 1.
These are encoded as follows:
a

c

d

g

a

d

a

e

nogoodfx1:a ; x2:c g, nogoodfx1:a ; x2:d g,nogoodfx1:c ; x3:e g, nogoodfx2:d ; x3:g g, 1 1 1 .

To nd solutions that satisfy these justi cations,
ATMS uses a label update algorithm. Since ATMS
is complete for Horn clauses but not for arbitrary logical formula, ATMS fails to calculate the correct labels for the above encodings. To attain completeness,meta rules concerning choose and nogood are needed.
These meta rules perform hyperresolutions for thesepredicates. Some examples of hyperresolutions arelisted below:
choosefx3:f ; x3:g g
nogoodfx2:c ; x3:f g
nogoodfx2:c ; x3:g g

nogoodfx2:c g

b

c

d

f

g

e

a

b

c

a

d

d

f

d

e

e

g

f

g

b

c

b

d

b

f

b

g

d

f

e

g

g

d

d

e

c

d

f

b

e

c

x

x1:b

The nal solutions are(x1: ^ x2: ^ x3: ) _ (x1: ^ x2: ^ x3: ):
f

a

g

e

d

b

f

d

f

d

e

d

b

e

g

a

c

d

f

b

d

f

a

e

c

g

f 1: ^ 2: ^ 3: ^ : 1: ^ : 2: ^ : 3: ^ : 3:
^ 2: ^ 3: ^ : 1: ^ : 2: ^ : 2: ^ : 3: g.

choosefx2:d ; x2:e gd

2.2 Encoding by CMS
The simple problem is directly encoded by logicalexpressions. In CMS encoding, the same propositional
symbols as ATMS are used. The domain of each variable is encoded as X 1, X 2, and X 3. The select-one
type constraint that each variable has only one value is
encoded by C 1, C 2, and C 3. The constraints between
two variables are directly encoded.
X1= x1: _ x1:
X2= x2: _ x2: _ x2:
X3= x3: _ x3:
C1= (x1: ^ :x1: ) _ (:x1: ^ x1: )C2= (x2: ^ :x2: ^ :x2: ) _ (:x2: ^ x2: ^ :x2: )_(:x2: ^ :x2: ^ x2: )C3= (x3: ^ :x3: ) _ (:x3: ^ x3: )C 12= (x1: ^ x2: ) _ (x1: ^ x2: ) _ (x1: ^ x2: )C 13= (x1: ^ x3: ) _ (x1: ^ x3: )C 23= (x2: ^ x3: ) _ (x2: ^ x3: )F= X1 ^ X2 ^ X3 ^ C1 ^ C2 ^ C3
^C 12 ^ C 13 ^ C 23
(2)
The simple problem is encoded as F . The prime implicates of F are:x2: _ :x3: , x2: _ x3: , :x3: _ x2: ,x3: _ :x2: , :x2: _ :x2: , x3: _ x2: ,:x2: _ :x2: , ...
Let Goal be the goal literal. The simple problem
is thus encoded as F  Goal. The label of the Goal
literal is computed by Equation (1) and the following
results are obtained:(x1: ^x2: ^x3: ^:x1: ^:x2: ^:x3: ^:x3: )  Goal
(x1: ^x2: ^x3: ^:x1: ^:x2: ^:x2: ^:x3: )  Goal
Thus, the solution is obtained as the label of the literal
Goal , that is,choosefx2:c ; x2:d ; x2:e gnogoodfx2:c gbThis encoding works well for the simple problem, butdoes not work for all CSPs. de Kleer pointed outthat the meta rules correspond to local consistency
algorithms [deK89]. Applying a meta rule that corresponds to arc-consistency algorithm is very expensive,
and thus the completeness may be ful lled not at all
time.

b

e

g

b

x

x

e

d

x

x

g

f

x

x

a

a

x

x

c

e

x

x

d

c

x

x

f;

g

Since the labels in ATMS satis es four properties |soundness, completeness, consistency, and minimality|, they can be computed incrementally and ecientlyDESIGN AND IMPLEMENTATION OF BMTMS

x1 ^ x3 , (x1 ^ :x2 ) _ x3 , :x2 _ x3

(x1 ^ :x2 ) _ x3
x1

x1
1

0

x3

1

0

1

1

x1 1
0

o

x2

x2

o

x3

o

o

x3

0
0

o

x3

x3
x3

x1

o1

0

x2

x2

x2
x3

x1

1

0

1

0

1

0

0

(b) Negated edges(c) SBDD

1

FIGURE 2 Tree representation[deK86a]. On the other hand, the labels are computedin batch in CMS by enumerating all prime implicates,
because no algorithms are proposed so far to get allprime implicates incrementally. The label of a nodeplays a key role for ecient processing in ATMS, while
it is one source of ineciency in CMS. To cope with
CMS's ineciency due to enumeration of prime implicates, we exploit BDDs in the following two ways in
the next section.
1) TMS operations without using labels, and2) ecient enumeration of prime implicates.

3 Binary Decision Diagram (BDD)
3.1 Representing logical functions
Akers proposed a Binary Decision Diagram (BDD)[Ake78] as a compact representation of boolean (logical) functions, and Bryant invented ecient algorithms for manipulating them [Bry86]. Boolean functions can be represented by a tree. For example, thelogical function, ((x1 ^ :x2 ) _ x3 ), is represented by atree, where a node represents a variable and two kindsof leaves represent 0 and 1 (Figure 2). Two edges ofeach node are called 0-edge and 1-edge, which represent the value when the variable associated with thenode takes 0 and 1, respectively.
By xing the order of variables, say, x1 ; x2 ; x3
(where x1 is the uppermost variable), sharing leaves
and duplicate nodes, and removing redundant nodes,
this tree can be transformed into an ROBDD (Reduced
Ordered BDD) (Figure 3-(a)). An ROBDD gives acanonical form of a boolean function, and thus equivalent functions are represented by the same ROBDD.
Various techniques have been invented to reduce thesize of BDDs. One is a negated edge, which is indicatedas a small circle attached to an edge (Figure 3-(b)).
Another example is a Shared BDD (SBDD), whichshares BDDs among many functions. Three functions(a) ROBDDFIGURE 3 ROBDD and its variants

share BDDs (Figure 3-(c)). Hereafter, BDD refers to
SBDD with negated edges.
A BDD is constructed incrementally by the apply function instead of reducing a tree representation. Suppose var-order returns the order of a variable. Then, the apply function is de ned recursively
as follows:
apply (bdd1,bdd2,operation) =8  if var-order (bdd1's root) = var-order (bdd2's>>>> root), create a node by performing the opera>> tion to get a 0-edge and 1-edge.
>>  if var-order (bdd1's root) > var-order (bdd2's< root), create a node with apply (bdd1's 0-edge,>> bdd2, operation) for the 0-edge, and>> apply (bdd1's 1-edge, bdd2, operation) for the>> 1-edge.
>>  otherwise,: apply (bdd2, bdd1, operation).
This de nition can be explained as performing logical operations on the Shannon expansion. Supposethat the Shannon expansions of functions f and g are
as follows:f = (:x ^ f x=0 ) _ (x ^ f x=1 ), andg = (:x ^ g x=0 ) _ (x ^ g x=1 ).
The logical AND of f and g, f ^ g, is computed as(:x ^ (f x=0 ^ g x=0 )) _ (x ^ (f x=1 ^ g x=1 )).
The computational cost of the logical AND is in theorder of the product of the numbers of nodes of both
BDDs. Most functions can be executed in the sameorder. In addition, the apply function can be implemented eciently by using a node hash table and a
result cache (hash table). Since the result cache stores
recent results of apply functions, redundant computations may be avoided if the cache hits. Since BDD is acompact representation of boolean functions and many
usual boolean operations are performed eciently with
BDDs, BDD is commonly used in VLSI CAD systems.
j

j

j

j

j

j

j

j

DESIGN AND IMPLEMENTATION OF BMTMS
Table 2 Comparison of size of BDDs
(2)
Best

(3) 3
Best 3

101

31

24

30

BDD
BDD-based Multiple-context TMSCInference
EngineBinterface

Constraint ordering
Variable ordering
Maximum size of intermediate BDDs
Size of nal BDD

Problem Solving System

Both constraint and variable ordering are determined by
the CCVO heuristics.

The simple problem of the previous section can besolved directly by creating the BDD for F by using
Equation (2). However, this BDD is an implicit representation of solutions and all the paths from the rootof the BDD to the leaf of 1 should be enumerated to
get the explicit representations of solutions.

3.2 Issues in using BDD
Applying BDDs to TMS has four main issues:
1) Variable ordering2) Constraint ordering
3) Encoding by logical functions4) Compatibility with existing systems
The number of nodes of a BDD, or the size of BDD,
is determined by variable order. The minimum (best)
size of 2-level AND-OR circuit of n variables is in thelinear order of n, while the worst size is in the order of
2 . Therefore the optimal variable order under which
the size of BDD is minimum is very important. However, the computational complexity of nding the optimal variable order is NP-complete. This is well-known
problem and many heuristics to nd a near-optimalvariable ordering is proposed.
However, constraint order is essential to avoid combinatorial explosions [Oku94]. In creating the BDD for
F , nine constraints, X 1, ..., C 23, are used. Consider
two constraint orderings below:
X 1 ^ X 2 ^ X 3 ^ C 1 ^ C 2 ^ C 3 ^ C 12 ^ C 13 ^ C 23
(2)
X 1 ^ C 1 ^ X 2 ^ C 2 ^ C 12 ^ X 3 ^ C 3 ^ C 13 ^ C 23
(3)
The size of BDDs created by (2) and (3) is shown in
Table 2. The size of intermediate BDDs is a ectedby constraint order. The importance of constraint
ordering is discovered by applying BDDs to solve
combinatorial problems. Okuno proposed the CCVO
(Correlation-based Constraint and Variable Ordering)heuristics to nd a near-optimal constraint ordering.
The CCVO rst calculates the correlation of variables
between constraints and then determines constraint
ordering. Variable ordering is determined the rst
time a variable is used by constraint ordering.
n

SBDD
graph

ATMS/CMSdata

TMS node

hypothesis

assumption

inferencejustification

contradiction

nogood3

in Common LispA

BDD
in C, BEM, ...

SBDD
graph

FIGURE 4 Structure of BMTMS

Another problem of constraint ordering occurs inapplying BDDs to TMS, because constraints or justi cations are given incrementally. Therefore, a new
method of determining constraint ordering is required.
The third issue is concerning the expressive powerof logical functions. In this paper, arithmetic booleanfunctions are used [Min93a]. A select-one type constraint can be easily encoded by them. For example, aconstraint that variable x2 has one and only one valueof its domain, that is X 2 ^ C 2, can be encoded by
x2: + x2: + x2: == 0(4)
The nal issue is that the interface between BDD
and TMS should be compatible with existing systems,
since many applications are developed and it costs very
expensive to re-implement them from scratch.
cde

4 Design of BMTMS
In this section, the BDD-based Multiple-context
TMS (BMTMS), is proposed to cope with the above

issues. The whole system is depicted in Figure 4.
BMTMS provides three interfaces to various kinds ofexisting systems:
1) interface to ATMS/CMS ( A in Figure 4),2) interface to extensions of ATMS such as consumer
architecture [deK86b] ( B in Figure 4), and
3) interface to inference engine ( C in Figure 4).
These interfaces are only conceptual and thus
treated uniformly within the BMTMS, since it can manipulate any logical formulas.

4.1 Interface functions
The criteria of designing the primitive functions
is whether they can be implemented eciently with
BDDs.
1) BDD primitive functions:bddand, bddor, bddnot, bddrstr0, bddrstr1, 1 1 1

DESIGN AND IMPLEMENTATION OF BMTMS
Each function corresponds to a primitive operation of BDDs, and take BDDs as its arguments.
For example, (bddrstr0 BDD x) computes a
BDD restricted to the case that x has value of 0,
that is, f x=0 .
2) Variable ordering:
variable-order speci es the variable order.
3) Logical operations:land, lor, lxor, imply, lnot, 1 1 1
These functions accept any number of arguments.
4) Arithmetic logical operations:l* (multiplication), l+ (addition), l/ (quotient),l% (remainder), l- (subtraction), l<< (left-shift)l== (equal to), ...
These operations are implemented by simulating
arithmetic logic unit (ALU) operations [Min93a].
Equation (4) is encoded by(l== (l+ x2: x2: x2: ) 0).
5) BDD graph operations:forall, exists, 1-path, 1 1 1
forall is universal quanti er and exists is existential quanti er. Consider a function, f , is expressed in Shannon expansion,f = (:x ^ fx=0 ) _ (x ^ f x=1 ):Universal quanti er 8xf is computed by
8xf = f x=0 ^ f x=1 :Or (bddand (bddrstr0 f x) (bddrstr1 f x)).
Existential quanti er 9xf is computed by
9xf = f x=0 _ f x=1 :Or (bddor (bddrstr0 f x) (bddrstr1 f x)).
1-path enumerates all the paths from the root ofa BDD to the leaf of 1.
6) Output functions:sop returns a sum of products, which is a set of
irredundant prime implicants. And pos returns
a product of sums, which is a set of irredundantprime implicates.
7) User de ned data types:
In addition to system-de ned binary and integer data, the user can de ne any data type bydefentity.
f

j

c

d

e

j

j

j

j

j

j

(defentity datatype(slot 1 slot 2 1 1 1 )(:exclusive-p) )A slot can be accessed by a function datatypeslotname. If :exclusive-p is speci ed, elementsof a data de ned by defentity hold exclusively.
An operation for a data type is de ned as follows:(defop (operation datatype)argument-list . body )Its name is datatype-operation.
8) Select function:(choice-of p1 1 1 1 p ) selects one element exclusively from the set. This function can be encodedby (lor p1 1 1 1 p ) and (l== (l+ p1 1 1 1 p ) 1).
9) Addition of Constraints(add-constraint l C) adds a constraint C to
the logical formula l. This is conceptually thesame as (setq C (land C l)).
nnn

4.2 TMS Data Representation
Four kinds of nodes in TMS are encoded as follows:
1) Premise: the variable itself.
2) Contradiction: This node is used to represent
a nogood relation in ATMS. It is not needed in
the BMTMS, since a nogood relation can be represented by a logical formula.
3) Assumption: An assumption variable is introduced to express environments in the BMTMS,
but is not discriminated from other nodes in
BDDs.
4) Normal node: a variable itself.
Constraints between nodes are represented straightforward as follows: Justi cation, n1 ; 1 1 1 ; n ! c, (c is an arbitraryclause), is encoded by(imply (land n1 1 1 1 n ) c).
 nogoodfn1 ,1 1 1,n g is encoded by(lnot (land n1 1 1 1 n )).
 classfn1 ; :::; n g, that selects one element from a
set of nodes is encoded as follows:(choice-of n1 1 1 1 n ).
k

k

k

k

k

k

4.3 TMS operations
Let 5 be a logical AND of all justi cations and d bea node. An environment E is expressed by an AND ofassumption variables, a1 ^ ::: ^ a . Implementations ofsome main TMS operations are listed below:
1) Check whether all justi cation are not consistent.
If the BDD for 5 reduces to 0, all justi cations
are not consistent.
2) Check whether node d is consistent withenvironment E : node-consistent-with(d, E )If the BDD for 5 ^ d ^ a1 ^ 1 1 1 ^ a reduces to 0,
node d is not consistent with environment E .
kk

DESIGN AND IMPLEMENTATION OF BMTMS
3) Computethetms-node-label(d).

Let

label

of

node

d

:

be assumption variables, andbe normal variables. The label of d iscomputed as follows:(1) Construct the BDD for 0 = (8d1 ; d2 ; :::(5 d)). (2) Enumerate all prime implicates of 0 that
contain d. This enumeration is described in Section 4.4. (3) Compute fX jX  d of a prime
implicateg, and this set is the label of d.
If the justi cations are restricted to Horn clauses(as in ATMS), the step (2) can be replaced withpos(0), which runs much faster.
4) Check the status of node d: in-node?,
out-node?, true-node?, false-node?
Let a1 ; a2 ; ::: be assumption variables, andd1 ; d2 ; ::: be normal variables. Construct the BDD
for (5  d). If the BDD reduces 1 or 0, thenode status of d is :TRUE and :FALSE, respectively.
Otherwise, construct the BDD for 8d1 ; d2 ; :::(5 d).
If the BDD is not 0, the node status of d
is :IN. Otherwise it is :OUT. (In addition, if thenode status of :d is :OUT, the node status of d is
:UNKNOWN.)
5) Force an assumption true or false.
These functions are implemented byretract-assumption(a or :a ), which are encoded as follows: (add-constraint a or :a 5).
a1 ; a2 ; :::d1 ; d2 ; :::

i

i

i

i

4.4 Prime implicatesIn the research of boolean and switching functions,a prime implicant which is in the form of product ofliterals is usually used. (A literal is either a symbol ora negated symbol). Ecient algorithms for obtaining
all prime implicants are proposed [CM92].
On the other hands, in truth maintenance, constraint satisfaction and logic programming, a prime
implicate which is in the form of sum of literals is usually used. Since a conjunctive normal form is dual to a
disjunctive normal form, a set of prime implicates canbe computed by performing the duality operation ona set of prime implicants.
In other words, given a logical function f (x), letf(x) be a function gotten by exchanging _ with ^ andvice versa, and by replacing every literal with its negation, simultaneously. Then all the prime implicates forf(x) are computed. Finally, exchanging ^ with _ andreplacing every literal with its negation simultaneously
computes every prime implicate.
The resulting set of prime implicates is enough forcomputing the label of a node, although it is not complete in the sense that any tautology such that (y _:y)is a prime implicate,

A

B

C

FIGURE 5 Two-pipe system ([FdK93, p.466])

In the BMTMS, all the prime implicates are computed directly from BDDs. The key point of the algorithm is that a BDD can be interpreted as anotherexpansion on f .
f = (x _ f x =0 ) ^ (:x _ f x =1 ),kk
The prime implicates of the function f can be obtained by combining the prime implicates of two subfunctions f xk =0 and f xk =1 . The algorithm recursively
computes prime implicates. This algorithm is a dual
version of Coudert's [CM92]. Intermediate sets aremaintained by Zero-Suppressed BDDs [CMF93], which
are well suited for the set representation [Min93b].
k

j

k

j

j

j

4.5 Label enumeration
In the BMTMS, it has been shown that all TMS
operations concerning labels except tms-node-label
can be implemented without enumerating prime implicates. Although such enumeration is needed at leastby abduction reasoning or dependency-directed search[RdK87], we guess that it is not so often in other applications. If this is true, many applications can be
implemented by BDDs very eciently.
4.6 Constraint and variable ordering
The constraint ordering algorithm used in the
BMTMS is simpler than CCVO. The BMTMS does
not construct a BDD for class constraints immediately
when they are given to the system. Instead, adding
those to the system is delayed until some variable ofthe class is used by some constraint. Variable ordering
is determined the rst time when it is used by such a
constraint similar to that of CCVO.
5 APPLICATIONS OF BMTMS
In this section, some capabilities of the BMTMS are
demonstrated in qualitative simulation.
Consider the system that has two pipes, A and C,
which are connected by a joint, B (Fig.5). The pressure and ow in the system can be modeled by thefollowing qualitative equations [deK91]:[dP ] 0 [dP ] = [dQ ];[dP ] 0 [dP ] = [dQ ];[dQ ] = [dQ ];
A

B

B

AB

C

AB

BC

BC

DESIGN AND IMPLEMENTATION OF BMTMS
where [dx] denotes the sign (+, 0, -) of .
First, the sign data type and its operations are dened as follows:dx
dt(defentity sign
(positive zero negative)(:exclusive-p t) )(defop (- sign) (s)(make-sign (sign-minus s)(sign-zero s) (sign-plus s) ))(defop (+ sign) (s1 s2)(let ((xp (sign-plus s1))(x0 (sign-zero s1))(xm (sign-minus s1))(yp (sign-plus s2))(y0 (sign-zero s2))(ym (sign-minus s2)) )(make-sign(bddnot(lor (bddand x0 ym) (bddand x0 y0)(bddand xm y0) (bddand xm ym)))(bddnot(lor (bddand xp yp) (bddand xp y0)(bddand x0 yp) (bddand x0 ym)(bddand xm y0) (bddand xm ym)))(bddnot(lor (bddand x0 yp) (bddand x0 y0)(bddand xp yp) (bddand xp y0))))))(defop (sign =0) (s) (sign-zero s))
Since the sign is de ned with :exclusive-p, the operation =0 is speci ed quite simply instead of the fol-lowing complicated de nition:(land (lnot (sign-plus s))(sign-zero s)(lnot (sign-minus s)) )The logical formula that express (x + y = 0) is dened as follows: (we use logical formula for economyof space.)(y ^ :y ^ :y0 ^ :x ^ x ^ :x0 ) _(:y ^ y ^ :y0 ^ x ^ :x ^ :x0 ) _(:y ^ :y ^ y0 ^ :x ^ :x ^ x0 )where indexes, p; 0; m, indicate three slots of the sign
data type, respectively.
Let C be a Lisp variable that holds the constraint
set. The above qualitative equations are encoded asfollows:
m

m

m

p

m

p

m

p

m

p

p

p

(setq Pa (make-sign) Pb (make-sign)
Pc (make-sign) Qab (make-sign)
Qbc (make-sign) )(add-constraint(sign-= (sign-- Pa Pb) Qab) C)(add-constraint(sign-= (sign-- Pb Pc) Qbc) C)(add-constraint(sign-= Qab Qbc) C)

Now, consider the situation that the pressure at A
is increasing and one at C is not changing. This fact
is encoded as follow:(setq Constraint(land Constraint(sign-plus Pa)(sign-zero Pc) ))(add-constraint Constraint C).

Finally, the result shows that the BDDs for(imply C (sign-plus Qab)), and(imply C (sign-plus Qbc))

reduce to 1. This means that both [dQ ] and [dQ ]are +, that is, the pressures at the interfaces between A
and B, and between B and C are increasing. Note that
this computation does not need enumerating prime implicates.
On the other hand, in QPE, every qualitative equation is expanded to a set of clausal form and all the prohibited combination are enumerated [deK91]. Then,
all the prime implicates are computed. The nal step isto apply the BCP to the set of all the prime implicates,
which computes the labels of [dQ ] and [dQ ].
AB

AB

BC

BC

6 EVALUATION OF BMTMS
The current BMTMS system is implemented in Lispand has two BDD packages (see Figure 4). One BDD
package is implemented in C, which is called Boolean
Expression Manipulator, BEM-II [Min93a]. This implementation of the BMTMS is referred to BMTMS
with BDD in C. Another BDD package is written in
Lisp and this implementation of the BMTMS is referred to BMTMS with BDD in Lisp. The timing data
is measured on the SPARCStation10 with 128 MBytesof main memory.

6.1 Evaluating interface A
N-Queens problem Two implementations of the
BMTMS are compared with the ATMS which is implemented in Lisp. Two kinds of N-Queen problem
programs by ATMS are used; one is by label update,
and the other is by interpretation construction. Bothprograms computes column by column. The timing
results of N-Queen problem programs are shown in
Figure 6. The BMTMS with BDD in Lisp is much

Time (sec)Madre and Coudert [IJCAI-91]



10.00






|| | | | | |









|

|| | | | | | |




1.00





 BMTMS with BDD in C
 BMTMS with BDD in Lisp
 Label Update with ATMS




























|

Interpretation Construction with ATMS
Madre and Coudert [IJCAI-91]



0.10





|

|| | | | | | |







|| | | | | |

|






|

|| | | | | | |






|

|




|| | | | | ||| | | | | | |



|



|

0.1

 BMTMS with BDD in C
 BMTMS with BDD in Lisp

|



|

1.0




|

|| | | | | | |

10.0





|

100.0

100.00|| | | | | ||| | | | | | |1000.0||

10000.0|| |Time (sec)

DESIGN AND IMPLEMENTATION OF BMTMS

|

|
4

|
5

|
6

|
7

|
8

|
9

|
10

|
|
|
11
12
13
Number of Queens

0.01 | |
1

|

|

0.0 |
3

|

|

|

|

|

|

|

|

|
10

|
|
|
|
|
|
| | |
100
Number of supporting environments

FIGURE 6 N-Queen problem results

FIGURE 7 Minimal Cover results

slower than the ATMS. The reasons are twofold. (1)The algorithm of N-Queens is di erent. If the mostfair algorithm by ATMS, which creates only one goal,
installs all the justi cations that justify the goal, andthen computes labels, is used, it runs much slower
than the BMTMS with BDD in Lisp and can get solutions only up to 6-Queen problem [Oku90]. (2) The
BDD is not considered suitable for Lisp due to Lisp's
memory management. Usually ecient implementations of BDD use only main memory, while such memory management is dicult in Lisp systems [Bry92;
MIY91]. The BMTMS with BDD in C shows a good
performance for large n.

6.3 Evaluating interface C : Qualitative
simulation
As described in the previous section, qualitative simulation of the two pipe system can be e ectively computed by the BMTMS without enumerating all theprime implicates. However, this is a preliminary resultand full assessment should be done by implementing
the full set of QPE by the BMTMS.

Minimal cover This benchmark was used by Madre
and Coudert [MC91]. The timing results of minimal
cover are shown in Figure 7. The gure shows that theoverheads of the BMTMS with BDD in Lisp exceed
those of the BMTMS with BDD in C. This is causedby the overheads of Lisp runtime system.
6.2 Evaluating interface B : ATMS trace leWe use an ATMS trace le generated by consumer
architecture [deK86b], for which de Kleer's ATMS
could not compute the labels. Both BMTMS implementations succeed in constructing BDDs by theconstraint ordering algorithm. However, they fail inconstructing BDDs due to combinatorial explosions,when the constraint and variable ordering mechanism
is not used. The ordering algorithm is very simple, but
proved e ective.

7 CONCLUSIONSIn this paper, a new multiple-context truth maintenance system called BMTMS is proposed and its design and implementation is presented. The key ideaof the BMTMS is to use BDDs to avoid enumerating
prime implicates in manipulating general clauses. The
two issues in applying BDDs to multiple-context TMSs
are pointed out; variable ordering, and constraint ordering. To cope with these issues, the BMTMS schedules the constraint ordering by considering the dependency of variables and justi cations (or constraints).
The BMTMS also provides three level interface to existing problem solving and TMS systems so that BDD
can be used in \plug-and-play" manner. Since the logical relations are stored in BDDs and most TMS operations can be performed without enumerating all prime
implicates, the BMTMS runs eciently. The BMTMS
enumerates all prime implicates directly from BDDs.
In addition, the capability of de ning a data type andits operations makes it easy to implement applications
with the BMTMS.
Future work includes implementation of the full
QPE system with the BMTMS to demonstrate it

DESIGN AND IMPLEMENTATION OF BMTMS
power and open a new load to intelligent systems.
Applying the BMTMS to various sophisticated expert
systems is also an interesting area.

Acknowledgments
The authors thank Mr. Yuji Kukimoto of UCB, Dr.
Shin'ichi Minato of NTT LSI Laboratories, and Mr.
Hideki Isozaki of NTT Basic Research Laboratories
for their discussions. The rst author also thanks Dr.
Ken'ichiro Ishii and Dr. Norihiro Hagita of NTT Basic
Research Laboratories for their supports.

References[Ake78] S.B., Akers. Binary Decision Diagrams. IEEE
Transactions on Computer, Vol. C-27, No. 6,
pages 509{516, 1978.
[Bry86] R.E. Bryant. Graph-based algorithm for
Boolean function manipulation. IEEE Transactions on Computer, Vol. C-35, No. 5, pages
677{691, 1986.
[Bry92] R.E. Bryant. Symbolic Boolean Manipulations with Ordered Binary Decision Diagrams. Computing Surveys, Vol. 24, No. 3,
pages 293{318, ACM, 1992.
[CM92] O. Coudert, and J.C. Madre. Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions. In Proceedings of the 29th Design Automation Conference (DAC), pages 36{39, ACM/IEEE, 1992.

[CMF93] O. Coudert, J.C. Madre, and H. Fraisse.
A New Viewpoint on Two-Level Logic Minimization. In Proceedings of the 30th Design
Automation Conference (DAC), pages 625{
630, ACM/IEEE, 1993.
[deK86a] J. de Kleer. An Assumption-based TMS. Arti cial Intelligence, 28:127-162, 1986.
[deK86b] J. de Kleer. Extending the ATMS. Arti cialIntelligence, 28:163-196, 1986.
[deK89] J. de Kleer. A Comparison of ATMS and CSP
Techniques. In Proceedings of the Eleventh Internatioal Joint Conference on Arti cial Intelligence (IJCAI), pages 290{296, 1989.

[deK91] J. de Kleer. Compiling Devices: Locality ina TMS. In Faltings, B. and Strauss, P. (eds):
Recent Advances in Qualitative Physics, MIT
Press, 1991.
[Dow84] W.F. Dowling and J.H. Gallier. Linear timealgorithms for testing the satis ability of

propositional horn formulas. Journal of Logic
Programming, vol.3, pages 267{284, 1984.
[FdK93] K. Forbus, and J. de Kleer. Building Problem
Solvers, MIT Press, 1993.
[LCM92] B. Lin, O. Coudert, and J.C. Madre. Symbolic prime generation for muliple-valued
functions. In Proceedings of the 29th Design
Automation Conference (DAC), paages 40{
44, ACM/IEEE, 1992.
[MC91] J.C. Madre, and O. Coudert. A logically complete reasoning maintenance system. In Proc.

of the Twelfth Internatioal Joint Conferenceon Arti cial Intelligence (IJCAI), pages 294{

299, 1991.
[MIY91] S. Minato, N. Ishiura, and Y. Yajima. Shared
Binary Decision Diagram with Attributed
Edges for Ecient Boolean Function Manipulation. In Proceedings of the 27th Design
Automation Conference (DAC), pages 52{57,IEEE/ACM, 1990.
[Min93a] S. Minato. BEM-II: An arithmetic Boolean
expression manipulator using BDDs. IEICE
Transactions of Fundamentals, Vol. E76-A,
No. 10, pages 1721{1729, 1993.
[Min93b] S. Minato. Zero-Suppressed BDDs for
Set Manipulation in Combinatorial Problems. In Proceedings of the 30th Design Automation Conference (DAC), pages 272{277,ACM/IEEE, 1993.
[Oku90] H.G. Okuno. AMI: A New Implementation of ATMS and its Parallel Processing (inJapanese ). Journal of Japanese Society for
Arti cial Intelligence, Vol.5, No.3, pages 333{
342, 1990.
[Oku94] H.G. Okuno. Reducing Combinatorial Explosions in Solving Search-Type Combinatorial
Problems with Binary Decision Diagrams (inJapanese ). Transactions of Information Processing Society of Japan Vol.35, No.5, pages
739{753, 1994.
[OST96] H.G. Okuno, O. Shimokuni, and H. Tanaka.
Binary Decision Diagram based MultipliContext Truth Maintenance System BMTMS(in Japanese ). Journal of Japanese Society
for Arti cial Intelligence, Vol.10, No.2, 1996.
[RdK87] R. Reiter, and J. de Kleer. Foundations ofAssumption-Based Truth Maintenance System. In Proceedings of National Conferenceon Arti cial Intelligence (AAAI), pages 183{
188, 1987.