Ordered binary decision diagrams as knowledge-bases.
We consider the use of ordered binary decision diagrams (OBDDs) as a means of realizing knowledge-bases, and show that, from the view point of space requirement, the OBDD-based representation is more efficient and suitable in some cases, compared with the traditional CNF-based and/or model-based representations. We then present polynomial time algorithms for the two problems of testing whether a given OBDD represents a unate Boolean function, and of testing whether it represents a Horn function.
Introduction
Logical formulae are one of the traditional means of representing knowledge in AI [11]. However,
it is known that deduction from a set of propositional clauses is co-NP-complete and abduction
is NP-complete [13]. Recently, an alternative way of representing knowledge, i.e., by a subset
of its models, which are called characteristic models, has been proposed (see e.g., [6, 7, 8, 9]).
Deduction from a knowledge-base in this model-based approach can be performed in linear time,
and abduction is also performed in polynomial time [6].
In this paper, we propose yet another method of knowledge representation, i.e., the use of
ordered binary decision diagrams (OBDDs) [1, 2, 12]. An OBDD is a directed acyclic graph
representing a Boolean function, and can be considered as a variant of decision trees. By
restricting the order of variable appearances and by sharing isomorphic subgraphs, OBDDs have
the following useful properties: 1) When a variable ordering is given, an OBDD has a reduced
canonical form for each Boolean function. 2) Many Boolean functions appearing in practice
can be compactly represented. 3) There are e-cient algorithms for many Boolean operations
on OBDDs. As a result of these properties, OBDDs are widely used for various applications,
especially in computer-aided design and verication of digital systems (see e.g., [4, 14]). The
manipulation of knowledge-bases by OBDDs (e.g. deduction and abduction) was rst discussed
by Madre and Coudert [10].
We rst compare the above three representations, i.e., formula-based, model-based, and
OBDD-based, on the basis of their sizes. In particular, we show that, in some cases, OBDDs
require exponentially smaller space than the other two representations, while there are also cases
in which each of the other two requires exponentially smaller space. In other words, these three
representations are mutually incomparable with respect to space requirement.
It is known that OBDDs are e-cient for knowledge-base operations such as deduction
and abduction [10]. We investigate two fundamental recognition problems of OBDDs, that is
testing whether a given OBDD represents a unate Boolean function, and testing whether it
represents a Horn function. We often encounter these recognition problems, since a knowledge-base
representing some real phenomenon is sometimes required to be unate or Horn, from the
hypothesis posed on the phenomenon and/or from the investigation of the mechanism causing
the phenomenon. For example, if the knowledge-base represents the data set of test results on
various physical measurements (e.g., body temperature, blood pressure, number of pulses and
so on), it is often the case that the diagnosis of a certain disease is monotonically depending
on each test result (we allow changing the polarities of variables if necessary). Also in articial
intelligence, it is common to consider Horn knowledge-bases as they can be processed e-ciently
in many respects (for example, deduction from a set of Horn clauses can be done in linear
time [5]). We show that these recognition problems for OBDDs can be solved in polynomial
time for both the unate and Horn cases.
The rest of this paper is organized as follows. The next section gives fundamental denitions
and concepts. We compare the three representations in Section 3, and consider the problems of
recognizing unate and Horn OBDDs in Sections 4 and 5, respectively.
Preliminaries
2.1 Notations and Fundamental Concepts
We consider a Boolean function f : f0; 1g n ! f0; 1g. An assignment is a vector a 2 f0; 1g n ,
whose i-th coordinate is denoted by a i . A model of f is a satisfying assignment a of f , i.e.
and the theory (f) representing f is the set of all models of f . Given a; b 2 f0; 1g n ,
we denote by a  b the usual bitwise (i.e., componentwise) ordering of assignments; a i  b i for
Given a subset E  f1; 2; . ; ng,  E denotes the characteristic
vector of E; the i-th coordinate  E
be the n variables of f , where each x i corresponds to the i-th coordinate
of assignments and evaluates to either 0 or 1. Negation of a variable x i is denoted by x i .
Variables and their negations are called literals. A clause is a disjunction of some literals, and a
conjunction of clauses is called a conjunctive normal form (CNF). We say that f is represented
by a CNF ', if holds for all a 2 f0; 1g n . Any Boolean function can be represented
by some CNF, which may not be unique.
We sometimes do not make a distinction among a function f , its theory (f ), and a
CNF ' that represents f , unless confusion arises. We dene a restriction of f by replacing
a variable x i by a constant a i 2 f0; 1g, and denote it by f
Restriction may be applied to many variables. We also
Lemma 2.1 The relation  has the following properties:
holds if and only if f j x i =a i  gj x i =a i holds for both a
holds if and only if f  h and g  h hold.
For an assignment p 2 f0; 1g n , we dene a  p b if (a  bit p)  (b  bit p) holds, where  bit
denotes the bitwise (i.e., componentwise) exclusive-or operation. A Boolean function f is unate
with polarity p if f(a)  f(b) holds for all assignments a and b such that a  p b. A theory  is
unate if  represents a unate function. A clause is unate with polarity p if positive
literals x i and negative literals x i in the clause. A CNF is unate with polarity p if
it contains only unate clauses with polarity p. It is known that a theory  is unate if and only
if  can be represented by some unate CNF. A unate function is positive (resp., negative) if its
polarity is (00
A theory  is Horn if  is closed under operation ^ bit , where a ^ bit b is bitwise AND of
models a and b. For example, if a = (0011) and (0001). The closure of
a theory  with respect to ^ bit , denoted by
(), is dened as the smallest set that contains
and is closed under ^ bit . We also use the operation ^ bit as a set operation; (f) ^ bit (g)
holds for some b 2 (f) and c 2 (g)g. We often denotes (f) ^ bit (g) by
convenience. Note that the two functions are dierent.
A Boolean function f is Horn if (f) is Horn; equivalently if f holds (as sets of
models). A clause is Horn if the number of positive literals in it is at most one, and a CNF is
Horn if it contains only Horn clauses. It is known that a theory  is Horn if and only if  can be
represented by some Horn CNF. By denition, a negative function is Horn, but not conversely.
For any Horn theory , a model a 2  is called characteristic if it cannot be produced by
bitwise AND of other models in ; a 62
fag). The set of all characteristic models of
a Horn theory , which we call the characteristic set of , is denoted by Char(). Note that
every Horn theory  has a unique characteristic set Char(), which satises
. The set of minimal models of f with respect to p 2 f0; 1g n is dened as
there exists no b 2 (f) satisfying b < p ag,
where b < p a denotes that b  p a and b 6= a hold. The following lemma gives an upper bound
on the size (i.e., cardinality) of the characteristic set.
Lemma 2.2 [9] Let f be a Horn function on n variables. Then, the characteristic set of f has
size at most
ng and  E n;i is the characteristic
vector of the set E n;i  f0; ng given by
ng for
2.2 Ordered Binary Decision Diagrams
An ordered binary decision diagram (OBDD) is a directed acyclic graph that represents a Boolean
function. It has two sink nodes 0 and 1, called the 0-node and the 1-node, respectively (which
are together called the constant nodes). Other nodes are called variable nodes, and each variable
node v is labeled by one of the variables x 1 denote the label of node v.
Each variable node has exactly two outgoing edges, called a 0-edge and a 1-edge, respectively.
One of the variable nodes becomes the unique source node, which is called the root node. Let
denote the set of n variables. A variable ordering is a total ordering
associated with each OBDD, where  is a permutation f1; 2; . ; ng !
ng. The level 3 of a node v, denoted by level(v), is dened by its label; if node v has
label x (i) , level(v) is dened to be That is, the root node is in level n and has
label x (1) , the nodes in level n 1 have label x (2) and so on. The level of the constant nodes
is dened to be 0. On every path from the root node to a constant node in an OBDD, each
variable appears at most once in the decreasing order of their levels.
Every node v of an OBDD also represents a Boolean function f v , dened by the subgraph
consisting of those edges and nodes reachable from v. If node v is a constant node, f v equals
to its label. If node v is a variable node, f v is dened as var(v) f 0-succ(v) _ var (v) f 1-succ(v)
by Shannon's expansion, where 0-succ(v) and 1-succ(v), respectively, denote the nodes pointed
by the 0-edge and the 1-edge of node v. The function f represented by an OBDD is the one
represented by the root node. Figure 1 illustrates three OBDDs representing x 3 x 2 _ x 1 with a
3 This denition of level may be dierent from its common use.
0-edge
1-edge
constant node
variable node
(a)
(b) (c)

