A New Algorithm for Incremental Prime Implicate Generation

1 Introduction

In the early 1950's, when researchers were studying various ways of minimizing boolean circuits, they discovered that the notion of prime implicant played an important role [Quine, 1952]. In particular, it was shown that the sum of prod­ ucts minimization of boolean circuits will consist of only the prime implicants of the propositional description of the cir­ cuit. Subsequently, many algorithms were proposed for the purpose of prime implicant generation [McCluskey, 1965; Slagle et al., 1970; Tison, 19671.

Recently, in an attempt to generalize the ATMS, it was re­ alized that the dual notion, prime implicate, subsumes the concept of labels calculated by an ATMS. This has lead to the study of Clause Management Systems (CMS) [Re­ iter and de Kleer, 1987] which essentially accepts a set of propositional clauses and outputs the corresponding set of prime implicates. Similar to an ATMS, the applications for a CMS include diagnosis [de Kleer and Williams, 1987; Reiter, 1987], qualitative physics [Forbus, 1990] and non­ monotonic reasoning [McCarthy, 1980; Reiter, 1980].

In this paper, we present a new algorithm for computing the prime implicates (hence, the prime implicants for the dual problem) based on a <I> operation described in the next section. The major differences between this algorithm and the existing prime implicate generation algorithms are 1. it w.J.s originally motivated entirely from the order-theoretic point of view; and 2. it allows input in a more general form: a conjunction of DNF formulas.

The latter is especially important for problem solving be­ cause the existing algorithms can only accept as input a single CNF formula (or a single DNF formula as in [Slagle et al., 1970]) which is a special case of conjunction of DNF formu­ las. These algorithms are needlessly expensive for problems that are naturally encoded by a conjunction of some com­ plex DNF formulas, because these DNF formulas need to be transformed into their CNF equivalence first. This additional step is very expensive computationally and can lead to an exponential increase in the input size. On the other hand, our new algorithm does not suffer from this shortcoming and we will present empirical results to demonstrate its superior performance. Furthermore, we will describe an application in abductive reasoning to show how its generality can be useful to problem solving.

We will adopt the following notation in the later discussion: for any DNF formula B, £(B) is the set of conjuncts in B; and for any disjunctive clause t'J, i.e. a disjunction ofnon-repetitive literals, 1? is the conjunction of the negation of literals in t'J. Furthermore, we interpret a disjunctive clause as a special case of a DNF formula, where each conjunct happens to contain a single element.

