Fast Subsumption Checks Using Anti-Links.
The concept of anti-link is defined (an anti-link consists of two occurrences of the same literal in a formula), and useful equivalence-preserving operations based on anti-links are introduced. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. Those anti-links that directly indicate the presence of subsumed paths are characterized. The operations have linear time complexity in the size of that part of the formula containing the anti-link.The problem of removing all subsumed paths in an NNF formula is shown to be NP-hard, even though such formulas may be small relative to the size of their path sets. The general problem of determining whether there exists a pair of subsumed paths associated with an arbitrary anti-link is shown to be NP-complete. Additional techniques that generalize the concept of pure literals are introduced and are also shown to eliminate redundant subsumption checks. The effectiveness of these techniques is examined with respect to some benchmark examples from the literature.
Introduction
The logical consequences of a ground formula, expressed as minimal implied clau-
ses, are useful in certain approaches to non-monotonic reasoning (Kean and Tsi-
knis, 1992; Przymusinski, 1989; Reiter and de Kleer, 1987), where all consequences
of a formula set (e.g., the support set for a proposed commonsense conclusion) are
required. Minimal conjunctions that imply a formula are useful in situations where
satisfying models are desired, as in error analysis during hardware verification.
Such minimal implied clauses are the formula's prime implicates, and the minimal
conjunctions that imply it are its prime implicants.
Many algorithms have been proposed to compute the prime implicates of propositional
boolean formulas. Most algorithms (de Kleer, 1992; Jackson and Pais,
1990; Jackson, 1992; Kean and Tsiknis, 1990; Slagle et al., 1970) assume that
the input is either in conjunctive normal form (CNF) or in disjunctive normal
form (DNF). The algorithm of (Ngair, 1993) requires the input to be a conjuncti-
This research was supported in part by National Science Foundation Grant CCR-9101208
(Ramesh and Murray) and by Deutsche Forschungsgemeinschaft within the Schwerpunktpro-
Deduktion (Beckert and H-ahnle). Some of the results in this paper appear in condensed
form in the Proceedings of the 5 th International Conference on Logic Programming and Automated
Reasoning, Kiev, Ukraine, July 16-21, 1994, and in the Proceedings of the National Conference
on Artificial Intelligence, Seattle, WA, July 31-August 4, 1994.
on of DNF formulas. In (Ramesh and Murray, 1993) we propose a set of techniques
for finding the prime implicates of formulas in negation normal form (NNF). Our
techniques are based on dissolution, an inference rule introduced in (Murray and
Rosenthal, 1987b), and on an algorithm called Pi. We have discovered classes of
formulas for which our techniques are polynomial but for which any CNF/DNF-
based technique must be exponential in the size of the input. Ngair has also
introduced similar examples; however, our method is more general than Ngair's
which is based on order theory (Ngair, 1993). Coudert and Madre (1992) have
also developed an algorithm for computing prime implicates and implicants of formulas
in which binary decision diagrams (BDDs) are employed. Although we use
prime implicate/implicant generation as an example to demonstrate the utility of
anti-link operations, anti-link operations can be employed in any application that
requires eliminating subsumed paths in an NNF formula. We have successfully
used anti-link operations in a diagnosis system (Ramesh and Murray, 1995).
In (Ramesh and Murray, 1993) we describe the Pi algorithm; there, Pi is used
to enumerate all the prime implicates of a full dissolvent, an NNF formula that
has no conjunctive links (defined later). Pi repeatedly does subsumption checks to
keep intermediate results as small as possible. However these checks are expensive.
Many result in failure, and they have to be done on sets which can be exponentially
large. The time required for these operations can be reduced by using a more
compact representation of the intermediate results (de Kleer, 1992), but avoiding
as many such checks as possible is the focus of this paper.
We show that the full dissolvent can be restructured before applying Pi such
that many non-prime implicates are removed without doing subsumption checks
at all. We define disjunctive and conjunctive anti-links 1 in NNF formulas, and we
identify operations to remove such anti-links and their associated subsumed paths.
This leaves fewer subsumption checks for the Pi algorithm.
In the next section we describe our path semantics viewpoint and our graphical
representation of formulas in classical logic. In Section 3 we introduce anti-links
and develop useful equivalence-preserving operations based on them. In Section 4,
complexity issues are discussed and some NP-completeness results are proven.
Section 5 introduces further techniques based on strictly pure subformulas. The
effectiveness of our techniques on certain benchmark formulas described by Ngair
(1993) is explored. In Section 6 we introduce strictly pure full blocks and use them
to develop a method that reduces the number of subsumption tests required.
1 Anti-links and some associated operators were first proposed by Beckert and H-ahnle - personal
communication. The first motivation for studying anti-links arose in connection with regular
clausal tableau calculi (Letz et al., 1992). The anti-link rule as it will be defined later can be
viewed as an implementation of the regularity condition in (Letz et al., 1992) for the propositional
non-clausal case (Letz et al. considered the first-order clausal case). There, refinements of general
inference rules are considered, whereas the anti-link rule allows implementation as a preprocessing
step.
Fast Subsumption Checks Using Anti-Links 3
Foundations: Facts on Formulas in Negation Normal Form
We assume the reader to be familiar with the notions of atom, literal, and formula
from classical logic. We consider only formulas in negation normal form (NNF):
The only connectives used are conjunction and disjunction, and all negations are
at the atomic level. This restriction is reasonable, since formulas that contain
negations and other operators at any level can be converted to NNF in polynomial
time.
In this section, we introduce a number of technical terms and definitions that
are treated in detail in (Murray and Rosenthal, 1993). They are required for the
development of the anti-link operations defined in Section 3, and they make the
paper self-contained even for readers not familiar with dissolution.
2.1 Semantic Graphs
Semantic graphs are a graphical representation of NNF formulas:
Definition 1. A semantic graph consists either of
1. one of the constants true and false,
2. a literal A or A,
3. a c-arc, which is a conjunction of two semantic graphs, or
4. a d-arc, which is a disjunction of two semantic graphs.
We use the notation (X; Y ) c for the c-arc from X to Y and similarly use (X; Y ) d
for a d-arc; the subscript may be omitted when no confusion is possible.
Each semantic graph used in the construction of a semantic graph G is called
an explicit subgraph of G. If
subgraph of G if X (Y ) is not a c-arc; otherwise the fundamental subgraphs of X
(Y are fundamental subgraphs of G. Similarly if
a fundamental subgraph of G if X (Y ) is not a d-arc, otherwise the fundamental
subgraphs of X (Y ) are fundamental subgraphs of G.
The set of nodes of a semantic graph G consists of all literal occurrences used
in its construction; the same holds for the set of c-arcs of G and the set of d-arcs
of G; i.e., these sets include the nodes, c-arcs, and d-carc, respectively, occurring
in the explicit subgraphs of G.
In the following, we identify a semantic graph G and the formula it represents 2 ;
essentially, the only difference between the semantic graph and the formula is the
point of view, and we will use either term depending upon the desired emphasis.
For a more detailed exposition, see (Murray and Rosenthal, 1993).
true, false, and positive literals represent themselves; a negative literal A represents :A;
4 Anavai Ramesh et al.
In addition, we identify a semantic graph and the triple consisting of its set of
nodes, its set of c-arcs, and its set of d-arcs. The only exception, were this latter
identification is not possible, because it would be ambiguous, are the semantic
graphs true and false (both correspond to (;; ;; ;)). Note, however, that when a
semantic graph contains occurrences of true and false, the obvious truth-functional
reductions apply. Unless otherwise stated, we will assume that semantic graphs
are automatically so reduced.
In pictorial representations, c-arcs and d-arcs are indicated by the usual symbols
for conjunction and disjunction; the arguments of a c-arc are placed vertically
above each other, the arguments of a d-arc horizontally besides each other.
Example 1. Below, the formula
E) - (:A - (B - C)) (1)
is displayed as a semantic
A
Y
(2)
The boxes in (2) show the explicit subgraphs used in the construction of the
semantic graph (since c-arcs and d-arcs are associative and commutative we do
not show the explicit subgraphs in subsequent pictorial representations).
Definition 2. If A and B are nodes in a graph, and if (X; Y ) ff is an arc
or d) with A in X and B in Y , we say that is the arc connecting A
and B, and that A and B are ff-connected.
Example 2. In (2), C is c-connected to each of B, A, C, D, and E, and is d-
connected to A.
Definition 3. Let G be a semantic graph. A partial c-path through G is a set
of nodes such that any two are c-connected, and a c-path through G is a partial
c-path that is not properly contained in any partial c-path.
(Partial) d-paths are defined accordingly using d-arcs instead of c-arcs.
'(p) denotes the set of literals of a path p.
Fast Subsumption Checks Using Anti-Links 5
Example 3. Below, the semantic graph (2) is shown with lines indicating its c-
paths (on the left) and its d-paths (on the right):
A
A
The c-paths are fC; A; Ag, fC; A; B; Cg, fD; Ag, fD; B; Cg, fE; Ag, fE; B; Cg;
the d-paths are fC; D; Eg, fA; D; Eg, fA; Bg, fA; Cg.
The following lemma is obvious.
Lemma 1. Let G be a semantic graph. Then an interpretation I satisfies (falsi-
fies) G iff I satisfies (falsifies) every literal on some c-path (d-path) through G.
2.1.1 Subgraphs
We will frequently find it useful to consider subgraphs of a semantic graph that
are not explicit.
Definition 4. Given a semantic graph G and a non-empty subset N of the nodes
of G, the subgraph of G that corresponds to N is that part of G that consists of
nodes from N , where the logical structure of that part is preserved.
denotes the subgraph of G corresponding to the set of nodes of G that
are not in N .
Two subgraphs H and H 0 of G meet each other if they have nodes in common.
A non-empty subset N of nodes corresponds unambiguously to one subgraph
of G. The empty set corresponds to both true and false; true and false are sub-graphs
of all semantic graphs.
For a more precise definition of subgraphs, see (Murray and Rosenthal, 1993).
Example 4. Below the subgraph of (2) is shown that corresponds to the node set
g.
A - D
A
6 Anavai Ramesh et al.
2.1.2 Blocks
The most important subgraphs are the blocks:
Definition 5. A c-block H is a subgraph of a semantic graph G with the property
that any c-path p that includes at least one node from H passes through H , where p
passes through H iff the subset of p consisting of nodes of H is a c-path through H .
d-blocks are accordingly defined using d-paths.
Example 5. In (2), the subgraph corresponding to the node set fA; D; E;A; Cg
is a c-block. However, it is not a d-block since the d-path fA; Bg restricted to the
subgraph is fAg, which is a proper sub-path of fA; Cg in the subgraph.
Definition 6. A full block is a subgraph that is both a c-block and a d-block.
One way to envision a full block is to consider conjunction and disjunction as
n-ary connectives. Then a full block is a subset of the arguments of one connective,
i.e., of one explicit subformula.
Full blocks may be treated as essentially explicit subgraphs (up to the order of
arguments), and the Isomorphism Theorem from (Murray and Rosenthal, 1987a)
assures us that they are the only structures that may be so treated.
Example 6. In (2), the subgraph corresponding to fC; A; Eg is a full block. It
can be written as (fC; Ag; E) d ; i.e., we can regard the upper part of the graph
as (fC; A; Eg; D) d . The fundamental subgraphs of the upper disjunction are
and the literals D and E.
Definition 7. Let H be a full block; H is a conjunction or a disjunction of fundamental
subgraphs of some explicit subgraph M . If the final arc of M is a
conjunction, then we define the c-extension of H to be M and the d-extension of
H to be H itself. The situation is reversed if the final arc of M is a d-arc.
We use the notation CE(H) and DE(H) for the c- and d-extensions, respecti-
vely, of H .
Example 7. In (2),
In this paper, we compute c- and d-extensions of single nodes only. Single nodes
are always full blocks and so testing for this property will be unnecessary. If we
assume that formulas are represented as n-ary trees, computing these extensions
can be done in constant time; we merely determine whether the given node's parent
is a conjunction or a disjunction, and the appropriate extension is then either the
node itself or the parent.
Fast Subsumption Checks Using Anti-Links 7
2.2 Path Dissolution
Path dissolution (Murray and Rosenthal, 1993) is an inferencing mechanism for
classical logic that has several interesting properties. It is an efficient generalization
of the method of analytic tableaux, is strongly complete in the propositional case,
and can produce a list of satisfying interpretations of a formula. The latter feature
is particularly valuable in this or in any setting in which one wishes to make use
of satisfying interpretations rather than merely to determine whether any exist.
Path dissolution works by selecting a link and restructuring the formula so
that all paths through the link are eliminated. The nature of the restructuring is
such that one cannot rely on CNF (conjunctive normal
starts out in CNF, a single dissolution step produces an unnormalized formula.
One consequence of eliminating all paths through a link is strong completeness:
Any sequence of dissolution steps will eventually create a linkless formula. The
paths that remain may be interpreted as models (satisfying interpretations) of the
formula.
Definition 8. A c-link is a complementary pair of c-connected nodes; d-connec-
ted complementary nodes form a d-link.
Unless stated otherwise, we use the term link to refer to a c-link. Path dissolution
is in general applicable to collections of links; here we restrict attention to
single links.
Example 8. Consider the link fA; Ag in (2). Then the entire graph
is the smallest full block containing the link.
Definition 9. Let X be a semantic graph and H an arbitrary subgraph. 3
The c-path complement of H with respect to X , written CC(H;X), is the
subgraph of X consisting of all literals in X that lie on c-paths that do not contain
nodes from H . If no such literal exists, CC(H;X)= false.
The c-path extension of H with respect to X , written CPE(H;X), is the sub-graph
of X containing all literals that lie on c-paths that pass through H . If no
such literal exists,
In the development of anti-link operations, we will use operations that are the
duals of CC and CPE. We use DC for the d-path complement and DPE for the
d-path extension operators. Their definitions are straightforward by duality,
Because we consider only single link dissolution, the first arguments of CC
and CPE will be literals when these operators are used in the construction of
dissolvents in the examples below. However, this is not the case in Section 3, and
hence the above definitions of these operators are in full generality.
usually is but does not have to be a subgraph of X.
4 Note, that CPE has two arguments whereas CE (Def. 7) has but one; intuitively, CE has an
implicit second argument that is always the entire graph in which the explicit argument occurs.
8 Anavai Ramesh et al.
Example 9. In (2),
E)
The above definitions of the operators CC and CPE are adequate for the
definition of dissolution. However, (equivalent) more constructive definitions are
given in Section 3, where they will be required in proving the correctness of the
anti-link operations introduced there.
The reader is referred to (Murray and Rosenthal, 1993) for the proofs of the
lemmas below.
Lemma 2. Let H be an arbitrary subgraph of G. The c-paths of CPE(H;G) are
precisely the c-paths of G that pass through H .
Corollary 1. CPE(H;G) is exactly the subgraph of G relative to the set of
nodes that lie on c-paths that pass through H .
Lemma 3. Let H be an arbitrary subgraph of G. The c-paths of CC(H;G) are
precisely the c-paths of G that do not pass through H .
Corollary 2. CC(H;G) is exactly the subgraph of G relative to the set of nodes
that lie on c-paths that do not pass through H .
Lemma 4. If H is a c-block, then CC(H;G)- CPE(H;G) and G have the same
c-paths.
The above lemmas and corollaries about CC and CPE all hold in dual form
for DC and DPE.
Suppose that we have literal occurrences A and A residing in conjoined sub-graphs
X and Y , respectively. It is intuitively clear that the c-paths through (X -
Y ) that do not contain the link fA; Ag are those through (CPE(A;X)-CC(A; Y
plus those through (CC(A; X)
Ag be a link, and let be the smallest
full block containing H . DV (H; M ), the dissolvent of H in M , is defined as follows:
If H is a single c-block, then DV (H;
Otherwise (i.e., if H consists of two c-blocks),
Fast Subsumption Checks Using Anti-Links 9
The only way that H can be a single c-block is if H is a full block (it is trivially a
d-block). In that case, and A and A must be (up to commutations and
reassociations) arguments of the same conjunction.
The following proposition follows from the corollaries and Lemma 4:
Proposition 1. Either of the two more compact graphs shown below has the
same c-paths as DV (H; M ), and may thus be used instead:
Y
The semantic graphs from the above proposition are not identical to DV (H; M)
as graphs, but they do have the identical c-paths: all those of the original full block
except those of CPE(A;X)- CPE(A; Y ), i.e., except those through the link.
Example 10. If we dissolve on the link fA; Ag in (2) (using the compact form (4)
of dissolution from Proposition 1), the graph that results is:
A
Theorem 1. Let H be a link in a semantic graph G, and let M be the smallest
full block containing H . Then M and DV (H; M) are logically equivalent.
A proof of Theorem 1 (in a more general form) can be found in (Murray and
Rosenthal, 1993).
We may therefore select an arbitrary link H in G and replace the smallest full
block containing H by its dissolvent, producing (in the ground case) an equivalent
graph. We call the resulting graph the dissolvent of G with respect to H . Since
the paths of the new graph are all that appeared in G except those that contained
the link, this graph has strictly fewer c-paths than the old one. As a result, finitely
many dissolutions (bounded above by the number of c-paths in the original graph)
will yield a linkless equivalent graph. This proves:
Theorem 2. At the ground level, path dissolution is a strongly complete rule of
That means, that the result of applying dissolution repeatedly to an unsatisfiable semantic
graph results in the graph false, independently of the choice of the link that is dissolved on at
each step.
2.3 Prime Implicates/Implicants
We briefly summarize basic definitions regarding implicates. The treatment for
implicants is completely dual and is indicated by appropriate dual expressions in
parentheses.
Definition 11. A disjunction (conjunction) D subsumes another disjunction D 0
(conjunction
true (false) is subsumed by all disjunctions (conjunctions).
A disjunction is called true iff it is equivalent to true. A conjunction is called
false iff it is equivalent to false.
Lemma 5. If a disjunction (conjunction) D 0 that is not true (false), then D subsumes
A true disjunction (false conjunction) subsumes another true disjunction (false
conjunction) only.
Definition 12. A disjunction (conjunction) P of literals is an implicate (impli-
cant) of a formula G, iff G
A disjunction (conjunction) D is a prime implicate (prime implicant) of a formula
G iff
1. D is not true (false).
2. D is an implicate (implicant) of G.
3. For all literals A i in D, Gj= (D
Note that the set of all prime implicates (implicants) of a formual G, when
treated as a CNF (DNF) formula, is equivalent to G.
Definition 13. Let D be the set of all prime implicates of a formula G. A prime
implicate D of G is essential if D n fDg is not equivalent to G, otherwise D is
inessential.
2.4 Fully Dissolved Formulas
If we dissolve in a semantic graph G until it is linkless, we call the resulting graph
the full dissolvent of G and denote it by FD(G). Observe that FD(G) is dependent
on the order in which links are activated. However, the set of c-paths in FD(G) is
unique: It is exactly the set of satisfiable c-paths in G. Because FD(G) is link-free,
the consequences, i.e., implicates, of G are represented in the d-paths of FD(G).
In a dual manner, we may define dissolution for disjunctive links; in that case,
FD(G) has no disjunctive links, and the implicants of G are represented in the
c-paths of FD(G). These relationships are made precise by Theorem 3 below.
Fast Subsumption Checks Using Anti-Links 11
In the discussion that follows, we will often refer to subsumption of d- and c-
paths rather than of disjuncts and conjuncts. Paths are defined as sets of literal
occurrences, but with regard to subsumption, we consider the literal set '(p) of
a path p. In this way, no change in the standard definitions is necessary. The
theorem below was proved in (Ramesh and Murray, 1993).
Theorem 3. In any non-empty formula in which no c-path (d-path) contains a
link, every implicate (implicant) of the formula is subsumed by some d-path (c-
path) in the formula.
Corollary 3. Every prime implicate (implicant) of a reduced DNF (CNF) for-
mula, i.e., one with no false conjuncts (true disjuncts), is subsumed by some d-path
(c-path) in the formula.
This follows directly from the theorem because such a DNF (CNF) formula has
no c-paths (d-paths) with links.
In (Ramesh and Murray, 1993), the prime implicates of G are computed by first
obtaining FD(G); then, knowing that all implicates are present in the d-paths of
FD(G), the Pi algorithm computes -(FD(G)), where
is a d-path through F , '(p) is not true;
for all d-paths q through
When used in this way, Pi extracts all unsubsumed non-tautological d-paths from
an NNF formula without c-links. In general, Pi computes -(F ) for an arbitrary
3 Subsumed Paths and Anti-Links
Much of the material in this section is a detailed description of the results sketched
in (Ramesh et al., 1994). Our goal is to first identify as many subsumed paths
as possible in an efficient manner and then eliminate them. The presence of anti-
links (both disjunctive and conjunctive) in a graph may indicate that subsumed
d-paths are present in the graph. We now define anti-links and then discuss ways
to identify and remove subsumed paths due to anti-links.
Definition 14. If is a d-arc in a semantic graph G and if AX and
A Y are nodes (occurrences of literal in X and in Y respectively, then we call
a disjunctive anti-link.
is a c-arc in G, then we call fAX ; A Y g a conjunctive anti-link.
Note, that M is the smallest full block containing the anti-link.
The following theorem relates subsumed paths to anti-links. The theorem is
immediate for CNF formulas; there is an obvious dual theorem regarding subsumed
c-paths that is immediate for DNF formulas.
12 Anavai Ramesh et al.
Theorem 4. Let G be a semantic graph in which a d-path p is subsumed by a
distinct non-tautological d-path p 0 in G. Then G contains either a disjunctive
anti-link or a conjunctive anti-link.
Proof. There are two distinct possibilities, either
Suppose there must be a literal having two different occurrences.
These two occurrences must be either d- or c-connected and thereby constitute
either a disjunctive or a conjunctive anti-link.
Suppose '(p) oe '(p 0 ). The proof is by induction on the structure of G.
Basis: G is a literal. The result is vacuously true since there cannot be two distinct
d-paths through G.
Induction step:
(a) Suppose are
both from the same explicit subgraph (X or Y ) or from different explicit
subgraphs. If they lie in the same explicit subgraph then the result
follows directly from the induction hypothesis. If they are from different
subgraphs then every literal in '(p 0 ) occurs at least once in X and at least
once in Y . Any two such occurrences of some literal in '(p 0 ) constitute
a conjunctive anti-link.
(b) Suppose Y be the restriction of p to X and
to Y respectively. Let p 0
Y be the restriction of p 0 to X and to
Y respectively. Since p and p 0 are distinct, either p X and p 0
X must be
distinct, or p Y and p 0
Y must be distinct (or both), so assume without loss
of generality that p X and p 0
are distinct.
If either p X subsumes p 0
X or vice versa, then by the induction hypothesis,
must have an anti-link and so does G. On the other hand if p X and
X do not subsume each other, then there must be some literal (say L)
in '(p 0
which is not in p X . But since p 0 subsumes p, there must be
an occurrence of L in p Y . The two occurrences of L, one in p 0
X and the
other in p Y , constitute a disjunctive anti-link.
Unfortunately, the presence of anti-links does not imply the presence of subsumed
paths, and hence the converse of the above theorem is not true.
3.1 Redundant Anti-links
We now identify those disjunctive anti-links which do imply the presence of subsumed
paths.
Definition 15. A disjunctive anti-link fAX ; A Y g with respect to the graph G is
redundant if either CE(AX ) 6= A or
Fast Subsumption Checks Using Anti-Links 13
Definition 16. Let fAX ; A Y g be a disjunctive anti-link in graph G, where
is the smallest full block containing the anti-link.
is the set of all d-paths of M which pass through both
and A Y or through both and AX .
Example 11. Consider the following graph
Y
A Y
The two occurrences of A form a disjunctive anti-link. Because
contains the d-path
(indicated by a line). But since CE(AX there are no paths
through is the only member of DP (fAX ; A Y g; G). The anti-
link is redundant, and p is subsumed by p (with literal set fA; Cg).
Notice that had G been embedded in a larger graph G 0 , every d-path q containing
p in G 0 would be subsumed by a corresponding d-path q 0 that differs from q only
in that q 0 contains p 0 instead of p.
In general, one or both of the literals in a redundant anti-link fAX ; A Y g is an
argument of a conjunction, and DP (fAX ; A Y In the above example,
the two occurrences of C are both arguments of disjunctions, and thus comprise a
non-redundant anti-link for which DP (fCX ; C Y
Although only redundant disjunctive anti-links contribute directly to subsumed
d-paths, non-redundant anti-links do not prohibit the existence of subsumed paths.
However, such non-redundant anti-links do not themselves provide any evidence
that such paths are in fact present.
Theorem 5. Let fAX ; A Y g be a redundant disjunctive anti-link in a semantic
graph G. Then each d-path in DP (fAX ; A Y g; G) is properly subsumed by a d-
path in G that contains the anti-link.
Proof. Recall that a d-path (c-path) in a graph G is said to pass through a sub-graph
X of G if the path when restricted to the set of nodes in X forms a d-path
(c-path) in X . Let p 2 DP (fAX ; A Y g; G), and assume without loss of generality
that p passes through both CE(AX and A Y . Note that CE(AX is
non-empty and that is the largest full block containing the anti-link.
We may write CE(AX ) as
are p restricted to X and to Y , respectively,
and p o is p restricted to nodes outside of both X and Y . By construction, AX 62 p X
and thus p X passes through some C
restricted to C i , and hence
. The d-path p 0
14 Anavai Ramesh et al.
3.2 An Anti-Link Operator
The identification of redundant disjunctive anti-links can be done easily by checking
to see if either CE(AX ) 6= AX or After identifying a redundant
anti-link, it is possible to remove it using the disjunctive anti-link dissolvent
(DADV) operator defined below; in the process, all d-paths in DP (fAX ; A Y
are eliminated, and the two occurrences of the anti-link literal are collapsed into
one.
Definition 17. Let fAX ; A Y g be a disjunctive anti-link and let
the smallest full block containing the anti-link. Then
Example 12. Consider again the semantic graph (5) from Example 11. We have
C), so the upper conjunct in DADV is
E). For the middle conjunct,
this conjunct is (B - A). Finally in the lower conjunct, DPE(AX
and false, so this reduces to C). The result is:
We point out that although DADV produces a CNF formula in the above
simple example, in general it does not. In particular, the above graph can be
simplified as the consequence of easily recognizable conditions, and the resulting
graph is not in CNF. For the details, see Case 1 of Section 3.5.
3.3 Extension and Path Complement Operators
A number of more primitive operators are used in the definition of DADV ; they are
described in (Murray and Rosenthal, 1993) and have been defined in Section 2. We
present equivalent constructive descriptions here in order to prove Lemma 6 below,
and, in the next subsection, to verify that DADV has the desired properties.
Fast Subsumption Checks Using Anti-Links 15
Proposition 2. Let G be a semantic graph and H an arbitrary subgraph. Then
false if H does not meet G
the final arc of G is a d-arc
if the final arc of G is a c-arc
true if H does not meet G
the final arc of G is a c-arc
if the final arc of G is a d-arc
G if H does not meet G
false if
the final arc of G is a d-arc
if the final arc of G is a c-arc
G if H does not meet G
true
the final arc of G is a c-arc
if the final arc of G is a d-arc
are the fundamental subgraphs of G that meet H , and F i
are those that do not.
Lemma 6. If G is a graph and A is a literal occurrence in G, then CC(A;G) is
logically equivalent to
Proof. We prove the lemma by showing that the formula on the left and the
formula on the right possess exactly the same set of d-paths; the result then follows
from Lemma 1. The proof is done via induction on the syntactic structure of G
(the lemma trivially holds if true or
1. If G is a literal, then and both the set of d-paths of CC(A;G) and the
set of d-paths of are empty. Note, that
2. If loss of generality assume A belongs to X .
Hence By the induction hypothesis, the d-
paths of CC(A;X) are just those of (DPE(A;X) \Gamma fAg)-DC(CE(A);X). So
CC(A;G) has the same d-paths as (DPE(A;X) \Gamma fAg)-DC(CE(A);X)-Y .
Now consider the right hand side of the equation. Since A is in X ,
Therefore,
be disjoint from Y , and thus
Therefore we can write the right hand side of the equation as (DPE(A;X) \Gamma
factoring out the subgraph Y we get
an equivalent subgraph having
the same d-paths. But this is just the semantic graph that has been shown to
have the same d-paths as the left hand side.
3. Finally suppose again assume that A is in X . Now there are
two subcases to consider.
a) If false and thus has no d-paths, then A in X is not d-
connected to any other subgraph in X . Hence X is of the form A-C 1 -
and A. As a result, both DC(CE(A);G)
and d-paths.
(b) If CC(A;G) 6= false, then
and thus CC(A;X) 6= false. Therefore, by the induction hypothesis,
CC(A;G) has the same d-paths as
Focusing now on the right hand side of the equation,
DPE(A;X) by definition. The c-extension of A can only include nodes
from X (otherwise, contrary to the subcase (b) condi-
tion). Therefore, . Therefore the
right hand side of the equation has the same d-paths as (DPE(A;X) \Gamma
fAg)- (DC(CE(A);X)-Y ). This is just the result obtained for the left
hand side in this subcase.
3.4 Correctness of DADV
In Theorem 6 below we show that DADV (fAX ; A Y g; G) is logically equivalent
to G and does not contain the d-paths of DP (fAX ; A Y g; G).
Theorem 6. Let be the smallest full block containing fAX ; A Y g, a
disjunctive anti-link in semantic graph G. Then DADV (fAX ; A Y g; M) is equivalent
to M and differs in d-paths from M as follows: d-paths in DP (fAX ; A Y
are not present, and any d-path of M containing the anti-link is replaced by a path
with the same literal set having only one occurrence of the anti-link literal.
Fast Subsumption Checks Using Anti-Links 17
Proof. Note that AX and A Y are literal occurrences (and hence d-blocks) in X
and in Y respectively. By the dual of Lemmas 4, X is equivalent to DC(AX ; X)-
X), and from the distributive law, M is equivalent to
Similarly, Y is equivalent to we expand the
upper occurrence of Y and distribute. Thus, M is equivalent to
By the duals of Lemmas 2 and 3, not only have we rewritten M equivalently, but
the d-paths of M have been preserved. We will continue to rewrite M ; our goal is to
eventually put it in an equivalent form in which the d-paths of DP (fAX ; A Y
have been omitted.
Consider the d-paths of DC(AX ; X) - the d-paths in X that miss AX . They
either miss CE(AX ), the c-extension of AX , or pass through CE(AX g.
Hence DC(AX ; X) has the same d-paths as
By replacing the lower occurrence of DC(AX ; X) in the previous graph, we get
the following graph M 0 which is equivalent to M and has the same d-paths as
Every d-path in the subgraph DPE((CE(AX
Theorem 5, all these paths are subsumed by other d-
paths. Therefore, we can remove the subgraph DPE((CE(AX
preserving equivalence to get the graph M 00 shown below.
Again by using arguments dual to the one given earlier for X , we have that Y and
have identical d-paths.
Replacing Y in M 00 , we find that every d-path in the subgraph DPE(AX ; X)-
Again by Theorem 5, these
paths are also subsumed by other d-paths. Therefore we can remove the subgraph
preserve equivalence; M 000 results.
The d-paths in M 000 are those of M excluding the d-paths in DP (fAX ; A Y
Consider now the d-paths of DPE(AX . They are
exactly those of M (and of M 000 ) that contain the anti-link: They each contain two
occurrences of the literal A. Hence we can remove the node A Y from
Fast Subsumption Checks Using Anti-Links 19
and apply Lemma 6 to get M 0000 .
Applying Lemma 6 to M 0000 we get DADV (fAX ; A Y
In constructing DADV (fAX ; A Y g; M)we have removed only subsumed d-paths
and altered only d-paths that contain the anti-link by collapsing the double occurrence
of the anti-link literal. Hence DADV (fAX ; A Y g; M) is equivalent to M , does
not contain the anti-link, and does not contain any d-path of DP (fAX ; A Y
Theorem 6 gives us a method to remove disjunctive anti-links and some subsumed
d-paths: Simply identify a redundant anti-link and the
smallest full block M containing it, and then replace M by DADV (H; M ). The
cost of this operation is proportional to the size of the graph replacing M , and
this is linear in M . Also, c-connected literals in M do not become d-connected in
truly new disjunctive anti-links are not introduced. Howe-
ver, parts of the graph may be duplicated, and this may give rise to additional
copies of anti-links not yet removed. Nevertheless, persistent removal of redundant
disjunctive anti-links (in which case DP (fAX ; A Y g; M) 6= ;) is a terminating
process, because the number of d-paths is strictly reduced at each step. This
proves:
Theorem 7. Finitely many applications of the DADV operation on redundant
anti-links will result in a graph without redundant disjunctive anti-links, and termination
of this process is independent of the choice of anti-link at each step.
Although we can remove all the redundant disjunctive anti-links in the graph,
this process can introduce new conjunctive anti-links. Such anti-links may indicate
the presence of subsumed d-paths, but the situation is not as favorable as with
disjunctive anti-links - see Section 3.7.
Simplifications
Obviously, DADV (fAX ; A Y g; M) can be syntactically larger than
Under certain conditions we may use simplified alternative definitions for DADV .
These definitions result in formulas which are syntactically smaller than those that
result from the general definition. The following is a list of possible simplifications.
20 Anavai Ramesh et al.
1. If
then DC(CE(AX Therefore by (possibly non atomic)
factoring on DC(AX ; X) and observing that
has the same d-paths as Y , DADV (fAX ; A Y g; M) becomes
It turns out that this rule applies to (2) in Example 1. Since CE(AX
the simplified rule for this case results in the following graph.
A
2. If
then DC(CE(AX Hence
3. If both Case 1 and Case 2 apply, then CE(AX and the above
formula simplifies to
Note that in all the above versions of DADV , the roles of X and Y can be
interchanged.
Fast Subsumption Checks Using Anti-Links 21
3.6 Disjunctive Anti-Links and Factoring
It is interesting to note that the DADV operation contains factoring (i.e., the
ordinary application of the distributive law to a pair of conjunctions containing a
common argument) as a special case. This is just the condition for Case 2 above
except that both CE(AX
A
This is the graph obtained by disjunctive factoring (Murray and Rosenthal, 1993).
The DADV operator also captures the absorption law (or merging). If AX and
A Y are both arguments of the same disjunction, then
Note, however, that technically the anti-link is not
redundant in this case.
3.7 Conjunctive Anti-Links
There are conjunctive anti-links that always indicate the presence of d-paths that
are subsumed by others, and they are easy to detect. However, the conditions
to be met are much more restrictive than those for redundant disjunctive anti-
links. Consider a conjunctive anti-link fAX ; A Y g, where the smallest full block M
containing the anti-link is (AX Every d-path in Y which passes through A Y
will be subsumed by the d-path consisting of the single literal AX . Hence we can
replace Y by
This is a kind of dual to Case 3 of the simplified versions of DADV discussed
earlier. There, the anti-link fAX ; A Y g is disjunctive and . The simplified
DADV operation just replaces Y by Note that the conjunctive
anti-link operation above removes subsumed d-paths, whereas the Case 3 disjunctive
anti-link operation can either remove paths or merely remove the second occurrence
of the anti-link literal on paths that contain the anti-link. Both operations
involve d-paths, and both have strictly dual operations that would affect c-paths
instead.
4 Complexity Considerations
The problem of eliminating all subsumed paths in a graph in an efficient manner
does not seem feasible. The following definition makes precise the notion of minimality
with respect to subsumed d-paths. Then we show that it is NP-hard to
achieve this property.
Definition 18. Let G be a semantic graph; we say that a graph G 0 is a d-minimal
equivalent of G if it satisfies the following conditions.
22 Anavai Ramesh et al.
1. G is logically equivalent to G 0 .
2. If p 0 and q 0 are two distinct d-paths in G 0 , then p 0 does not subsume q 0 and
vice versa.
3. If p 0 is a d-path in G 0 , then there is a d-path p in G such that,
4. If p is a minimal d-path in G, then there is a d-path p 0 in G 0 such that
The c-minimal equivalent of a graph is defined in the obvious dual way.
Note that Property 1 above is implied by Properties 3 and 4, and that G 0 needs
not be unique. However, the d-paths of G 0 will always include all essential (and
possibly some inessential) prime implicates of G.
Computing d-minimal equivalent graphs efficiently would be helpful for finding
prime implicates. In a d-minimal equivalent graph of a full dissolvent, subsumption
checks can be completely eliminated by Property 2 above. Hence to find the prime
implicates of G, we can find a d-minimal equivalent G 0 of the full dissolvent FD(G),
and then simply enumerate the d-paths of G 0 .
A d-minimal equivalent of a given graph G can be trivially obtained by first
enumerating all the d-paths of the given graph G and then eliminating all the
subsumed d-paths. The above algorithm is exponential in the size of G, because
G 0 is being constructed in CNF. However an NNF d-minimal equivalent G 0 of G
may be small compared to a CNF d-minimal equivalent. Even so, the problem is
NP-hard (proof follows) and hence is not likely to have an efficient algorithm.
Theorem 8. The following problem (elimination of subsumed paths) is NP-hard.
Given a graph G, find a d-minimal equivalent graph G 0 .
Proof. To show NP-hardness we reduce from satisfiability of CNF formulas. Let
C be an instance of the CNF satisfiability problem and fX be the
set of variables in C. Let A; X 0
n be distinct variables not occurring in
g. Let D be the semantic graph obtained by replacing X i by X 0
(by which we denote the NNF of the negation of C). We
construct the following semantic graph G.
A - D
Fast Subsumption Checks Using Anti-Links 23
The size of the graph G is no more than a constant factor of the size of C and can
therefore be constructed in linear time. It is easy to see that any d-path which
includes the literal A must pass through D and vice versa.
Let G 0 be any graph which is a d-minimal equivalent to G. We will show that
C is satisfiable iff the literal A occurs in G 0 .
Suppose C is satisfiable; then :C is falsifiable, and there are d-paths (in fact,
clauses, since :C is in DNF) in :C that do not contain any disjunctive link
g. All such d-paths through D do not contain any fX
at
least one such, say p, is not subsumed by another d-path through D. The d-path
pA cannot be subsumed by any other d-path in G and hence there will be a path
in G 0 which has the same literal set as pA. Hence the literal A must occur in G 0 .
If C is not satisfiable, then :C is valid. Therefore for every d-path p in D (and
hence every d-path through A), there is some i, 1 - i - n, such that the pair
of literals fX
'(p). But every such pair of literals forms a d-path in G
and hence every d-path containing A will be subsumed by another d-path in G.
Furthermore the subsuming path will not contain the literal A. By definition of
d-minimal equivalent and by construction of G 0 , no d-path in G 0 can contain the
literal A, and thus the literal A cannot occur in G 0 .
If we can solve the elimination of subsumed paths problem in polynomial time
then we have the following algorithm which can solve the satisfiability of CNF
in polynomial time: Given any instance C of the CNF satisfiability problem, we
can construct in polynomial time the graph G as shown earlier. We then find the
graph G 0 using the algorithm for elimination of subsumed paths. The size of G 0
will be polynomial in the size of G (since computing it required only polynomial
time). Now C is satisfiable iff the literal A occurs in G 0 and this check can be done
in polynomial time.
By a completely dual construction we obtain the following corollary.
Corollary 4. Given a graph G, finding a c-minimal equivalent of G is NP-hard.
We have seen that the general problem of computing d- or c-minimal graphs
is NP-hard. Nevertheless, redundant disjunctive anti-links are easily recognized,
and eliminating their corresponding subsumed d-paths can be done without direct
subsumption checks. On the other hand, recognizable subsumed d-paths due to
conjunctive anti-links are not likely to be as plentiful due to the strong restriction
defining such useful anti-links. It is also difficult to find out if an arbitrary conjunctive
anti-link results in subsumed d-paths. In fact, this problem is NP-complete.
Theorem 9. The following problem is NP-complete. Given a conjunctive anti-
link in a graph G, determine whether there are there two d-paths p X
and p Y in G, such that p X passes through AX and p Y passes through A Y and
either p X subsumes p Y or vice versa.
Proof. It is easy see that this problem is in NP. To show NP-hardness we reduce
from satisfiability of CNF formulas. Let C be an instance of the CNF satisfiability
problem and fX be the set of variables in C. Let A;
n be
distinct variables not occurring in fX g. Let D be the semantic graph
obtained by replacing X i by X 0
We construct the following
semantic graph G.
The subgraph D is a DNF formula, and A 1 and A 2 are two different occurrences
of the literal A. These two literal occurrences form a conjunctive anti-link in G.
Every d-path through A 2 contains the literal B, and only d-paths containing A 1
can possibly subsume d-paths through A 2 . The size of the graph G is no more
than a constant factor of the size of C and can therefore be constructed in linear
time.
We must show that C is satisfiable iff there is a d-path through A 1 that subsumes
another d-path through A 2 . Suppose first that C is satisfiable. Then :C is
falsifiable, and there is at least one d-path in :C that does not contain any disjunctive
link g. Therefore some d-path p through D does not contain any
of the literal pairs fX
Recall that '(p) is defined to be the literal
set of path p. It is easy to see that since '(p) does not contain such a literal pair
(corresponding to a d-link in :C), a d-path p 0 can be chosen that passes through
the n rightmost disjuncts in the lower part of G, such that '(p 0
subsumed by A 1 p.
To show the if-part, suppose there is some d-path (say p) through A 1 that
subsumes another d-path (say p 0 ) through A 2 . Then p cannot contain any literal
because no such pair occurs on any d-path in the lower part of G.
Therefore p when restricted to D will not have such a literal pair, :C has a d-path
without a d-link, and hence C is satisfiable.
Corollary 5. The problem dual to the one described in Theorem 9 involving
disjunctive anti-links and c-paths is NP-complete.
5 Some Benchmark Examples
Ngair (1993) has investigated examples that prove difficult for many proposed
prime implicate/implicant algorithms. In this section, we show that Pi
links is effective for some of these examples. For other examples from (Ngair,
1993), applying anti-link techniques appears not to produce as significant an impro-
vement. We develop an additional technique based on strictly pure full blocks that
results in a dramatic improvement for these latter examples.
Fast Subsumption Checks Using Anti-Links
In (Ngair, 1993) a class of formulas is proposed for which reliance on an intermediate
CNF form can result in an exponential increase in size and hence would be
intractable for CNF-based algorithms. Dissolution does poorly for these
examples: Although the full dissolvent can be computed quickly, a large number
of subsumption checks must be performed by Pi. It turns out, however, that in
this case the subsumed implicates correspond to easily recognizable anti-links of
both the disjunctive and conjunctive kind. We show that if these anti-links are
removed after dissolution is performed, dissolution + Pi can find all the implicates
in polynomial time.
Ngair's formulas are abbreviated with F n (n - 1) and are defined as:
A
A 2i
In the left part of Figure 1 we show the graph of F n for a fixed n.
A 3
A
A 4
A 2n
A
A 2n
A 3
A
A 4
A 2n
A
A 2n
A 3
A 4
Fig. 1. Semantic graph of Ngair's formulas before and after dissolution.
F n has 4n literals, and 2n \Gamma 2 c-links; dissolution can remove these links
by performing 2n dissolution steps. The full dissolvent that results is depicted in
the right part of Figure 1.
The structure of the full dissolvent depends on the order in which links are
selected for application of dissolution; the above dissolvent is the one obtained
by the current version of our propositional dissolution prover Dissolver. (The
26 Anavai Ramesh et al.
compact version (3) from Proposition 1 of the dissolvent is used; X is chosen to
be the smallest of the two c-blocks). We can now factor on all the occurrences
of both A 1 and A 2 in the upper right hand part of the graph and on the two
occurrences of A 1 in the lower left corner. The resulting graph is shown in Figure 2.
(Since Dissolver is NNF-based, such factoring is not only feasible but is in fact
implemented and routinely employed to produce the final output.)
A 3
A
A 4
A 2n
A
A 2n
A 3
A 4
Fig. 2. Ngair's formulas after dissolution and factoring.
The two occurrences of A 2 at the bottom left part of the graph form a redundant
disjunctive anti-link; they can be removed using the special case covered by Rule 1
for disjunctive anti-links. The two occurrences of A 1 on the left hand side of
the graph form a conjunctive anti-link and can be removed using the conjunctive
anti-link rule. This produces:
A
A 2n
A 3
A 4
By factoring on A 1 and removing the conjunctive anti-link comprised of the
two occurrences of A 2 (or by just factoring on A 1 - A 2 ), the above graph reduces
Fast Subsumption Checks Using Anti-Links 27
to the prime implicates are just fA 1 g and fA 2 g. To get this graph,
factoring and 3 anti-link operations were required - obviously polynomial
time. Hence dissolution + removal of anti-links + Pi can handle the above class
of problems in polynomial time. Perhaps the most important point is that no
subsumption checks whatsoever are required.
6 A Generalized Purity Principle
6.1 Strictly Pure Full Blocks
Recall that a full block is essentially an explicit subgraph; it is a subset of the arguments
of a conjunction or disjunction, and, via commutations and reassociations,
can in fact be made explicit.
Definition 19. A subgraph M in a graph G is pure iff all c-links or d-links that
meet M at all are totally within M . 6 If, in addition, all conjunctive or disjunctive
anti-links that meet M at all are totally within M , we say that M is strictly pure. 7
If M is a full block in G we speak of a (strictly) pure full block .
When factored, some of the examples from (Ngair, 1993) contain surprisingly
many strictly pure full blocks. Note that both factoring and recognizing strictly
pure full blocks are polynomial operations. Intuitively, such full blocks can be
replaced by single new variables, and the implicates of the resulting graph bear a
strong relationship to those of the original. Of course, the full block in question
must be satisfiable (since the new variable certainly is). At first, this may appear
to be a heavy penalty. It is not, however, because the prime implicates of the full
block itself must be computed anyway. In doing so, its satisfiability is determined
as a byproduct.
The following theorems characterize the properties of strictly pure full blocks
with respect to prime implicates. In them we employ the following notation: let
M be an explicit subgraph of a graph G and let X be a variable not occurring in
G. By G X
M we denote the graph obtained by the substitution of X for M in G.
Similarly, if D is a disjunction of literal occurrences from G we denote by DM the
disjunction of literals that occur in M and by DG\GammaM the disjunction of literals
that do not. Obviously, holds. Finally, we set
ae
DG\GammaM otherwise
Theorem 10. Let M be a satisfiable strictly pure full block in a satisfiable semantic
graph G and let D be a non-tautological disjunction of literals from G. If
DM 6= false, then the following statements are equivalent:
6 This is just the obvious generalization of the concept of a pure literal as it is used in the
literature on CNF-based automated deduction.
7 Simply put, M shares no variables with the rest of G.
28 Anavai Ramesh et al.
1. D is a prime implicate of G.
2. D X
M is a prime implicate of G X
M , and DM is a prime implicate of M .
This theorem turns out to be a special case of Theorem 11 to be proved in the
following subsection.
If a graph G contains several strictly pure full blocks M then the
repeated application of Theorem 10 provides a potentially significant speedup in
computing the prime implicates of G: Replace each strictly pure full block M i by
a new variable X n) and compute the prime implicates of the resulting
graph G X
M . Then, all substitutions of prime implicates of M i for X i in the prime
implicates of G X
M result in prime implicates of G. The speedup is potentially
dramatic: Each subsumption test performed within some M i would otherwise be
performed once for every d-path in G X
M that can be extended through M i to form a
d-path in G. Observe that prime implicates of G X
containing none of the variables
are simply prime implicates of G that do not contain literals from
any of the blocks M i .
Several distinct strictly pure full blocks can be handled by repeated application
of Theorem 10 as explained above. However, multiple occurrences M of
a single full block M in G require an extended analysis. The problem is that the
multiple occurrences themselves preclude any single M i from being strictly pure,
even if M shares no variables with the rest of G. Intuitively, we would expect that
by replacing each of the occurrences M i in G by the single new variable X , the
prime implicates of the resulting graph G X
would also bear a strong relationship
to those of G. This is made precise in the next section.
6.2 Multi-Pure Full Blocks
Definition 20. Suppose that M are occurrences of full blocks in G and
that all of them are syntactically identical (up to associativity and commutativity
of disjuncts and conjuncts). The subgraph M   formed by taking all the nodes of
the blocks M i is not necessarily a full block; 8 but let M   be strictly pure. Then
we call the M i multi-pure full blocks.
In addition, suppose that there are occurrences M n+m of full
blocks syntactically identical (up to associativity and commutativity of disjuncts
and conjuncts) to M , the NNF of the complement of any of the M i (1 - i - n). We
call complementary multi-pure full blocks.
Note that each (complementary) multi-pure full block M i is not strictly pure,
since it has anti-links (and possibly links) to its equivalent (complementary) full
blocks in G.
Observe that complementary non-atomic formulas must be recognized. For
example, if could be A - B or B - A. In fact, M could
8 As the blocks M i could be single literals occuring in arbitrary positions, this is hardly
surprising.
Fast Subsumption Checks Using Anti-Links 29
have been input as or as :(:A oe B). If NNF formulas are stored in an
appropriate canonical way, complementarity is easily (that is, in polynomial time)
detectable; the situation is also straightforward when complementary formulas
have the form M and :M prior to conversion to NNF. In any case, a detailed
treatment of this issue is beyond the scope of this paper. We do note that in
the absence of complements, multi-pure full blocks are recognizable in polynomial
time via a canonical NNF representation. A modification of any algorithm for
finding common subtrees (see (Grossi, 1993) for one such algorithm) can be used
for recognizing multi-pure full blocks.
It turns out that the results of Theorem 10 can be extended to the case in
which a formula contains complementary multi-pure full blocks. We use the notation
of Theorem 10 with the understanding that M denotes any occurrence of an
and the M are treated as negated occurrences
of M (thus G X
M replaces the complementary occurrences M j as well). M   is
defined as the subgraph of G relative to the M i and
are defined as before, but relative to M   . Additionally,
we define D X
M in the obvious way (Intuitively, we use D X
M when the literals of DM
correspond to unnegated occurrences of M , and we use D X
M when the literals in
DM correspond to negated occurrences of M ).
Theorem 11. Let M n+m be complementary
multi-pure full blocks in a satisfiable semantic graph G, where all of the
blocks M i and M j are satisfiable (we allow D be a non-tautological
disjunction of literals from G. Then the following statements are equivalent:
1. D is a prime implicate of G.
2. false and D is a prime implicate of GX
or
DM 6= false and D X
M is a prime implicate of G X
M , and DM is a prime
implicate of M
or
DM 6= false and D X
M is a prime implicate of G X
M , and DM is a prime
implicate of M .
Proof. Let G 0 X
M be a graph without c-links that is equivalent to G X
(for instance,
M could be the full dissolvent of G X
Similarly, let M 0 be a c-linkless equivalent
of M , and M 0 be a c-linkless equivalent of M . Let G 0 be the graph obtained from G
by replacing X by M 0 and X by M 0 . It is easy to see that G 0 is equivalent to G
but has no c-links. By Theorem 3, every prime implicate of G is present as a
d-path in G 0 and every prime implicate of G X
M is present as a d-path in G 0 X
M .
To prove the only-if-part, let D be a prime implicate of G. Then there must
be an unsubsumed d-path p in G 0 such that are
complementary, p can never meet (and thus pass through) both M i and M j for
any i and j.
Suppose first that p does not pass through any of the occurrences of M or M .
In this case, p must also be a d-path in G 0 X
(technically, p is isomorphic to a d-
path in G 0 X
To prove that p is not subsumed by another d-path in G 0 X
M , assume
otherwise, namely, that there is a path p 0 in G 0 X
M that subsumes p. But p 0 cannot
contain X or X, and hence would also be a d-path in G 0 that subsumes p, which
is a contradiction. Thus D is a prime implicate of G 0 X
M and hence of G X
M .
Now suppose p passes through the full blocks
be the restriction of p to M i j 0 . Notice that for 1 - j, k - q, '(p
wise, the d-path obtained by replacing p j by p k in p would subsume p. Similarly,
cannot be subsumed by another d-path in M i j 0 . Since p j is an unsubsumed d-
path in M i j 0 which is a linkless equivalent of M ,
of M . Now let p X be the d-path obtained by replacing each of the p j by X in p;
X is a d-path in G X
M . Furthermore, p X cannot be subsumed by another d-path
in G X
M (again, such a subsuming path would induce a path in G 0 that subsumes p).
Therefore D X
prime implicate of G X
M .
Finally, in the case that p passes through the full blocks
argument is similar as in the previous paragraph.
To prove the if-part, first suppose DM = false and D is a prime implicate of G X
M .
Then there is an unsubsumed d-path (say p) in G 0 X
M such that
contains neither X nor X. Thus p is an unsubsumed d-path of G 0 ,
and D is a prime implicate of G.
Now suppose that D X
M is a prime implicate of G X
M and that DM is a prime
implicate of M . Then there are unsubsumed d-paths p X in G 0 X
M and p M in M 0 ,
respectively, such that '(p X
M and '(p M respectively. In the present
subcase, by definition, D X
contains X (and cannot contain X). Let p 0 be the
result of replacing all occurrences of X in p X by p M ; p 0 is a d-path in G 0 . Since
both p M and p X are unsubsumed in G X
respectively, and since M 0 does
not share any variables with the rest of G 0 , p 0 will also be unsubsumed in G 0 .
Hence, by Theorem 3, prime implicate of G.
Similarly, if D X
M is a prime implicate of G X
M and DM is a prime implicate of M ,
then D is a prime implicate of G.
It is straightforward to see that in the case when Theorem 11
collapses into Theorem 10.
On the one hand we expect to substitute new variables for multi-pure full blocks
and achieve a savings in the computation of prime implicates comparable to that
provided by Theorem 10. But note that some complementary occurrences of M
may be c-connected; this means that such occurrences play a role in whatever
inference process is employed prior to computation of the implicates themselves. In
Fast Subsumption Checks Using Anti-Links 31
particular, we may treat them as literals and dissolve (indeed, the set of individual
links between such full blocks would satisfy the requirements of a multiple link
dissolution chain as it is defined in (Murray and Rosenthal, 1993)).
That dissolving on two complementary full blocks accomplishes exactly what
dissolving on all the corresponding single-links would is clear: All c-paths through
both full blocks are eliminated from the graph. But the former operation is much
more efficient than the latter. Therefore, recognizing such complementary full
blocks and performing inference directly on them, rather than on their constituent
literals, is desirable. Note also that for the inference phase of a prime implicate
computation, complementary full blocks do not have to be multi-pure full blocks.
This condition is necessary only for the extraction of implicates using Theorem 11
once all implicates are known to be present.
Finally, the remarks above apply also to identical full blocks if they form appropriate
non-atomic anti-links as discussed in Section 3.
6.3 More Examples
Kean & Tsiknis (1990) provide a class of examples referred in the following to
as Knm . They have mn+1 input CNF clauses and (m+1) n +mn prime implicates.
This set of clauses can be factored to obtain a more compact representation in NNF
as shown in Figure 3.
Snm
Fig. 3. Semantic graph of Kean & Tsiknis's formulas.
Since the number of prime implicates is exponential, so is the number of subsumption
checks required. The number of subsumption checks for the Ipia (de
Kleer, 1992) and Gen-Pi (Ngair, 1993) algorithms are shown in Table I.
Examples Ipia Gen-Pi Pi
K33 5166 972 164
K44 506472 11600 887
K54 1730120 29074 887


I
Number of subsumption checks needed for Kmn by
Ipia, Gen-Pi, and Pi
For each i, the literals S a full block M i , and all literals in it are
strictly pure. Let K 0
mn be the graph obtained by replacing each full block M i by
a new variable X i . By the corollary of Theorem 10, we can get the prime implicates
of Kmn from the prime implicates of K 0
mn . Since each of the subgraphs M i
has no c-links, the prime implicates of M i are present as d-paths by Theorem 3.
Since they also have no anti-links, by the contrapositive of Theorem 4, neither are
subsumption checks required to find these prime implicates. Thus the number of
subsumption checks to be done is exactly that required for computing the prime
implicates of K 0
mn , and this is significantly less than that needed for Kmn . Note
that the number of prime implicates of K 0
mn is only n. For the problems in

Table

I, we applied the above technique in combination with anti-link operations.
For
mn , the full dissolvent depends only on n and can be defined recursively. The
full dissolvent of K 0
m2 (basis) and of the general case of K 0
are shown in

Figure

4.
The number of subsumption checks required here is also shown in Table I. Cle-
arly, our techniques produce a significant reduction in the number of subsumption
checks required. Note that for the problem Kmn , the number of subsumption
checks depends only on n and not on m, and is not reduced by applying the
anti-link operations to the full dissolvent.
Our techniques are not limited to NNF formulas. They can sometimes be used
by other algorithms like Ipia and Gen-Pi which are not based on NNF formulas.
For example K 0
mn turns out to be in CNF and hence both Ipia and Gen-Pi can
handle these formulas, thereby reducing the number of subsumption checks nee-
ded. However normal forms like CNF provide very little scope for applying these
techniques directly. For example the literals S in the unfactored form of
Kmn do not form a full block. Hence one cannot apply Theorem 10. They do form
a full block after factoring. This provides stronger evidence that by avoiding less
general normal forms like CNF/DNF, one can improve the performance of prime
Fast Subsumption Checks Using Anti-Links 33
A n
A
Fig. 4. The full dissolvent of Km2 (left) and of Kmn , n ? 2 (right).
implicate algorithms.
We also note that we have implemented some of the anti-link operations presented
above in a diagnosis system introduced in (Ramesh and Murray, 1995). As
a result, we greatly increased the size of problems solvable on our system. (The
anti-link operations used were the special cases that do not increase the size of the
7 Comparison with BDDs
BDDs (Bryant, 1986) are commonly used in verification of boolean circuits. Coudert
and Madre (Coudert and Madre, 1992) describe an algorithm which produces
the prime implicates/implicants of a propositional formula represented as a BDD.
Any algorithm including theirs which uses BDDs must perform large amounts of
subsumption testing. Given any formula in NNF, a BDD based method would
first construct the BDD and then extract the prime implicates/implicants from it.
In contrast, our system would first compute the full dissolvent. But for either of
these approaches, the next stage - extracting the prime implicates/implicants -
requires extensive testing for subsumption.
The size of the BDD depends critically on the ordering (of variables) chosen.
There are classes of NNF formulas (Breitbart et al., 1990) for which any BDD
will be exponentially large in the formula size. These formulas do not have any
c-links, so the dissolution phase of our method does not change the formula. Hence
the input to Pi would be a small formula, whereas the BDD based method would
have to handle an exponentially larger intermediate representation. However these
formulas have many prime implicates and prime implicants, and the subsumption
checking is the bottleneck for both methods.
34 Anavai Ramesh et al.
In all likelyhood, the relative performance of these two methods can be determined
through experimental evaluation only; formulas will exist for which one
method is superior, and vice versa.
8 Conclusions and Future Work
We have introduced anti-links and defined useful equivalence-preserving operations
on them. These operations can be employed so as to strictly reduce the
number of d-paths in an NNF formula. Unlike path dissolution, which removes
unsatisfiable (or tautological, in the dual case) paths, anti-link operations remove
subsumed paths without any direct checks for subsumption. This is significant for
prime implicate computations, since such computations tend to be dominated by
subsumption checks.
Although prime implicate/implicant problems are intractable in general, our
techniques perform exponentially better than others on certain examples. In addi-
tion, we are able to improve performance greatly on the inherently exponential
examples of (Ngair, 1993).
Some experimental results on a dissolution- and Pi-based system for computing
prime implicates are reported in (Ramesh and Murray, 1993). That system is
currently being extended; some anti-link operations are already implemented and
have shown to improve performance. Operations based on strictly pure full blocks
are under development, and their effectiveness in practice will be tested.



--R

Hunt III

Implicit and incremental computation of primes and essential implicant primes of boolean functions.
An improved incremental algorithm for computing prime implicants.
On finding common subtrees.
Computing prime implicants.
Computing prime implicants incrementally.
An incremental method for generating prime implicants/im- plicates
Assumption based reasoning and clause management systems.


Inference with path resolution and semantic graphs.
Path dissolution: A strongly complete rule of inference.
Dissolution: Making paths vanish.
A new algorithm for incremental prime implicate generation.
An algorithm to compute circumscription.

An application of non clausal deduction in diagnosis.
On anti-links
Foundations of assumption-based truth maintenance systems: preliminary report
A new algorithm for generating prime implicants.
--TR

--CTR
A. K. Shiny , Arun K. Pujari, An Efficient Algorithm to Generate Prime Implicants, Journal of Automated Reasoning, v.22 n.2, p.149-170, February 1999
anti-links;subsumption