Figure

1: OBDDs representing x 3 x 2 _ x 1 .
variable ordering Given an assignment a, the value of f(a) is determined by following
the corresponding path from the root node to a constant node in the following manner: at a
variable node v, one of the outgoing edges is selected according to the assignment a var(v) to the
variable var (v). The value of the function is the label of the nal constant node.
When two nodes u and v in an OBDD represent the same function, and their levels are the
same, they are called equivalent. A node whose 0-edge and 1-edge both point to the same node
is called redundant. An OBDD is called dense if every variable node v satisfy
all paths from the root node to constant nodes visit
nodes). A dense OBDD which has no equivalent nodes is quasi-reduced. A quasi-reduced OBDD
which has no redundant nodes is reduced. The OBDDs (a), (b) and (c) in Fig. 1 are dense, quasi-
reduced and reduced, respectively. In the following, we assume that all OBDDs are reduced,
unless otherwise stated. The size of an OBDD is the number of nodes in the OBDD. Given
a function f and a variable ordering, its reduced OBDD is unique and has the minimum size
among all OBDDs with the same variable ordering. The minimum sizes of OBDDs representing
a given Boolean function depend on the variable orderings [2].
Given an OBDD that represents f , the OBDDs of f j x i =0 and f j x i =1 can be obtained in
denotes the size of the OBDD of f . The size does not increase by
a restriction. Given two OBDDs representing f and g, applying fundamental logic operators,
g, can be performed in O(jf j  jgj) time, and property f  g
can be also checked in O(jf j
A partition for f is a pair of sets (L; R) satisfying L; R
and L \ is called a left partition and R is called a right partition. Let l denote an
assignment to the variables in L, and r denote an assignment to the variables in R. Then, l  r
denotes the complete assignment obtained by combining l and r. Let X 0 be a subset of X, and
! be a positive number satisfying 0 < ! < 1. Then, a partition (L; R) is called !-balanced for
Given a partition (L; R), a set A of assignments
l i for L and r i for R, h, is called a fooling set if it satises
for some a 2 f0; 1g. The next lemma tells that the size h of a fooling set gives a lower bound
on the size of an OBDD that represents f .
Lemma 2.3 [3] Let f be a Boolean function on n variables, X 0 be a subset of the variables and
! be a positive number satisfying 0 < ! < 1. If f has a fooling set of size at least h for every
!-balanced partition (L; R) for X 0 , then the size of OBDD representing f is at least h for any
variable ordering.
3 Three Approaches for Knowledge-Base
Representation
In this section, we compare three knowledge-base representations: CNF-based, model-based, and
OBDD-based. It is known that CNF-based and model-based representations play orthogonal
roles with respect to space requirement. Namely, each of them sometimes allows exponentially
smaller sizes than the other, depending on the functions. We show that OBDD-based representation
is incomparable to the other two in the same sense.
We start with relations between OBDD and CNF representations.
Lemma 3.1 There exists a negative theory on n variables, for which OBDD and CNF both
require size O(n), while its characteristic set requires
size
z n=2 ).
Proof: Consider a function
2m. The size of this CNF is obviously O(n). The characteristic set is given by
exactly one of a 2i 1 or a 2i is 0 for all whose size is
The OBDD representing f A is illustrated in Fig. 2, with a variable ordering
The size of this OBDD is O(n). 2
0-edge
1-edge