Definition: Given a set of propositional formulas e, a dis­ junctive clause t'J is called an implicate of e if e I= t'J. Fur­ thermore, it is called a prime implicate 1 if there is no other disjunctive clause t'J' such that £( t'J') c £( t'J) and e I= t'J'. A conjunctive clause 1? is called an implicant of e if t'J is an implicate of -.e. It is called a prime implicant if t'J is a prime implicate of -.e. o

By applying de Morgan's law twice, a direct consequence of the dual nature of implicate and implicant is that any algorithm which generates the prime implicates given a conjunction of DNF formulas can automatically be used to generate the prime implicants when given a disjunction of CNF formulas.

2 <I> Operation

Our new algorithm for prime implicate generation is based on order theory. In this section, we introduce the basic definitions that are relevant to this paper. First, the notion of a closure operation:

1 Our definition of prime implicate/implicant is slightly more gen­ eral than the definition used by some other authors. In particular, we allow clauses that contain complementary literals to be prime. However, one can easily derive one set from the other.

Definition: Given a lattice (L, ::::0 and a function f : L --+ L, f is called a closure operation if it satisfies the following properties:

Cl. x ::::; f( x ), for any x in L; C2. f(f(x)) = f(x); and C3. f(x)::::;J(y),ifx=:;y. 0

The significance of a closure operation lies in its images which are called fixed points. For the purpose of this paper, we need only to observe that for any x E L, f(x) t xis the smallest element in L that remains invariant under f. Hence, f(x) is said to be the least fixed point above x. The operation which leads to the new algorithm is defined below:

Definition: Given any poset (P, ::::;), a subset C ~ Pis said to be downward closed if p E C and p' ::::; p implies p' E C. Furthermore, given any subsetS ~ P, the downward closure of Sis the set 1 S = {pEP l3p' E S, p::::; p'}. o

Definition: Let (P, ::::;) be any lattice. Given any subset T E P(P) , the operation <l>r is defined on downward closed sets C E P(P) by:

where 1\ is the lattice meet operation induced by::::;. o

An important property of <l> [N gair, 1992] is:

Theorem 1 Given any <l>r 1 , · ·· , <l>r.. and any downward closed C, F = <l>r 1 o · · · o <l>r .. (C) is the least common fixed point of every <l>r,, 1 :'5 i :'5 n, above C.

3 Algorithm

Given a propositional systemS with a finite number of propo­ sitional symbols xi , x2, ... , xn . we consider the lattice P which is the power set of {xi , -.xi, ... , xn , -.xn} . Let Cp be the downward closure defined by the set {{ x;, -.xi} I 1 :'5 i :'5 n}. Note that the elements of P are ordered by the reverse of set inclusion, i.e. ::::; = :2.

Using the same terminology as in [de Kleer, 1986], we refer to elements of P as environments and P as the environment lattice of S . We interpret an environment { x;., ... , x;.} as the conjunctive clause x; 1 1\ · · · 1\ x; ·. Therefore, Cp represents the set of all inconsistent conjunctive clauses in P. Observe that the ordering on P is defined for the lattice theoretic meet operation to coincide with the logical and operation. How­ ever, bear in mind that set theoretically 1\ = U and V = n in P.

Given an environment p = {x;., .. . , x;.}, we denote its negation by p, i.e. p = -.x; 1 V · · · V -.x;.. Hence, if p is inconsistent, we have x; 1 1\ · · · 1\ x;. f=.l which implies that F= -.x; 1 V · · · -.x;., i.e. pis a tautology.

The above observation can be extended to the case when a given set of formulas 9 is assumed to be true. In particular, given any environment p, we say that pis inconsistent with e if e 1\ p f=.l. It is not difficult to see that:

Lemma 2 An. environment p is inconsistent with e if, and only if, p is an implicate of e. Furthermore, p is maximal if, and only if, p is a prime implicate.

Hence, to find the prime implicates of e, it suffices to find the maximal environments (minimal subsets) inconsistent with e. In view of the lemma, we shall also refer to such maximal environments as the negated prime implicates.

In the following, we will first discuss an operation which computes the set of environments inconsistent with e and describe later an equivalent algorithm which only generates the maximal environments. From now on, we will always assume that e is a conjunction ofDNF formulas.

Theorem 3 Given a conjunction of DNF formulas e = 8i 1\ · · ·I\ 8k, {} is an implicate of9 if, and only if, :J is an element of C~ = <I>r. o · · · o <l>r 1 ( Cp ), where T; = £( 8;) for 1 :'5 i :'5 k.

What remains to be done is to find an algorithm to compute the <l> operation. The following result tells us how:

Theorem 4 If P is an environment lattice, given any down­ ward closed C with maximal elements { Si , ... , sm} and any T = {ti , . . . , tn}. we have:

where Ej {p E P I p 1\ t i ::::; si}. Furthermore, Ej is a downward closed set with an unique least upper bound e~ = s; - ti.

For efficiency reason, we don't want to compute every el­ ement in <l>r (C) if we don't have to. In particular, during the computation of <l>r( C), we can safely ignore those elements that are already inC, because we can simply add C to there­ sulting set to obtain the desirable results. Therefore, a straight forward optimization is to ignore Ej when s;- ti = s;, because the Ej in this instance is contained entirely in C and would not have contributed any new element in the computa­ tion ofEq. (1).

Furthermore, in an actual implementation of the <l> opera­ tion, it is expensive to consider the entire downward closed set. Since we are only interested in the maximal elements . of <l>r(C), it would be desirable if we could represent ev­ ery downward closed set by their maximal elements and find equivalent operations for n and U which operate on this repre­ sentation. The following result says that this can be achieved.

Theorem 5 Given two downward closed sets A and B, let SA and S B be the maximal-element sets of A and B respectively, then

where MAX is the subsumption check operation which re­ turns the set of maximal elements of its input set.

So if we are given the maximal elements of two downward closed sets A and B, the above formulas allows us to compute the maximal elements of A n B and A U B directly. For the convenience in later discussion, we will denote the above operations as SAn SB and SA USB respectively.

For the rest of this paper, we will use the maximal elements to represent every downward closed set. In particular, the <l>r operation will operate in this representation, i.e. taking in a set of maximal elements and using the formulas in Theorem 4 and 5 for computing the corresponding output as a set of maximal elements.

From the above discussion, we obtain the following al­ gorithm for incremental calculation of the prime implicates, where S is the existing set of prime implicates:

procedure GEN-PI(S, T)

for each propositional symbol x in T

if x is not encountered earlier

then add { x, x} to S;

return «<>T(S);

end-procedure GEN-PI

Note that most of the tautological prime implicates are rep­ resented implicitly in the algorithm and are introduced only when required. This improves the efficiency of the algorithm as well as allows for potentially unbounded number of propo­ sitional symbols.

From our discussion that follows Theorem 4, we know that we can safely ignore e; in the computation of «<>T(S) when s; and t; are mutually exclusive sets. We just need to addS to the resulting set and perform subsumption check to derive the desirable results.

Example Consider the following set of clauses:

After processing the first two clauses, we obtain the following set of negated prime implicates:

By letting t, ={A,, Az} and tz = {A3, A4}, the processing of the final clause using the «<> operation is summarized in the Table 1: first, the set differences e; = s; - t i are calculated, e.g. el = s,- t, = {A, ;A3}- {A,,Az} = {A3}, and e~ is ignored because s1 and tz do not share any common element; then, we apply u to each row in the matrix to obtain MAX(U 1 <;< 6 Ej) for j = 1, 2; finally, we apply n on these results to get our new set of negated prime implicates { {A3} , {A4} }. By combining the new and the old prime implicates and performing subsumption check, the resulting list of prime implicates will be {A, V :A,, Az V Az, A3, A4}.

To help understand the «<> operation from a pure logical point of view, we map the above algorithm to the follow­ ing "resolution" rule which infers new implicates from the existing set of prime implicates and the input DNF formula:

4. Resolvent (a new implicate): V1eE -./.

From Theorem 3, 4 and 5, we can conclude that the in­ ference is sound and complete in terms of prime implicate generation. In particular, to obtain the new set of prime im­ plicates, we simply filter out from the set of new implicates those that are subsumed, i.e. remove an implicate if there ex­ ists another implicate that is a sub-clause of it.

The above resolution rule, though it appears simpler, lacks the matrix-like computational structure that is inherent in the order-theoretic approach. This is significant in terms of de­ riving an efficient algorithm for generating prime implicates.

4 Complexity and Optimization

It can be shown ([Ngair, 1992]) that starting with n prime implicates and an input disjunction of k conjuncts, the worst case complexity of computing GEN-PI is O(c * (n/k) 2 ") or O(c * n 2 ") respectively, depending on whether the input is a disjunctive clause or a more general DNF formula. Note that the complexity results for disjunctive clause coincide with those reported in [Kean and Tsiknis, 19901.

The GEN-PI algorithm as presented is not very efficient and can not be used to solve many interesting problems. Various optimization techniques have been proposed for traditional prime implicate generation algorithms [Kean and Tsiknis, 19901. Many of these techniques are equally applicable to our new algorithm. We have also discovered additional opti­ mization techniques for improving the efficiency of the GEN-PI algorithm and some of them are described below.

Consider the intersection of two maximal-element sets S, = {p,, .. . ,pm}andSz = {q,, .. . ,qn}. Asimpleminded algorithm will compute the set {p u q I p E s, , q E Sz} follow by deleting elements that are not maximal. This is an expensive 0( c * ( m * n ) 2 ) operation. Therefore, itis desirable to minimize this cost.

Lemma 6 If there exists p E S1 and q E Sz such that p j q, then s, n Sz = {q} u (S, n (Sz- {q})).

The above result says that we can remove every element from S1 and S2 that is subsumed by an element in the other list. The intersection can then be calculated by applying intersection to the two smaller lists followed by an union with the removed elements. This is beneficial since it might reduce a large number of elements that would otherwise be generated by the intersection operation, only to be discarded later.

Lemma 7 Given p E S1 and q E S2, one needs only to subsumption check p n q with respect to the set N = {p n q' I q' E Sz, q ::f; q'} u {p' n q I p' E s, , p ::f; p'}.

By viewing an intersection operation as first forming a cross product matrix between S1 and S2, the above result says that to check the maximality of each element in the matrix, it is sufficient to only compare it with elements from the same row or column. Therefore, one reduces the worst case cost of computing MAX in the intersection operation from O((ISd * ISzl?) to O((ISd + ISzl) * ISd * ISzi) . Note that the value (ISd + ISzl) * JSd * ISzl is minimum when ISd = ISzl, i.e. we have 2 * IS1I .

It is generally beneficial to compare the output of an inter­ section operation with the set S in the«<> procedure, so that no redundant element needs to be involved in further intersection operations which might otherwise generate an even larger re­ dundant set. In the following, we describe a method which helps to identify many such redundant elements.

Definition: In the «<>T operation, one computes elements of . i the form p = ej: U · · · U e;: for some 1 :::; p :::; k, such p's are called PPI (Partial Prime Implicate). The set T - {t;,, ... , t;p} is called the complement set of p. A PPI with null complement set is also known as a PI. A PPI p' is said to

Lemma 8 Given a disjunctive clause represented by T and a PPI p with complement set X, any PI q generated by p will be subsumed by S if p U X is subsumed by S.

Therefore, any PPI which satisfies the condition in the above lemma can be safely deleted without affecting the prime implicate generation process. The saving is significant be­ cause such PPI may generate many more new PPI's in the <I> operation, if it is not deleted. From empirical experience, we may eliminate as much as eighty percent of PPI's by the above optimization.

5 Comparison with existing algorithms

In this section, we compare the GEN-PI algorithm with some existing prime implicate generation algorithms, in particular, the IPIA algorithm described in [Kean and Tsiknis, 1990] and the CLTMS algorithm described in [de Kleer, 1992].2 We will compare the algorithms based on two examples 3 which represent two types of problem, one is an artificial set of clauses which is designed to produce an exponential number of prime implicates while the other is derived from more practical problems. The first example is usually referred to as the "m(x)k(y)" problem. It has two integer parameters, x, y with x * y + 1 input clauses and will produce ( x + 1 )Y + x * y (non-tautological) prime implicates:

The second example is Kean and Tsiknis's propositional en­ coding of a familiar diagnosis problem; the 5-gate adder cir­ cuit (see [Kean and Tsiknis, 1992]).

The GEN-PI and the CLTMS algorithms are both implemented in Common Lisp and run on a Sun 4/490 machine. On the other hand, the IPIA algorithm is implemented in Quintus Pro log running on a Sun Sparc-1 machine. 4 The results of the comparison are listed in Table 2 where all timing information are in seconds and PI# is the number of non-tautological prime implicates.

2 The latter algorithm is also called IPIA in the actual paper. We use CLTMS here to avoid confusion.

3 Both examples were originally proposed by Alex Kean in a series of e-mail correspondences between Alex Kean, Johan de Kleer and the author.

4 The timing information of the IPIA program was provided by Alex Kean.

Note that the CLTMS algorithm is sensitive to the input order of the clauses. This is reflected by the two-value entries for the "m3k6" and "m3k7" examples. In both the examples, input of the x * y Horn clauses are given in lexicographical order based on the two indices of s. The two values represent the times needed depending on how we prioritize the two indices.

From the results of the comparison, we can conclude that if the input is already in a CNF, the GEN-PI algorithm will perform as,efficiently as, or better than, some of the existing prime implicate generation systems. In the following, we show that the GEN-PI algorithm will greatly outperform the existing algorithms if the input is in a more general form.

6 The generality of the GEN-PI algorithm

As already emphasized earlier in this paper, the GEN-PI algo­ rithm naturally allows input formula to be a conjunction of DNF formulas. Therefore, an obvious advantage to this new algorithm is its flexibility in terms of what it can take as input, i.e. a set of DNF formulas instead of just a set of disjunctive clauses. Although a set of DNF formulas can be converted to a single CNF formula by converting each DNF formula to an equivalent CNF formula. We will show in the follow­ ing, however, that such a conversion is computationally very expensive.

Since the conversion of a DNF formula to a CNF formula is computationally equivalent to the process of coverting a CNF formula to a DNF formula (modulo a linear term), it suffices to demonstrate a particular CNF formula of length 0( n) such that any of its DNF equivalence is necessary of length exponential in n . Let us consider the DNF formula: f = (x,Vx2)1\ · · ·l\(x2n-!VX2n),whereeachx; , 1 ~ i ~ 2n, is a distinct propositional symbol. It can be shown that:

Theorem 9 Any DNF formula equivalent to the propositional formula f has at least 2" conjuncts.

Hence, the problem of converting a CNF formula to an equiv­ alent DNF formula (or vice versa) is a provably intractable problem.

Examples: The following shows some instances where DNF

formulas arise naturally in problem encoding.

1. An exclusive-or constraint, e.g. xor(x1, ... , xn). com­ monly encounter in a constraint satisfaction problem, can be intuitively encoded as a singleDNF formula (x1 A ...,x2A ···A ...,xn)V · · ·V(...,x!A ···A ...,Xn-1 Axn) but needs at least O(n 2 ) disjunctive clauses in CNF encoding. In general, it is much simpler to use a DNF encoding for a constraint describing a complete set of possible outcomes.

2. An OR-gatein a diagnostic problem, e.g. (x1 V · · .Yxn)A ...,AB( G) ~ x, can be naturally represented as a single DNF formula but needs n disjunctive clauses in CNF encoding. In the worst case, consider the "black-box" circuit shown in Figure 1. It can be encoded as a single DNF formula (...,X! A ...,x2) V · · · V ( ...,X2n-! A ...,X2n) V AB(G) V X but needs at least 2" disjunctive clauses in CNF encoding (Theorem 9).

The above results and examples tell us that the existing prime implicate generation algorithms are very inefficient be­ cause they need to perform the additional expensive oper­ ation of converting every DNF formula to a CNF formula if the input contains some DNF formulas. Such conversion also entails the possibility of enormous growth in the input size to the algorithms. Note that such additional process­ ing cost is not hidden in the GEN-PI algorithm. In particular, the algorithm treats each DNF formula as a single input with computational complexity determines roughly by the size of output. For instance, consider the following set of clauses (generalization of the example in Section 3) which produces only 2 non-tautological prime implicates, A1 and A2:

Feeding it to the prime implicate generation algorithms, we obtain the run times listed in Table 3. It is clear that GEN­ PI is the only reasonable algorithm for computing the prime implicates with such input even with reasonably small size. The poor performance of the other algorithms is due to their additional costs in converting the final input clause into 2" disjunctive clauses and processing the exponentially larger input.

A point which we have not addressed so far is the seemingly workable solution of encoding a DNF formula as a linear size CNF formula by introducing new literals. For instance, any DNF formula

can be encoded as the following set of disjunctive clauses:

where cl , ... , ck are new propositional symbols. This method does not suffer from exponential conversion cost and preserves all the prime implicates. In particular, it is not diffi­ cult to show that by filtering out the prime implicates contain­ ing the new propositional symbols from the prime implicates of the encoded problem, we obtain the prime implicates of the original problem. However, the cost of generating additional new prime implicates usually outweighs the benefit of the compact encoding. Consider the previous example that has only two non-tautological prime implicates. Using the encod­ ing method, we ended up with 3"- + 2 * n non-tautological prime implicates. Computationally, this is much more expen­ sive than just converting the DNF formula to 2" disjunctive clauses and processing them as a CNF formula. Hence, the restriction in the traditional algorithms of accepting only a CNF formula does in fact lead to a significant computational overhead in problem solving.

7 Abductive Reasoning

Abduction is a form of reasoning where given an inference system, some facts I: and a goal formula g, the reasoner finds an explanation e for g, i.e. I:Ae F g. Usually, we also require consistency in the explanation that the reasoner finds, i.e. we want I: A e to be consistent. In this section, we study a limited form of abductive reasoning where the inference system is restricted to the propositional logic and the explanation is restricted to conjunctive clause. To this end, we consider the notion of minimal support originally proposed in [Reiter and de Kleer, 1987] to solve this problem. However, the original proposal restricts the goal formula to a disjunctive clause. We will show that such a restriction is unnecessary and a much more complex class of goal formulas can be specified directly using the GEN-PI algorithm.

Definition: Given a set of propositional formulas :F and any formula Z, a disjunctive clause Y is said to be a support for Z with respect to :F iff :F ~ Y and :F F Y v Z. Y is said to be a minimal support for Z with respect to :F iff no sub-clause Y' C Y is a support for Z with respect to :F.

It is immediate that a conjunctive clause ...,y is a consistent explanation for Z in the system :F if, and only if, Y is a support for Z with respect to :F, or equivalently, there exists minimal support Y' for Z with respect to :F such that Y' ~ Y. In the following, we describe how the CZ, operation can also be used for generating minimal supports. By observing that :F ~ Y V Z if, and only if, :F 1\ ...,z ~ Y, we have:

Lemma 10 A disjunctive clause Y is a support for Z with respect to :F iffY is not an implicate of :F but is an implicate of :FA ...,z. Y is a minimal support for Z with respect to :F iff Y is not an implicate of :F but is a prime implicate of :F 1\ ...,z.

In this paper, we assume that Z is a disjunction of CNF for­ mulas, i.e . ...,z is a conjunction of DNF formulas represented by say, Tt , ... , Tn. To calculate the set of minimal supports for Z with respect to :F, we can apply «<»T 1 , ··· , «<»T .. sequen­ tially to the setS of prime implicates of :F. Subsequently, by removing elements of the resulting prime implicates that are subsumed by some elements of S, we will obtain the set of minimal supports for Z.

Since any propositional formula can be transformed into a disjunction of CNF formulas, 5 the above technique allows us to compute the set of all minimal supports for any goal formula using the GEN-PI algorithm.

Example Consider the following set of clauses:

The set of prime implicates of :F is simply the union of :F and the set of binary tautologies. To find the set of minimal supports for (Btl\ B2) V (B3/\ B4), we apply CZ,{ {B.},{B 2 }} o «<» { {BJ},{B·}} to the prime implicates of :F to get a new set of prime implicates It U h where It = {A, Bt V B2, B3 V B4}, and I2 is the set ofbinary tautologies except AVA. In this case, the set of prime implicates in It U h that are also implicates of :F is exactly h Hence, the set of minimal supports is It.

8 Conclusion

Traditional algorithms for prime implicate generation can only accept a CNF formula as their input. For problems that are naturally encoded by a conjunction of some DNF formulas, these algorithms can be needlessly expensive. This is because the transformation of the input formulas into their CNF equiv­ alence is a very expensive process and can result in a dramatic explosion of the input size.

In this paper, we studied a more general algorithm GEN-PI for prime implicate generation. The algorithm is based on a CZ, operation originally inspired by the order-theoretic study of the extended AlMS [Gunter et al., 199ll It is superior to the existing approaches in that it allows a larger class of input formulas, namely, any conjunction ofDNF formulas.

We also presented empirical comparisons between the GEN­ PI algorithm and two existing implementations that are mainly based on the generalized consensus theory [Tison, 1967]. In the more restrictive case of a CNF formula, the results show that the GEN-PI algorithm performs at least as efficiently as these algorithms, while it greatly outperforms them when the input contains some DNF formulas.

soc course, a DNF formula or a CNF formula would suffice, but disjunction of CNF formulas allows a greater flexibility and better efficiency in encoding a formula (see previous section).

The usefulness of the GEN-PI algorithm is further demon­ strated by its application in generating explanations for com­ plex formulas in a propositional abductive reasoning system.