Figure

2: OBDD representing f
Lemma 3.2 There exists a negative theory on n variables, for which OBDD requires size O(n)
and the characteristic set requires size O(n 2 ), while CNF requires
size
z n=2 ).
Proof: Consider a function
_
to f A . The smallest CNF representation of f B , which is given above, has
clauses. The
characteristic set is f f1;2;.;2mgS 2 f0; 1g 2m
whose size is O(n 2 ) [6]. The OBDD representing
f B is illustrated in Fig. 3, with a variable ordering
f B is dual to f A , this OBDD is obtained by negating input variables (i.e., exchanging the roles
of 0-edges and 1-edges) and negating output (i.e., exchanging the roles of the 0-node and the
1-node) of the OBDD in Fig. 2. The size of this OBDD is O(n). 2
By combining Lemmas 3.1 and 3.2, we show that, for some theory, OBDD can be exponentially
smaller than its characteristic set and CNF representations.
Theorem 3.1 There exists a negative theory on n variables, for which OBDD requires size
O(n), while both of the characteristic set and CNF require
sizes
z n=4 ).
0-edge
1-edge

Figure

3: OBDD representing f
Proof: Consider a function
^@
2m _
As shown in Lemma 3.1, the characteristic set requires
size
z n=4 ) to represent
the rst half. Also by Lemma 3.2, CNF representation always requires
size
z n=4 ) to represent
the second half. Note the rst and second halves are independent since the variables in the rst
half do not appear in the second half and vice versa. Therefore, the above lower bounds of the
characteristic set and CNF are valid also for f C . An OBDD that represents f C is illustrated in
Fig. 4, with a variable ordering The size of this OBDD is O(n). 2
We now turn to the opposite direction, i.e., CNF and the characteristic set can be exponentially
smaller than the size of OBDD.
Lemma 3.3 The size of the characteristic set is O(n) for the following Horn function on n
variables x i;j , 1
f D =@
_
x i;jAA ^@

_
x i;j
as the set B n dened in Lemma 2.2,
for convenience, where E is the set E n;0 f(i; j)g
0-edge
1-edge
x n=2
x n=2+2

Figure

4: OBDD representing f
corresponding to variable x i;j . f D holds for the characteristic vector  E n;0 . Thus,
Similarly, jmin  E n;i;j (f D
since f D
Next, since f D implied by
we enumerate all minimal models for each  E n;i;m+1 . By denition, we obtain  E n;0 by
ipping the (i; m+1)-th coordinate of  E n;i;m+1 . This  E n;0 is a minimal model for  E n;i;m+1 since
When the (i; m+ 1)-th coordinate is xed to 0, the clause
is
satised by
ipping at least one of the (i; j)-th coordinates among
two or more (i; j)-th coordinates are
ipped, the corresponding vector is not minimal. Thus, we
have jmin  E n;i;m+1 (f D m. Similarly, we have jmin  E n;m+1;j (f D
We also enumerate all minimal models for  En;m+1;m+1 since f D ( En;m+1;m+1
obtain  E n;0 by
ipping the (m+1;m+1)-th coordinate. When the (m+1;m+1)-th coordinate
is xed to 0, minimal models are obtained by
ipping exactly one of the (i; m+1)-th coordinates
among exactly one of the (m coordinates among
Thus, we have jmin  E n;m+1;m+1 (f D In total, we have P
a2Bn jmin a (f D
i.e., O(n). By Lemma 2.2, this means that the size of the characteristic set of f D is O(n). 2
Lemma 3.4 [15] Let f be a Boolean function on n variables x i;j , 1
Then, for any partition (L; R) satisfying either of the following properties
holds:
(1) There are at least m=
dierent i's satisfying fx
(2) There are at least m=
dierent j's satisfying fx
Lemma 3.5 The size of OBDD representing the following negative function f E on n variables
variable ordering:
_
x i;jAA ^@
_
x i;j
Proof: We prove this by Lemma 2.3 in Section 2.2. Let us consider that the set X 0 in
Lemma 2.3 is given by the set of all variables, and for every balanced partition
assuming case (1) of Lemma 3.4 without loss of generality, we have at least m=
pdierent i's satisfying fx We select
2 of these i's, I
g. For every i k 2 I, we can select two variables x i k ;l k 2 L
and x i k ;r k 2 R. We construct a set A of assignments such that each assignment satises the
following restrictions:
(1) For every assigned either (0; 1) or (1; 0).
(2) For every are assigned 1.
(3) Other variables are assigned 0.
The size of the set A is 2 m=
2 since there are choices in restriction (1). Let l h  r h denote the
assignment satisfying
.
Now, we prove that set A is a fooling set, dened just before Lemma 2.3. First, we show
assigned 0,
all are assigned 0, we have W m
mg. Thus, we have f E (l h  r h
Next, we show that f E (l h  r h 0
there exists at least one
variable x which is assigned 1 by l h  r h and 0 by l h 0
. By restriction (1), x i k ;r k is then
assigned 0 by l h  r h and 1 by l h 0
. Therefore, x i k ;l k and x i k ;r k are assigned 1 by assignment
l h  r h 0
, implying that
holds. This proves that A is a fooling set. Since the size of
this fooling set is at least 2 m=
2 for any balanced partition, this lemma follows from Lemma 2.3.Theorem 3.2 There exists a Horn theory on n variables, for which CNF requires size O(n)
and the characteristic set requires size O(n), while the size of the smallest OBDD representation
is
s
Proof: Consider the function f D in Lemma 3.3. As stated in Lemma 3.3, the size of its
characteristic set is O(n). Also the size of the CNF is obviously O(n). The function f E in
Lemma 3.5 is obtained by restricting x 1;m+1 ; . ; xm;m+1 , xm+1;1 ; . ; xm+1;m and xm+1;m+1 of
f D to 0. Since the size of OBDD does not increase by a restriction, the size of the smallest
OBDD of f D is

The above results show that none of the three representations can always dominate the
other two. OBDDs can nd a place in knowledge-bases as they can represent some theories
more e-ciently than others.
Unfortunately, by combining Theorems 3.1 and 3.2, the following negative result is obtained.
Corollary 3.1 There exists a Horn function on n variables, for which both of the characteristic
set and CNF require
sizes
and the size of the smallest OBDD representation is
s
Proof: Consider a function which consists of two parts, where the rst one (resp., second
one) corresponds to f C in Theorem 3.1 (resp., f D in Theorem 3.2). Both have n=2 variables
respectively, and share none of the variables. Similarly to the case of Theorem 3.1, the lower
bounds for the three representations are easily obtained. 2
Checking Unateness of OBDD
In this section, we discuss the problem of checking whether a given OBDD represents a unate
function. We assume, without loss of generality, that the variable ordering is always
The following well-known property will show that this problem can be solved in polynomial
time.
Property 4.1 Let f be a Boolean function on n variables x 1 unate with
holds for every
As noted in subsection 2.2, an OBDD representing f can be obtained
in O(jf j log jf time from the OBDD representing f , where jf j denotes its size. The size does
not increase by a restriction f j x i =0 or f j x i =1 . Since the property g  h can be checked in
O(jgj  jhj) time, the unateness of f can be checked in O(njf checking the conditions
The following well-known property is useful to reduce the computation time.
Property 4.2 Let f be a Boolean function on n variables x 1 unate with
only if (i) both f j xn=0 and f j xn=1 are unate with polarity
The unateness of functions f j xn=0 and f j xn=1 can be checked by applying Property 4.2
recursively, with an additional condition that f j xn=0 and f j xn=1 have the same polarity. Note
that the property f j xn=0  f j xn=1 (resp., f j xn=0  f j xn=1 ) can be also checked recursively,
since it holds if and only if f j xn=0; xn 1 =an 1
Algorithm CHECK-UNATE in Fig. 5 checks the above conditions in the bottom-up manner
(i.e., from level to the root node). We use an array p[ ' ] to denote the polarity of f with
respect to x ' in level '; each element stores 0, 1 or  (not checked yet). We also use a two-dimensional
array imp[u; v] to denote whether f u  f v holds or not; each element stores YES,
NO or  (not checked yet). In Step 2, the unateness with the polarity specied by array p is
checked for the functions of the nodes in level '. More precisely, the unateness of the functions
is checked in Step 2-1, and the consistency of their polarities is checked in Step 2-2. In Step 3,
imp[u; v] are computed for the functions f u and f v in levels up to '.
The unateness check of f v in Step 2-1 can be easily done, since both f 0-succ(v) (i.e., f v j x ' =0 )
and f 1-succ(v) (i.e., f v j x ' =1 ) have already been checked to be unate with polarity (p[1 ]; p[2 ]; . ;
p[' 1]), and f 0-succ(v) and f 1-succ(v) have been compared in Step 3 of the previous iteration.
Note that constant functions 0 and 1 are considered to be unate. The polarity of f v with respect
to x ' in level ' is temporarily stored in pol in Step 2-1.
In Step 2-2, the polarity consistency with respect to x ' is checked by comparing the polarity
of node v (which is pol ) and p[ ' ]. If p[ ' is the rst node checked in level '), we store
Algorithm
Input: An OBDD representing f with a variable ordering
Output: \yes" and its polarity if f is unate; otherwise, \no".
imp[u; v] :=> > <
otherwise;
' := 1.
(check unateness in level ' and compute p[ ' ]). For each node v in level ' (i.e.,
labeled with x ' ), apply Steps 2-1 and 2-2.
Step 2-1. Set pol := 0 if imp[0-succ(v);
output \no" and halt.
Step 2-2. If p[ '
\no" and halt.
Step 3 (compute imp in level '). For each pair of nodes (u; v) (where (u; v) and (v; u)
are considered dierent) such that level(u)  ' and level(v)  ', and at least one of
level(u) and level(v) is equal to ', set imp[u; v] := YES if both imp[0-succ 0 (u); 0-succ 0 (v)] and
imp[1-succ 0 (u); 1-succ 0 (v)] are YES; otherwise, set imp[u; v] := NO.
Step 4 (iterate). If is the level of the root node, then output \yes" and polarity
halt. Otherwise set ' return to Step 2.

Figure

5: Algorithm CHECK-UNATE to check the unateness of an OBDD.
pol in p[ ' ]. Otherwise, pol is checked against p[ ' ] and \no" is output if they are not consistent.
Note that CHECK-UNATE outputs p[ ' there are no nodes in level ' (i.e., f does not
depend on x ' ).
In Step 3, comparison between f u and f v is also performed easily, since the comparisons
between f u j x ' =a ' and f v j x ' =a ' for both a Here we
use the convention that 0-succ 0 (v) (resp., 1-succ 0 (v)) denotes 0-succ(v) (resp., 1-succ(v)) if
This is because f v j x '
hold if holds if level(v) < '. Note
that f holds if and only if u and v are the same node. After Step 3 is done for some ', we
know imp[u; v] for all pairs of nodes u and v such that level(u)  ' and level(v)  '. We store
all the results, although some of them may not be needed.
Next, we consider the computation time of this algorithm. In Step 2, the computation for
each v is performed in constant time from the data already computed in the previous Step 3.
Thus the total time of Step 2 is O(jf j). In Step 3, the comparison between f u and f v for each
pair (u; v) is performed in constant time. The number of pairs compared in Step 3 during the
entire computation is O
Theorem 4.1 Given an OBDD representing a Boolean function f , checking whether f is unate
can be done in O(jf is the size of the given OBDD.
If we start Algorithm CHECK-UNATE with initial condition
for all check the positivity (resp. negativity) of f . This is because f is
positive (resp., negative) if and only if the polarities of all nodes are 0 (resp., 1).
Corollary 4.1 Given an OBDD representing a Boolean function f , checking whether f is positive
(resp., negative) can be done in O(jf is the size of the given OBDD.
Checking Horness of OBDD
In this section, we discuss the problem of checking whether a given OBDD represents a Horn
function. After examining the condition for Horness in the next subsection, an algorithm will
be given in subsection 5.2.
5.1 Conditions for Horness
We assume, without loss of generality, that the variable ordering is always
Denoting f j xn=0 and f j xn=1 by f 0 and f 1 for simplicity, f is given by
are Boolean functions on Similarly to the case
of unateness, we check the Horness of f in the bottom-up manner.
Lemma 5.1 Let f be a Boolean function on n variables x 1 which is expanded as
only if both f 0 and f 1 are Horn and f
holds.
Proof: We rst prove the identity
by considering all models:
Now, the if-part of the lemma is immediate from (1), because the Horness of f 0 and f 1 (i.e.,
and the property f imply
Next, we consider the imply
Equality (2) implies that f 1 is Horn. Also f holds since a ^ bit a = a holds
for any model a in (f 0 ). Thus, we have
By combining (3) and (4), we have f holds if and
only if g  f holds, we also have f
The Horness of f 0 and f 1 can be checked by applying Lemma 5.1 recursively. The following
lemma says that the condition Lemma 5.1 can be also checked in the bottom-up
Lemma 5.2 Let f , g and h be Boolean functions on n variables, which are expanded as
holds if and only if f
Proof: The identity
can be proved in a manner similar to (1) by considering all models. Then, since f ^ bit g  h
holds if and only if (f ^ bit g)j
hold, we can prove this lemma by Lemma 2.1(2). 2
Note that the condition of type f ^ bit g  f in Lemma 5.1 requires to check the condition
of type (i.e., checking of type f ^ bit g  h for three functions f , g and h). The
last condition can be checked recursively by Lemma 5.2.
5.2 Algorithm to Check Horness
Applying Lemmas 5.1 and 5.2 recursively, the Horness of a Boolean function f can be checked
by scanning all nodes in a given OBDD in the bottom-up manner. Namely, for each node v in
level ', we check the condition of Lemma 5.1, i.e., whether both f v j x ' =0 and f v j x ' =1 are Horn
holds. Lemma 5.2 gives the condition how f v j x '
can be checked in the bottom-up manner.
Algorithm CHECK-HORN in Fig. 6 checks the Horness of a given OBDD in the above
manner. We use an array horn [v] to denote whether each node v represents a Horn function
or not, and a three-dimensional array bit-imp[u; v; w] to denote whether f
or not. Each element of the arrays stores YES, NO or  (not checked yet); horn
says that f v is Horn and bit-imp[u; v; holds. We note here
that, since the OBDD is reduced, the condition f may be checked for functions
in dierent levels; in such case, all functions are considered to have l max variables by adding
dummy variables, where l max denotes the maximum level of the nodes u, v and w.
In Step 2 of Algorithm CHECK-HORN, horn [v] for each v can be computed in constant time
by Fig. 7, which corresponds to Lemma 5.1, since f v j x level(v)
f 1-succ(v) hold, and horn[0-succ(v)], horn[1-succ(v)] and bit-imp[0-succ(v); 1-succ(v); 0-succ(v)]
in Fig. 7 have already been computed in the previous iterations.
Similarly, bit-imp[u; v; w] in Step 3 for each triple (u; v; w) can be computed in constant
time by Fig. 8, which corresponds to Lemma 5.2. As in the case of Algorithm CHECK-UNATE,
itself if level(v) < '. Upon completing Step 3 for ', we have the results bit-imp[u; v; w] for all
triples (u; v; w) such that level(u)  ', level(v)  ' and level(w)  '. These contain all the
information required in the next iteration, although some of them may not be needed.
Now, we consider the computation time of Algorithm CHECK-HORN. In Step 2, since
horn [v] for each node v is computed in constant time, O(jf time is required for checking all
Algorithm CHECK-HORN
Input: An OBDD representing f with a variable ordering
Output: \yes" if f is Horn; otherwise, \no".
horn [v] :=
YES if v is a constant node 0 or 1;
otherwise;
otherwise;
' := 1.
(check Horness in level '). For each node v in level ' (i.e., labeled with x ' ), check
whether the function f v is Horn according to Fig. 7, and set its result YES or NO to horn [v]. If
there exists at least one node in level ' which is not Horn, output \no" and halt.
Step 3 (compute bit-imp in level '). For each triple (u; v; w) of nodes such that level(u)  ',
level(v)  ' and level(w)  ', and at least one of level(u), level(v) and level(w) is equal to
check whether f holds according to Fig. 8, and set its result YES or NO to
Step 4 (iterate). If halt. Otherwise set ' := return to
Step 2.

Figure

Algorithm CHECK-HORN to check the Horness of an OBDD.
YES if all of horn[0-succ(v)], horn[1-succ(v)] and
are YES.
NO otherwise.

Figure

7: Checking horn [v] for a node v in Step 2.
YES if all of bit-imp[1-succ 0 (u); 1-succ 0 (v); 1-succ 0 (w)],
and bit-imp[1-succ 0 (u); 0-succ 0 (v); 0-succ 0 (w)] are YES.
NO otherwise.

Figure

8: Checking bit-imp[u; v; w] (i.e., f
for a triple of nodes (u; v; w) in Step 3.
nodes in the OBDD. In Step 3, bit-imp[u; v; w] for each triple (u; v; w) is also computed in
constant time. The number of triples to be checked in Step 3 during the entire computation is
O(jf j 3 ). The time for the rest of computation is minor.
Theorem 5.1 Given an OBDD representing a Boolean function f , checking whether f is Horn
can be done in O(jf j 3 ) time, where jf j is the size of the given OBDD.
6 Conclusion
In this paper, we considered to use OBDDs to represent knowledge-bases. We have shown that
the conventional CNF-based and model-based representations, and the new OBDD representation
are mutually incomparable with respect to space requirement. Thus, OBDDs can nd their
place in knowledge-bases, as they can represent some theories more e-ciently than others.
We then considered the problem of recognizing whether a given OBDD represents a unate
Boolean function, and whether it represents a Horn function. It turned out that checking
unateness can be done in quadratic time of the size of OBDD, while checking Horness can be
done in cubic time.
OBDDs are dominatingly used in the eld of computer-aided design and verication of
digital systems. The reason for this is that many Boolean functions which we encounter in
practice can be compactly represented, and that many operations on OBDDs can be e-ciently
performed. We believe that OBDDs are also useful for manipulating knowledge-bases. Developing
e-cient algorithms for knowledge-base operations such as deduction and abduction should
be addressed in the further work.

Acknowledgement

The authors would like to thank Professor Endre Boros of Rutgers University for his valuable
comments. This research was partially supported by the Scientic Grant-in-Aid from Ministry
of Education, Science, Sports and Culture of Japan.



--R















Theoretical Studies on Memory-Based Parallel Computation and Ordered Binary Decision Diagrams
--TR
A theory of the learnable
Graph-based algorithms for Boolean function manipulation
On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication
Efficient implementation of a BDD package
Sequential circuit verification using symbolic model checking
Shared binary decision diagram with attributed edges for efficient Boolean function manipulation
Structure identification in relational data
An empirical evaluation of knowledge compilation by theory approximation
The complexity of logic-based abduction
Horn approximations of empirical data
Reasoning with models
Logic synthesis for large pass transistor circuits
Fast exact minimization of BDDs
Approximation and decomposition of binary decision diagrams
Doing two-level logic minimization 100 times faster
BDS
OBDDs of a Monotone Function and of Its Prime Implicants
On Horn Envelopes and Hypergraph Transversals
Reasoning with Ordered Binary Decision Diagrams
Translation among CNFs, Characteristic Models and Ordered Binary Decision Diagrams

--CTR
Takashi Horiyama , Toshihide Ibaraki, Translation among CNFs, characteristic models and ordered binary decision diagrams, Information Processing Letters, v.85 n.4, p.191-198, 28 February
unate functions;recognition problems;ordered binary decision diagrams OBDDs;automated reasoning;horn functions;knowledge representation