You miss 100% of the shots you don’t take. Wayne Gretzky

Uploaded by
Wayne Gretzky

103 downloads 5409 Views 552KB Size

SAT-Based Decision Procedures for Classical Modal Logics

If you feel beautiful, then you are. Even if you don't, you still are. Terri Guillemets

Fast Orthogonal Projection Based on Kronecker Product

Every block of stone has a statue inside it and it is the task of the sculptor to discover it. Mich

nelson mandela and wits university

Ego says, "Once everything falls into place, I'll feel peace." Spirit says "Find your peace, and then

Guidelines on Closure 2007-2013

Forget safety. Live where you fear to live. Destroy your reputation. Be notorious. Rumi

Decision on Jurisdiction

Never let your sense of morals prevent you from doing what is right. Isaac Asimov

Decision on Jurisdiction

The beauty of a living thing is not the atoms that go into it, but the way those atoms are put together.

Congruence Modulo n

Forget safety. Live where you fear to live. Destroy your reputation. Be notorious. Rumi

A Fast Goal Recognition Technique Based on Interaction Estimates

It always seems impossible until it is done. Nelson Mandela

Fast Decision Procedures Based on Congruence Closure G R E G NELSON A N D DEREK C. OPPEN

Stanford Umversity, Stanford, Caly'ornia ABSTRACT, The notion of the congruence closure of a relation on a graph ~s defined and several algorithms for computing it are surveyed A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality A decision procedure ts then given for the quanufier-free theory of LISP hst structure based on the congruence closure algorithm Both decision procedures determine the satisfiability of a conjunction of hterals of length n In average time O(n log n) using the fastest known congruence closure algorithm It is also shown that ff the axtomattzatton of the theory of list structure ts changed slightly, the problem of determmmg the satisfiabihty of a conjunction of hterals becomes NP-complete The decision procedures have been unplemented m the authors' simphfier for the Stanford Pascal Verifier KEYWORDSANDPHRASES' program verification, mechanical theorem proving, decision procedure, congruence closure, graph algorithms, theory of equahty, theory of recurstve data types CRCATEGORIES 5 21, 5.24, 5 25, 5.7

1. lntroductwn Consider the p r o b l e m o f verifying that one equality is a consequence o f several o t h e r equalities, for example, t h a t f ( f ( a , b), b) = a is a consequence o f f ( a , b) = a, or, less obviously, t h a t f ( a ) = a is a c o n s e q u e n c e of f ( f ( f ( a ) ) ) ~ a and f ( f ( f ( f ( f ( a ) ) ) ) ) = a. A practical algorithm for this p r o b l e m is essential to m e c h a n i c a l p r o g r a m verification (or to any other kind o f m e c h a n i c a l reasoning), since almost all proofs require reasoning about equalities. In 1954 A c k e r m a n n [1] showed that the p r o b l e m was decidable but did not give a practical algorithm. T h e p r o b l e m appears to h a v e been ignored for the next twenty-four years. I n 1976 and 1977 several people attacked the p r o b l e m f r o m quite different points o f view. D o w n e y , Sethi, and T a r j a n [3] viewed the p r o b l e m as a variation o f the c o m m o n subexpression problem, K o z e n [4] as the w o r d p r o b l e m in fimtely presented algebras, and Shostak [81 and N e l s o n and O p p e n [51 as the decision p r o b l e m for the quantifier-free theory o f equality with uninterpreted function symbols. All these p r o b l e m s reduce to the p r o b l e m o f constructing the " c o n g r u e n c e closure" o f a relation on a graph. In Section 2 we define th,s n o t i o n and describe a c o n g r u e n c e closure algorithm which we i m p l e m e n t e d in 1976 for use in the t h e o r e m p r o v e r o f the Stanford Pascal Verifier. Its worst-case time is O(m 2) for graphs with m edges. D o w n e y , Seth1, and T a r j a n [3] describe an algorithm with worst-case time O(m logZm), which, by using a hash table, can be m a d e to run in average-case time O(m log m). W e i m p l e m e n t e d this algorithm but did not find it faster t h a n the simpler algorithm in o u r application. Permission to copy without fee all or part of this material Is granted provided that the copies are not made or distributed for &rect commercial advantage, the ACM copyright notice and the title of the publication and ItS date appear, and notice is given that copying is by permission of the Association for Computing Machinery To copy otherwise, or to republish, requires a fee and/or specific permission An earlier version of this paper appeared m the Proceedings of the 18th Annual Symposmm on FoundaUons of Computer Science, Providence, R 1, October 1977 This research was supported by the National Science Foundation under contract MCS 76-000327 and by the Fannle and John Hertz Foundation Authors' address Artificial Intelhgence Laboratory, Computer Science Department, Stanford University, Stanford, CA 94305 © 1980 ACM 0004-5411/80/0400-0356 $00 75 Journal of the AssoclaUon for Computm S Machinery, Vo| 27, No 2, Apn| 1980, pp 356-364

Fast Decision Procedures Based on Congruence Closure

357

In Section 3 we prove that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equahty with uninterpreted function symbols. Other proofs have been given by Shostak [8] and Kozen [4], but ours is simpler. In Section 4 we give a decision procedure based on congruence closure for another theory of interest in program manipulation: the quantifier-free theory of LISP list structure with uninterpreted function symbols. The axioms of this theory are CAR(CONS(x, y)) = x, CDR(CONS(x, y)) = y, -TATOM(x) 3 CONS(CAR(x), CDR(x)) = x, ~ATOM(CONS(x, y)). (Terms may contain uninterpreted function symbols, as well as the function symbols CAR, CDR, and CONS.) Using the fastest version of the congruence closure algorithm, the decision procedure requires average time O(n log n) to determine the satisfiability of a conjunction of length n. We conclude Section 4 with a curiosity: If the axlomatlzation of the theory of hst structure is altered by specifying the result of CAR and C D R on atoms, the problem of determining the satlsfiability of a conjunction becomes NP-complete. The two deosion procedures given in Sectmns 3 and 4 have been implemented m the simplifier for the Stanford Pascal Verifier. Details of how these and other deosion procedures are combined to form a simplifier are given m [6]. 2. Computing the Congruence Closure Let G = ( V, E) be a directed graph with labeled vertices, possibly with multiple edges. For a vertex v, let ?,(v) denote its label and 8(v) its outdegree, that is, the number of edges leaving v. The edges leaving a vertex are ordered. For 1 ~_ t _< 8(v), let v[i] denote the ith successor of v, that is, the vertex to which the ith edge of v points. A vertex u is apredecessor of v if v = u[i] for some i. Since multiple edges are allowed, possibly v[t] = viii for i ~ lLet n be the number of vertices of G and m the number of edges of G. We assume there are no isolated vertices and therefore that n = O(m). Let R be a relation on V. Two vertices u and v are congruent under R if ~(u) = ~(v), 8(u) = 8(v), and, for all i such that 1 _< 1 _< 8(u), (u[t], v[i]) E R. R is closed under congruences if, for all vertices u and v such that u and v are congruent under R, (u, v) E R. There is a unique minimal extension R ' of R such that R' is an equivalence relation and R ' is closed under congruences; R ' is the congruence closure of R. For example, let G be the graph shown in Figure 1 and R the relation ((V2, V3)}. The vertices V 1 and V2 are congruent under R, so the congruence closure of R must include the pairs (V2, V3) and (VI, V2). In fact, the minimal equivalence relation containing these pairs, namely the equivalence relation with associated partition {(VI, V2, V3}, {V4}), is closed under congruences and is therefore the congruence closure of R. Notice that the vertices V1, V2, V3, and V4 of G represent in a natural way the terms f ( f ( a , b), b),f(a, b), a, and b, respectively. Deducing that V1 must be equivalent to V3 in the congruence closure is analogous to d e d u c i n g f ( f ( a , b), b) = a fromf(a, b) = a by the substitutivity of equality. As a second example, let G be the graph shown in Figure 2, R the relation {(VI, V6), (V3, V6)}, and R' the congruence closure of R. Vertices V2 and V5 are congruent under R, so (V2, V5) E R'. Since R ' is closed under congruences, (VI, V4) ~ R'. The pairs (VI, V4) and (VI, V6) are both m R', so (V4, V6) E R'. Hence (V3, V5) E R'. Thus all six vertices are equivalent in the congruence closure. Essentmlly, we have proved the fact that f ( f ( f ( a ) ) ) = a and f ( f ( f ( f ( f ( a ) ) ) ) ) = a together implyf(a) = a. We now consider the problem of computing the congruence closure. We represent an eqmvalence relation by its corresponding partition, that is, by the set of its eqmvalence classes. We use two procedures for operating on the partmon: U N I O N and FIND.

358

G. NELSON AND D. C. OPPEN

(~)vl (~)v2

(~) v3 (~)v2

/\ ®v3

®v,

(~) v4 (~) v5 ® ve FIGURE 2

U N I O N ( u , v) combines the equivalence classes o f vertices u and v. F I N D ( u ) returns the u n i q u e n a m e o f the equivalence class o f vertex u. Suppose that R is a relation o n the vertices o f a g r a p h G, that R is d o s e d u n d e r congruences, and that u and v are vertices o f G. T h e following procedure M E R G E ( u , v) constructs the congruence closure o f the relation R t.J {(u, v)). MERGE(u, v)

I If FIND(u) = FIND(v), then return 2 Let P, be the set of all predecessors of all verttces equivalent to u, and Po the set of all predecessors of all vertices eqmvalent to v. 3 Call UNION(u, v) 4 For each pair (x, y) such that x ~ P, and y ~ Po, If FIND(x) ~ FIND(y) but CONGRUENT(x, y) = TRUE, then MERGE(x, y). CONGRUENT(u, v). 1 If 8(u) ~ d(v), then return FALSE 2 For 1 _

Fast Decision Procedures Based on Congruence Closure

359

PROOF. Two vertices u and v are checked for congruence only when two o f their successors are merged; this can happen at most 8(u) + 6(v) - 1 times. Thus the number of calls to C O N G R U E N T is bounded by Y, (8(u) + d(v) -- 1) = Z 8(u) + Z 8(v) -- E 1 u,v

u,v

u,v

u,o

= 2mn - n(n - 1)/2 = O(mn).

[]

CLAIM 2. The number of calls to FIND from C O N G R U E N T is bounded by O(m2), for any sequence of calls to MERGE. PROOF. Let nk be the number o f vertices with outdegree k. Each pair of vertices with outdegree k can be checked for congruence at most 2k - 1 times; each check requires at most 2k calls to FIND. Thus the total number of calls to F I N D is bounded by

~ 4k2n~ _<

2knk

= 4m 2.

[]

We associate with each equivalence class a "predecessor list" of all vertices with successors in the class. No vertex appears more than once m the predecessor list. When U N I O N combines two equivalence classes, it merges their predecessor lists into one, eliminating any duplicates, and associates the new predecessor list with the new equivalence class. With each vertex is associated a unique number from 1 to n; the predecessor lists are kept sorted by vertex number. Thus the cost of merging two predecessor lists and eliminating duplicates is proportional to the sum of their lengths. We are now ready to compute the cost of O(n) top-level calls to MERGE. Since there are only n vertices, these top-level calls can result in only n - 1 additional calls in step 4, or O(n) calls in all. There are O(n) calls to F I N D from step 1, O(mn) from step 4, and O(m 2) from C O N G R U E N T , or O(m 2) calls in all. There are no more than n - 1 calls to UNION. In the fast implementation of U N I O N and F I N D analyzed in [9], U N I O N takes constant time and O(m 2) calls to F I N D take O(m 2) time. The total cost of splicing predecessor lists is O(n2). Thus, the asymptotic worst-case time for O(n) merges is O(m2). The double loop used in step 4 to find new congruent pairs is not very sophisticated. If the set of predecessors of the two vertices is lexicographically sorted on the sequences of their successors' equivalence classes, then congruent vertices will be adjacent in the sorted list. The cost of finding all new congruent pairs is proportional to the sum of the lengths of the predecessor lists mstead of to the product. If step 4 is changed in this way, the time bound for the algorithm becomes O(mn). In the sophisticated algorithm of Downey, Sethi, and Tarjan [3], the vertices are kept in a hash table keyed by the list of equivalence classes of their successors. Step 4 can be implemented so that only the vertices in the shorter predecessor list need be rehashed. The average Ume for O(n) merges using their algorithm is O(m log m). We have implemented both the O(m 2) and the O(m log m) algorithms. The more sophisticated algorithm is not faster for our applications. The reason is that the predecessor lists are short, so that the double loop runs at about the same speed as in the more sophisticated method.

3. The Quantifier-Free Theory of Equality In this section, we show how the decision problem for the quantifier-free theory of equality with uninterpreted function symbols reduces to the congruence closure problem. The language of the quantifier-free theory of equality consists of variables, unmterpreted function symbols, the usual Boolean connectives, and the predicate =. An example of a formula m the theory is x = y D fix) = fly). To determine the validity of a formula, it suffices to determme the unsatisfiability of the disjunctive normal form of its negation.

360

G. NELSON AND D. C. OPPEN

The disjunction is unsatisfiable if and only if each of its disjuncts is unsatisfiable, so it suffices to describe an algorithm for determining the satisfiability of conjunctions of literals. DECISION PROCEDLrRE. This algorithm determines the satisfiability of the conjunction of equalities and disequalities tx = ul A . . . A tp -- Up A rl # sl A . . . A rq # Sq.

1 Construct a graph G which corresponds to the set of all terms appearing m the conjunction For each term t appearing m the conJunction, let ¢(0 be the vertex m G representing t Let R be the ldenUty relation on the verttces of G 2 For 1 _*
*

The congruence closure algorithm forms the basis for a fast deciston procedure for determining satisfiability in the quantifier-free theory of list structure with unmterpreted function symbols. The language of this theory is the language of the quantifier-free theory of equahty plus distinguished function symbols CAR, CDR, and CONS and predicate symbol ATOM, satisfying the following axioms: CAR(CONS(x, y)) ffi x, CDR(CONS(x, y)) = y, --ATOM(x) D CONS(CAR(x), CDR(x)) = x, --ATOM(CONS(x, y)).

(1)

CAR, CDR, CONS, and A T O M are the well-known functions and predicates of LISP. An example of a theorem m this theory is CAR(x) = CAR(y) A CDR(x) -- C D R ( y ) A --ATOM(x) A ~ A T O M ( y ) Dr(x) = f l y ) . Notice that we do not restrict the domain of the LISP functions to noncircular lists, so that a formula like CAR(x) = x is satisfiable. If we include axioms enforcing acyclicity of hst structure (as in Pure LISP) and exclude uninterpreted function symbols, a faster algorithm is possible than the one described here. Oppen [7] describes a decision procedure which

Fast Decision Procedures Based on Congruence Closure

361

determines the saUsfiabihty of conjunctions over the quantifier-free theory of (pure) LISP in linear time. The algorithm represents terms by vertices in a directed graph as in Section 3. The basic idea of the decision procedure is to add all relevant instances of axiom schema (1) to this graph. For each term CONS(x, y) represented in the graph, we will add the equalities x = CAR(CONS(x, y)) and y = CDR(CONS(x, y)) to the graph. We assume that each literal ATOM(t) appearing negatively has been eliminated from the conjunction and replaced by an equality t = CONS(u, v), where u and v are variables appeanng nowhere else in the formula. Therefore, the only literals involving A T O M are positive. DECISION PROCEDURE. This algorithm determines the satisfiability of a conjunction F of the form ATOM(u1) A ATOM(u2) A . . . A ATOM(uq) A 111 " ~ W l A ° • • A V r "~" W r A

xl#ylA...Ax~#y~, where the terms in the literals may contain uninterpreted function symbols as well as the functions CAR, CDR, and CONS. 1 Constructa graph G which corresponds to the set of all terms appeanng in the conjunction For each term t appeanng m the conjunctton,let ~-(t)be the vertex m G representingt For ! <_z~ r, call MERGE(¢(v,),¢(w,)) 2 For each vertex u in G labeledCONS, add verticesv, labeledCAR, and w, labeledCDR, both with ontdegree i, such that v[l] = will = u Call MERGE(v, u[i]) and MERGE(w, u[2]) (That is, given a term CONS(x, y), add verttces representingCAR(CONS(x,y)) and CDR(CONS(x, y)) and merge them with the vertices representingx and y ) 3 For zfrom 1 to s, tf ~-(x,)is equivalentto ~-(y,),return UNSATISFIABLEFor t from 1 to q, If the eqmvalence class of t-(u,)containsa vertex labeledCONS, return UNSATISFIABLE Otherwise,return SATISFIABLE If the length of the formula F is n, the size of G after step 2 is O(n). The average time required by this decision procedure to determine the satisfiability of a conjunction of literals is therefore O(n log n) using the fast congruence closure algorithm. PROOF OF CORRECTNESS. It is straightforward to verify that the algorithm is correct if it returns UNSATISFIABLE. Suppose that it returns SATISFIABLE; we construct an interpretation satisfying F. Let So be the partition of the vertices of G corresponding to the final equivalence relation. We define two functions CAR0 and CDR0 from So to So, and a function CONS0 from a subset of So × So to So. If the equivalence class Q contains a vertex v with a predecessor u labeled CAR, then CARo(Q) is the equivalence class of u; otherwise CARo(Q) is arbitrary. If Q contains a vertex v with a predecessor u labeled CDR, then CDRo(Q) is the equivalence class of u; otherwise CDRo(Q) is arbitrary. The pair (Q1, Q2) is in the domain of CONSo only if there exists a vertex v labeled CONS such that v[l] E Q1 and v[2] E Q2; in this case CONSo(Q1, Q2) is the equivalence class of v. Note that CARo, CDRo, and CONS0 are well defmed because the graph is closed under congruences. Unfortunately, CONSo is not a total function. To construct an interpretation, we must extend CONS0 to be defined on all of So x So. We first extend it to a function CONS1 which agrees with CONSo where CONS0 is defined, and otherwise just returns the ordered pair of its arguments. Since CONS1 returns elements of So x So, the range So of the interpretation must be extended to a set $1 that includes both So and part of So x So. But then CONS~ is not total and must be extended so that it is defined on all of S~ x S~. To construct an interpretation we repeat this extension step infinitely many times. More precisely, suppose that we have defined the first i + 1 quadruples in the infinite sequence (So, CONSo, CAR0, CDRo), (Sx, CONS1, CAR1, CDR1), . . . , (S,, CONS,, CAR,, CDR3 . . . . . We define the next quadruple (S,+l, CONS,+1, CAR,+~, CDR,+0 by the following rules.

362

G. NELSON AND D. C. OPPEN

Let D, be the domain o f CONS,. (1) S,+l = S, U St X St - Dr.

(2) The domain of CONS,+i is St x S,. CONS,+i(x, y) = CONS,(x, y) if (x, y) is in the domain of CONS,; CONSt+i(x, y) = (x, y) otherwise. (3) CAR,+i(x) -- CAR,(x) if x E St. Otherwise x ~ S, x S, - D, and is thus an ordered pair (y, z); in this case define CAR,+~(x) = y. (4) CDRt+~(x) = CDR,(x) i f x E S,. Otherwise x ~ S, x S, - Dt and is thus an ordered pair (y, z); in this case define C D R , + i ( x ) = 2. We now show that, for each i, CARt, CDRt, and CONS, have the following two properties. (1) If (x, y) is in the domain of CONS,, then CAR,(CONS,(x, y)) = x and C D R , ( C O N S , ( x , y)) = y.

(2) I f x is m the range of CONS,, then (CAR,(x), CDR,(x)) is in the domain of CONS,, and CONSt(CARt(x), CDR,(x)) = x. Consider first the base case, when i = 0 and x and y are eqmvalence classes. If (x, y) is in the domain of CONS0, then there is a vertex u with h(u) = CONS, u[l] E x, and u[2] E y. Since u is a CONS, two vertices v and w labeled C A R and CDR, respectively, were added as predecessors of u. The vertices v and w satisfy the requirements of the definitions of CAR0 and CDR0, so CAR0(CONS0(x, y)) is the equivalence class of v and CDRo(CONS0(x, y)) is the equivalence class of w. Furthermore the pairs (v, u[1]) and (w, u[2]) were added to R in step 2, so v and w are in the equivalence classes x and y, respectively. The proof that CARo, CDRo, and CONSo have the second property is similar. Suppose now that CONS,, CAR,, and CDR, satisfy properties 1 and 2. If (x, y) is in the domain of CONS,, then CONSt+~(x, y) = CONS,(x, y); at follows that CARt+i(CONS,+i(x, y)) = CARt(CONS,(x, y)) = x and CDR,+~(CONSt+i(x, y)) = C D R , ( C O N S , ( x , y)) = y by the induction hypothesis. Otherwase, CONS,+~(x, y) as the ordered pair (x, y), and CARt+i(CONSt+i(x, y)) = x and CDR,+~(CONS,+~(x, y)) = y by definition. A similar argument shows that CONS,+1, CARt+l, and CDR,+i satisfy property 2. It follows by reduction that, for all i, the functions CARt, CDR,, and CONS, have the two properties. Let S' be the union of all the St. Let CAR'(x) be CAR,(x) for the first i such that x E S,. Let C D R ' and C O N S ' be defined similarly. It follows that CAR', CDR', and C O N S ' have properUes 1 and 2 and that CONS' is defined on all of S' x S'. We are finally ready to define an interpretation xk satisfying F. The range of tk is S'. interprets CAR, CDR, and CONS as CAR', CDR', and CONS'. An element of S ' is anterpreted to be nonatomic if and only if it is in the range of CONS'. If f is an uninterpreted function symbol, Q~. . . . . Qk are m S, and there exists a vertex v such that ~(v) = f, 8(0 = k, and v[i] E Q, for each i from 1 to k, then 6(f)(Q~ . . . . . Qk) is the eqmvalence class of v. If this definition does not determine the value of ~/(f), then the value is arbitrary. It follows from properties 1 and 2 and the fact that the set of nonatoms is exactly the range of CONS' that this interpretauon satisfies axiom schema (2). It remains to show that ~ksatisfies F. It is straightforward to show that for each term t in the original formula, ~ 0 is the equivalence class of z(t). But "r(vt) and ,(w,) have been merged for each i from 1 to r, so tk satisfies the equalities in F. "r(xt) and ~'(Y3 are in different eqmvalence classes (since step 3 returned SATISFIABLE), so tk satisfies the dasequalities in F. Finally, no equivalence class of any ,(u,) contains a node labeled CONS; hence these classes are not m the range of CONSo. They are certainly not in the range of any of the other functions CONS,, so they are interpreted as atoms by ~k. Hence tk satisfies F. This completes the proof of correctness of the decision procedure.

Fast Decision Procedures Based on Congruence Closure

363

Somewhat surprisingly, when the result o f a selector function on an atom is specified by the axioms, the problem of determining the satisfiability of a conjunction o f literals becomes NP-complete. Consider the following axioms for the theory of CAR, CDR, and CONS with the single atom NIL: CAR(CONS(X, Y)) = X, CDR(CONS(X, Y ) ) = Y, X # N I L D CONS(CAR(X), CDR(X)) = X, CONS(X, Y) # NIL, CAR(NIL) = CDR(NIL) = NIL. We show that the problem of determining the satisfiability in this theory o f a conjunction of equalities and disequahties between terms containing CAR, CDR, CONS, NIL, and uninterpreted function signs is NP-complete. It is straightforward to show that the problem is in NP, since a nondeterministic program can guess the equivalence relaUon on the set of terms in the conjunction and then check that the equivalence relation does not violate any of the above axioms or the substitutivity of equality. To show that the problem is NP-hard, we will reduce the 3-CNF satisfiability problem for propositional calculus to it. (See [2].) Let P1. . . . . Pn be propositional variables and F a conjunction of three-element clauses over the P,. We construct a conjunction G of equalities and disequalities between liststructure terms involving CAR, CDR, CONS, NIL, and the 2n variables X1, Y~. . . . . Xn, Yn such that G is satisfiable if and only if F is. The first part of G is CAR(X1) = CAR(Y1)/~ CDR(X~) = CDR(Y1)/k X~ # Y1 A CAR(X2) = CAR(Y2) A CDR(X2) = CDR(Y2) A X2 # Y2 A :

(2)

CAR(Xn) = CAR(Yn) A CDR(X~) = CDR(Yn) A Xn # Yn. For no t can X, and Y, both be non-NIL, smce then X, and Y, would be equal by the third axiom and the substitutwity of equality. One of them must be N I L and the other CONS(NIL, NIL). Given an interpretation ~pfor G, we construct an interpretation ¢pfor F by defining dr(P,) to be T R U E if and only if ~p(X,) = NIL. The remaining conjuncts in G guarantee that ~p satisfies G if and only if th satisfies F. We demonstrate the construction with an example. If one of the clauses of F is Pt ~/ -~P2 W Pa, we want to add a conjunct to G which is eqmvalent to (Xl = N I L V X2 # N I L V X3 = NIL). In light of (2), this is eqmvalent to

-1(Y2 = NIL A X2 = N I L / ~ Y3 = NIL), or to the single hteral CONS(Yz, CONS(X2, Y3)) # CONS(NIL, CONS(NIL, NIL)). Note that we have shown the problem is NP-hard even without uninterpreted function symbols. A simdar construcUon can be used whenever the result of a selector function on an atom Is specified. The problem ts also NP-complete with the axiomatizatlon (1) if predicates are interpreted as Boolean-valued funcuons and literals such as F(ATOM(x)) # F(ATOM(y)) are allowed. ACKNOWLEDGMENT. We are indebted to Bob Tarjan for many helpful discussions. REFERENCES l, ACKERMANN,W Solvable Cases of the Dectston Problem North-Holland, Amsterdam, 1954 2 AHO, A V, HOPCROFT, J E, AND ULLMANN, J D The Destgn and Analysts of Computer Algortthms Addison-Wesley, Reading, Mass 1974

364

G. NELSON AND D. C. OPPEN

3. DOWNEY,P. J, SETHI, R , ANDTARTAN,R E. Var,ations on the common subexpresslon problem To appear m £ ACM.

4. KOZEN, D. Complexity of finitely represented algebras. Proc. 9th Annual ACM Symp. on Theory of Comptg., Boulder, Colo., May 1977, pp. 164-177. 5. NE~ON, C G., AND OPPEN, D. C Fast decision procedures based on UNION and'FIND. Proc Eighteenth Annual Syrup on Foundations of Comptr. Scl, Providence, R 1., 1977 (This is an earher version of the present paper.) 6 NELSON,C G., AND OPPEN, D. C Stmphfication by cooperating decision procedures To be pubhshed 70PPEN, D C. Reasoning about recurstvely defined data structures Proc 5th ACM Symp on Prmctples of Programming Languages, Tucson, ADz, January 1978, pp 151-157 8. SHOSTAK,R An algorithm for reasoning about equality Comm ACM 21, 7 (July 1978), 583-585 9 TARIAN,R. E Efficiency of a good but not linear set umon algorithm J ACM 22, 2 (April 1975), 215-225 RECEIVED JUNE

1978,

REVISED APRIL

1979,

ACCEPTED APRIL 1979

Journal of the Assoclat*on for Computing Machinery Vol 27, No 2, Aprd 1980

Stanford Umversity, Stanford, Caly'ornia ABSTRACT, The notion of the congruence closure of a relation on a graph ~s defined and several algorithms for computing it are surveyed A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality A decision procedure ts then given for the quanufier-free theory of LISP hst structure based on the congruence closure algorithm Both decision procedures determine the satisfiability of a conjunction of hterals of length n In average time O(n log n) using the fastest known congruence closure algorithm It is also shown that ff the axtomattzatton of the theory of list structure ts changed slightly, the problem of determmmg the satisfiabihty of a conjunction of hterals becomes NP-complete The decision procedures have been unplemented m the authors' simphfier for the Stanford Pascal Verifier KEYWORDSANDPHRASES' program verification, mechanical theorem proving, decision procedure, congruence closure, graph algorithms, theory of equahty, theory of recurstve data types CRCATEGORIES 5 21, 5.24, 5 25, 5.7

1. lntroductwn Consider the p r o b l e m o f verifying that one equality is a consequence o f several o t h e r equalities, for example, t h a t f ( f ( a , b), b) = a is a consequence o f f ( a , b) = a, or, less obviously, t h a t f ( a ) = a is a c o n s e q u e n c e of f ( f ( f ( a ) ) ) ~ a and f ( f ( f ( f ( f ( a ) ) ) ) ) = a. A practical algorithm for this p r o b l e m is essential to m e c h a n i c a l p r o g r a m verification (or to any other kind o f m e c h a n i c a l reasoning), since almost all proofs require reasoning about equalities. In 1954 A c k e r m a n n [1] showed that the p r o b l e m was decidable but did not give a practical algorithm. T h e p r o b l e m appears to h a v e been ignored for the next twenty-four years. I n 1976 and 1977 several people attacked the p r o b l e m f r o m quite different points o f view. D o w n e y , Sethi, and T a r j a n [3] viewed the p r o b l e m as a variation o f the c o m m o n subexpression problem, K o z e n [4] as the w o r d p r o b l e m in fimtely presented algebras, and Shostak [81 and N e l s o n and O p p e n [51 as the decision p r o b l e m for the quantifier-free theory o f equality with uninterpreted function symbols. All these p r o b l e m s reduce to the p r o b l e m o f constructing the " c o n g r u e n c e closure" o f a relation on a graph. In Section 2 we define th,s n o t i o n and describe a c o n g r u e n c e closure algorithm which we i m p l e m e n t e d in 1976 for use in the t h e o r e m p r o v e r o f the Stanford Pascal Verifier. Its worst-case time is O(m 2) for graphs with m edges. D o w n e y , Seth1, and T a r j a n [3] describe an algorithm with worst-case time O(m logZm), which, by using a hash table, can be m a d e to run in average-case time O(m log m). W e i m p l e m e n t e d this algorithm but did not find it faster t h a n the simpler algorithm in o u r application. Permission to copy without fee all or part of this material Is granted provided that the copies are not made or distributed for &rect commercial advantage, the ACM copyright notice and the title of the publication and ItS date appear, and notice is given that copying is by permission of the Association for Computing Machinery To copy otherwise, or to republish, requires a fee and/or specific permission An earlier version of this paper appeared m the Proceedings of the 18th Annual Symposmm on FoundaUons of Computer Science, Providence, R 1, October 1977 This research was supported by the National Science Foundation under contract MCS 76-000327 and by the Fannle and John Hertz Foundation Authors' address Artificial Intelhgence Laboratory, Computer Science Department, Stanford University, Stanford, CA 94305 © 1980 ACM 0004-5411/80/0400-0356 $00 75 Journal of the AssoclaUon for Computm S Machinery, Vo| 27, No 2, Apn| 1980, pp 356-364

Fast Decision Procedures Based on Congruence Closure

357

In Section 3 we prove that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equahty with uninterpreted function symbols. Other proofs have been given by Shostak [8] and Kozen [4], but ours is simpler. In Section 4 we give a decision procedure based on congruence closure for another theory of interest in program manipulation: the quantifier-free theory of LISP list structure with uninterpreted function symbols. The axioms of this theory are CAR(CONS(x, y)) = x, CDR(CONS(x, y)) = y, -TATOM(x) 3 CONS(CAR(x), CDR(x)) = x, ~ATOM(CONS(x, y)). (Terms may contain uninterpreted function symbols, as well as the function symbols CAR, CDR, and CONS.) Using the fastest version of the congruence closure algorithm, the decision procedure requires average time O(n log n) to determine the satisfiability of a conjunction of length n. We conclude Section 4 with a curiosity: If the axlomatlzation of the theory of hst structure is altered by specifying the result of CAR and C D R on atoms, the problem of determining the satlsfiability of a conjunction becomes NP-complete. The two deosion procedures given in Sectmns 3 and 4 have been implemented m the simplifier for the Stanford Pascal Verifier. Details of how these and other deosion procedures are combined to form a simplifier are given m [6]. 2. Computing the Congruence Closure Let G = ( V, E) be a directed graph with labeled vertices, possibly with multiple edges. For a vertex v, let ?,(v) denote its label and 8(v) its outdegree, that is, the number of edges leaving v. The edges leaving a vertex are ordered. For 1 ~_ t _< 8(v), let v[i] denote the ith successor of v, that is, the vertex to which the ith edge of v points. A vertex u is apredecessor of v if v = u[i] for some i. Since multiple edges are allowed, possibly v[t] = viii for i ~ lLet n be the number of vertices of G and m the number of edges of G. We assume there are no isolated vertices and therefore that n = O(m). Let R be a relation on V. Two vertices u and v are congruent under R if ~(u) = ~(v), 8(u) = 8(v), and, for all i such that 1 _< 1 _< 8(u), (u[t], v[i]) E R. R is closed under congruences if, for all vertices u and v such that u and v are congruent under R, (u, v) E R. There is a unique minimal extension R ' of R such that R' is an equivalence relation and R ' is closed under congruences; R ' is the congruence closure of R. For example, let G be the graph shown in Figure 1 and R the relation ((V2, V3)}. The vertices V 1 and V2 are congruent under R, so the congruence closure of R must include the pairs (V2, V3) and (VI, V2). In fact, the minimal equivalence relation containing these pairs, namely the equivalence relation with associated partition {(VI, V2, V3}, {V4}), is closed under congruences and is therefore the congruence closure of R. Notice that the vertices V1, V2, V3, and V4 of G represent in a natural way the terms f ( f ( a , b), b),f(a, b), a, and b, respectively. Deducing that V1 must be equivalent to V3 in the congruence closure is analogous to d e d u c i n g f ( f ( a , b), b) = a fromf(a, b) = a by the substitutivity of equality. As a second example, let G be the graph shown in Figure 2, R the relation {(VI, V6), (V3, V6)}, and R' the congruence closure of R. Vertices V2 and V5 are congruent under R, so (V2, V5) E R'. Since R ' is closed under congruences, (VI, V4) ~ R'. The pairs (VI, V4) and (VI, V6) are both m R', so (V4, V6) E R'. Hence (V3, V5) E R'. Thus all six vertices are equivalent in the congruence closure. Essentmlly, we have proved the fact that f ( f ( f ( a ) ) ) = a and f ( f ( f ( f ( f ( a ) ) ) ) ) = a together implyf(a) = a. We now consider the problem of computing the congruence closure. We represent an eqmvalence relation by its corresponding partition, that is, by the set of its eqmvalence classes. We use two procedures for operating on the partmon: U N I O N and FIND.

358

G. NELSON AND D. C. OPPEN

(~)vl (~)v2

(~) v3 (~)v2

/\ ®v3

®v,

(~) v4 (~) v5 ® ve FIGURE 2

U N I O N ( u , v) combines the equivalence classes o f vertices u and v. F I N D ( u ) returns the u n i q u e n a m e o f the equivalence class o f vertex u. Suppose that R is a relation o n the vertices o f a g r a p h G, that R is d o s e d u n d e r congruences, and that u and v are vertices o f G. T h e following procedure M E R G E ( u , v) constructs the congruence closure o f the relation R t.J {(u, v)). MERGE(u, v)

I If FIND(u) = FIND(v), then return 2 Let P, be the set of all predecessors of all verttces equivalent to u, and Po the set of all predecessors of all vertices eqmvalent to v. 3 Call UNION(u, v) 4 For each pair (x, y) such that x ~ P, and y ~ Po, If FIND(x) ~ FIND(y) but CONGRUENT(x, y) = TRUE, then MERGE(x, y). CONGRUENT(u, v). 1 If 8(u) ~ d(v), then return FALSE 2 For 1 _

Fast Decision Procedures Based on Congruence Closure

359

PROOF. Two vertices u and v are checked for congruence only when two o f their successors are merged; this can happen at most 8(u) + 6(v) - 1 times. Thus the number of calls to C O N G R U E N T is bounded by Y, (8(u) + d(v) -- 1) = Z 8(u) + Z 8(v) -- E 1 u,v

u,v

u,v

u,o

= 2mn - n(n - 1)/2 = O(mn).

[]

CLAIM 2. The number of calls to FIND from C O N G R U E N T is bounded by O(m2), for any sequence of calls to MERGE. PROOF. Let nk be the number o f vertices with outdegree k. Each pair of vertices with outdegree k can be checked for congruence at most 2k - 1 times; each check requires at most 2k calls to FIND. Thus the total number of calls to F I N D is bounded by

~ 4k2n~ _<

2knk

= 4m 2.

[]

We associate with each equivalence class a "predecessor list" of all vertices with successors in the class. No vertex appears more than once m the predecessor list. When U N I O N combines two equivalence classes, it merges their predecessor lists into one, eliminating any duplicates, and associates the new predecessor list with the new equivalence class. With each vertex is associated a unique number from 1 to n; the predecessor lists are kept sorted by vertex number. Thus the cost of merging two predecessor lists and eliminating duplicates is proportional to the sum of their lengths. We are now ready to compute the cost of O(n) top-level calls to MERGE. Since there are only n vertices, these top-level calls can result in only n - 1 additional calls in step 4, or O(n) calls in all. There are O(n) calls to F I N D from step 1, O(mn) from step 4, and O(m 2) from C O N G R U E N T , or O(m 2) calls in all. There are no more than n - 1 calls to UNION. In the fast implementation of U N I O N and F I N D analyzed in [9], U N I O N takes constant time and O(m 2) calls to F I N D take O(m 2) time. The total cost of splicing predecessor lists is O(n2). Thus, the asymptotic worst-case time for O(n) merges is O(m2). The double loop used in step 4 to find new congruent pairs is not very sophisticated. If the set of predecessors of the two vertices is lexicographically sorted on the sequences of their successors' equivalence classes, then congruent vertices will be adjacent in the sorted list. The cost of finding all new congruent pairs is proportional to the sum of the lengths of the predecessor lists mstead of to the product. If step 4 is changed in this way, the time bound for the algorithm becomes O(mn). In the sophisticated algorithm of Downey, Sethi, and Tarjan [3], the vertices are kept in a hash table keyed by the list of equivalence classes of their successors. Step 4 can be implemented so that only the vertices in the shorter predecessor list need be rehashed. The average Ume for O(n) merges using their algorithm is O(m log m). We have implemented both the O(m 2) and the O(m log m) algorithms. The more sophisticated algorithm is not faster for our applications. The reason is that the predecessor lists are short, so that the double loop runs at about the same speed as in the more sophisticated method.

3. The Quantifier-Free Theory of Equality In this section, we show how the decision problem for the quantifier-free theory of equality with uninterpreted function symbols reduces to the congruence closure problem. The language of the quantifier-free theory of equality consists of variables, unmterpreted function symbols, the usual Boolean connectives, and the predicate =. An example of a formula m the theory is x = y D fix) = fly). To determine the validity of a formula, it suffices to determme the unsatisfiability of the disjunctive normal form of its negation.

360

G. NELSON AND D. C. OPPEN

The disjunction is unsatisfiable if and only if each of its disjuncts is unsatisfiable, so it suffices to describe an algorithm for determining the satisfiability of conjunctions of literals. DECISION PROCEDLrRE. This algorithm determines the satisfiability of the conjunction of equalities and disequalities tx = ul A . . . A tp -- Up A rl # sl A . . . A rq # Sq.

1 Construct a graph G which corresponds to the set of all terms appearing m the conjunction For each term t appearing m the conJunction, let ¢(0 be the vertex m G representing t Let R be the ldenUty relation on the verttces of G 2 For 1 _

The congruence closure algorithm forms the basis for a fast deciston procedure for determining satisfiability in the quantifier-free theory of list structure with unmterpreted function symbols. The language of this theory is the language of the quantifier-free theory of equahty plus distinguished function symbols CAR, CDR, and CONS and predicate symbol ATOM, satisfying the following axioms: CAR(CONS(x, y)) ffi x, CDR(CONS(x, y)) = y, --ATOM(x) D CONS(CAR(x), CDR(x)) = x, --ATOM(CONS(x, y)).

(1)

CAR, CDR, CONS, and A T O M are the well-known functions and predicates of LISP. An example of a theorem m this theory is CAR(x) = CAR(y) A CDR(x) -- C D R ( y ) A --ATOM(x) A ~ A T O M ( y ) Dr(x) = f l y ) . Notice that we do not restrict the domain of the LISP functions to noncircular lists, so that a formula like CAR(x) = x is satisfiable. If we include axioms enforcing acyclicity of hst structure (as in Pure LISP) and exclude uninterpreted function symbols, a faster algorithm is possible than the one described here. Oppen [7] describes a decision procedure which

Fast Decision Procedures Based on Congruence Closure

361

determines the saUsfiabihty of conjunctions over the quantifier-free theory of (pure) LISP in linear time. The algorithm represents terms by vertices in a directed graph as in Section 3. The basic idea of the decision procedure is to add all relevant instances of axiom schema (1) to this graph. For each term CONS(x, y) represented in the graph, we will add the equalities x = CAR(CONS(x, y)) and y = CDR(CONS(x, y)) to the graph. We assume that each literal ATOM(t) appearing negatively has been eliminated from the conjunction and replaced by an equality t = CONS(u, v), where u and v are variables appeanng nowhere else in the formula. Therefore, the only literals involving A T O M are positive. DECISION PROCEDURE. This algorithm determines the satisfiability of a conjunction F of the form ATOM(u1) A ATOM(u2) A . . . A ATOM(uq) A 111 " ~ W l A ° • • A V r "~" W r A

xl#ylA...Ax~#y~, where the terms in the literals may contain uninterpreted function symbols as well as the functions CAR, CDR, and CONS. 1 Constructa graph G which corresponds to the set of all terms appeanng in the conjunction For each term t appeanng m the conjunctton,let ~-(t)be the vertex m G representingt For ! <_z~ r, call MERGE(¢(v,),¢(w,)) 2 For each vertex u in G labeledCONS, add verticesv, labeledCAR, and w, labeledCDR, both with ontdegree i, such that v[l] = will = u Call MERGE(v, u[i]) and MERGE(w, u[2]) (That is, given a term CONS(x, y), add verttces representingCAR(CONS(x,y)) and CDR(CONS(x, y)) and merge them with the vertices representingx and y ) 3 For zfrom 1 to s, tf ~-(x,)is equivalentto ~-(y,),return UNSATISFIABLEFor t from 1 to q, If the eqmvalence class of t-(u,)containsa vertex labeledCONS, return UNSATISFIABLE Otherwise,return SATISFIABLE If the length of the formula F is n, the size of G after step 2 is O(n). The average time required by this decision procedure to determine the satisfiability of a conjunction of literals is therefore O(n log n) using the fast congruence closure algorithm. PROOF OF CORRECTNESS. It is straightforward to verify that the algorithm is correct if it returns UNSATISFIABLE. Suppose that it returns SATISFIABLE; we construct an interpretation satisfying F. Let So be the partition of the vertices of G corresponding to the final equivalence relation. We define two functions CAR0 and CDR0 from So to So, and a function CONS0 from a subset of So × So to So. If the equivalence class Q contains a vertex v with a predecessor u labeled CAR, then CARo(Q) is the equivalence class of u; otherwise CARo(Q) is arbitrary. If Q contains a vertex v with a predecessor u labeled CDR, then CDRo(Q) is the equivalence class of u; otherwise CDRo(Q) is arbitrary. The pair (Q1, Q2) is in the domain of CONSo only if there exists a vertex v labeled CONS such that v[l] E Q1 and v[2] E Q2; in this case CONSo(Q1, Q2) is the equivalence class of v. Note that CARo, CDRo, and CONS0 are well defmed because the graph is closed under congruences. Unfortunately, CONSo is not a total function. To construct an interpretation, we must extend CONS0 to be defined on all of So x So. We first extend it to a function CONS1 which agrees with CONSo where CONS0 is defined, and otherwise just returns the ordered pair of its arguments. Since CONS1 returns elements of So x So, the range So of the interpretation must be extended to a set $1 that includes both So and part of So x So. But then CONS~ is not total and must be extended so that it is defined on all of S~ x S~. To construct an interpretation we repeat this extension step infinitely many times. More precisely, suppose that we have defined the first i + 1 quadruples in the infinite sequence (So, CONSo, CAR0, CDRo), (Sx, CONS1, CAR1, CDR1), . . . , (S,, CONS,, CAR,, CDR3 . . . . . We define the next quadruple (S,+l, CONS,+1, CAR,+~, CDR,+0 by the following rules.

362

G. NELSON AND D. C. OPPEN

Let D, be the domain o f CONS,. (1) S,+l = S, U St X St - Dr.

(2) The domain of CONS,+i is St x S,. CONS,+i(x, y) = CONS,(x, y) if (x, y) is in the domain of CONS,; CONSt+i(x, y) = (x, y) otherwise. (3) CAR,+i(x) -- CAR,(x) if x E St. Otherwise x ~ S, x S, - D, and is thus an ordered pair (y, z); in this case define CAR,+~(x) = y. (4) CDRt+~(x) = CDR,(x) i f x E S,. Otherwise x ~ S, x S, - Dt and is thus an ordered pair (y, z); in this case define C D R , + i ( x ) = 2. We now show that, for each i, CARt, CDRt, and CONS, have the following two properties. (1) If (x, y) is in the domain of CONS,, then CAR,(CONS,(x, y)) = x and C D R , ( C O N S , ( x , y)) = y.

(2) I f x is m the range of CONS,, then (CAR,(x), CDR,(x)) is in the domain of CONS,, and CONSt(CARt(x), CDR,(x)) = x. Consider first the base case, when i = 0 and x and y are eqmvalence classes. If (x, y) is in the domain of CONS0, then there is a vertex u with h(u) = CONS, u[l] E x, and u[2] E y. Since u is a CONS, two vertices v and w labeled C A R and CDR, respectively, were added as predecessors of u. The vertices v and w satisfy the requirements of the definitions of CAR0 and CDR0, so CAR0(CONS0(x, y)) is the equivalence class of v and CDRo(CONS0(x, y)) is the equivalence class of w. Furthermore the pairs (v, u[1]) and (w, u[2]) were added to R in step 2, so v and w are in the equivalence classes x and y, respectively. The proof that CARo, CDRo, and CONSo have the second property is similar. Suppose now that CONS,, CAR,, and CDR, satisfy properties 1 and 2. If (x, y) is in the domain of CONS,, then CONSt+~(x, y) = CONS,(x, y); at follows that CARt+i(CONS,+i(x, y)) = CARt(CONS,(x, y)) = x and CDR,+~(CONSt+i(x, y)) = C D R , ( C O N S , ( x , y)) = y by the induction hypothesis. Otherwase, CONS,+~(x, y) as the ordered pair (x, y), and CARt+i(CONSt+i(x, y)) = x and CDR,+~(CONS,+~(x, y)) = y by definition. A similar argument shows that CONS,+1, CARt+l, and CDR,+i satisfy property 2. It follows by reduction that, for all i, the functions CARt, CDR,, and CONS, have the two properties. Let S' be the union of all the St. Let CAR'(x) be CAR,(x) for the first i such that x E S,. Let C D R ' and C O N S ' be defined similarly. It follows that CAR', CDR', and C O N S ' have properUes 1 and 2 and that CONS' is defined on all of S' x S'. We are finally ready to define an interpretation xk satisfying F. The range of tk is S'. interprets CAR, CDR, and CONS as CAR', CDR', and CONS'. An element of S ' is anterpreted to be nonatomic if and only if it is in the range of CONS'. If f is an uninterpreted function symbol, Q~. . . . . Qk are m S, and there exists a vertex v such that ~(v) = f, 8(0 = k, and v[i] E Q, for each i from 1 to k, then 6(f)(Q~ . . . . . Qk) is the eqmvalence class of v. If this definition does not determine the value of ~/(f), then the value is arbitrary. It follows from properties 1 and 2 and the fact that the set of nonatoms is exactly the range of CONS' that this interpretauon satisfies axiom schema (2). It remains to show that ~ksatisfies F. It is straightforward to show that for each term t in the original formula, ~ 0 is the equivalence class of z(t). But "r(vt) and ,(w,) have been merged for each i from 1 to r, so tk satisfies the equalities in F. "r(xt) and ~'(Y3 are in different eqmvalence classes (since step 3 returned SATISFIABLE), so tk satisfies the dasequalities in F. Finally, no equivalence class of any ,(u,) contains a node labeled CONS; hence these classes are not m the range of CONSo. They are certainly not in the range of any of the other functions CONS,, so they are interpreted as atoms by ~k. Hence tk satisfies F. This completes the proof of correctness of the decision procedure.

Fast Decision Procedures Based on Congruence Closure

363

Somewhat surprisingly, when the result o f a selector function on an atom is specified by the axioms, the problem of determining the satisfiability of a conjunction o f literals becomes NP-complete. Consider the following axioms for the theory of CAR, CDR, and CONS with the single atom NIL: CAR(CONS(X, Y)) = X, CDR(CONS(X, Y ) ) = Y, X # N I L D CONS(CAR(X), CDR(X)) = X, CONS(X, Y) # NIL, CAR(NIL) = CDR(NIL) = NIL. We show that the problem of determining the satisfiability in this theory o f a conjunction of equalities and disequahties between terms containing CAR, CDR, CONS, NIL, and uninterpreted function signs is NP-complete. It is straightforward to show that the problem is in NP, since a nondeterministic program can guess the equivalence relaUon on the set of terms in the conjunction and then check that the equivalence relation does not violate any of the above axioms or the substitutivity of equality. To show that the problem is NP-hard, we will reduce the 3-CNF satisfiability problem for propositional calculus to it. (See [2].) Let P1. . . . . Pn be propositional variables and F a conjunction of three-element clauses over the P,. We construct a conjunction G of equalities and disequalities between liststructure terms involving CAR, CDR, CONS, NIL, and the 2n variables X1, Y~. . . . . Xn, Yn such that G is satisfiable if and only if F is. The first part of G is CAR(X1) = CAR(Y1)/~ CDR(X~) = CDR(Y1)/k X~ # Y1 A CAR(X2) = CAR(Y2) A CDR(X2) = CDR(Y2) A X2 # Y2 A :

(2)

CAR(Xn) = CAR(Yn) A CDR(X~) = CDR(Yn) A Xn # Yn. For no t can X, and Y, both be non-NIL, smce then X, and Y, would be equal by the third axiom and the substitutwity of equality. One of them must be N I L and the other CONS(NIL, NIL). Given an interpretation ~pfor G, we construct an interpretation ¢pfor F by defining dr(P,) to be T R U E if and only if ~p(X,) = NIL. The remaining conjuncts in G guarantee that ~p satisfies G if and only if th satisfies F. We demonstrate the construction with an example. If one of the clauses of F is Pt ~/ -~P2 W Pa, we want to add a conjunct to G which is eqmvalent to (Xl = N I L V X2 # N I L V X3 = NIL). In light of (2), this is eqmvalent to

-1(Y2 = NIL A X2 = N I L / ~ Y3 = NIL), or to the single hteral CONS(Yz, CONS(X2, Y3)) # CONS(NIL, CONS(NIL, NIL)). Note that we have shown the problem is NP-hard even without uninterpreted function symbols. A simdar construcUon can be used whenever the result of a selector function on an atom Is specified. The problem ts also NP-complete with the axiomatizatlon (1) if predicates are interpreted as Boolean-valued funcuons and literals such as F(ATOM(x)) # F(ATOM(y)) are allowed. ACKNOWLEDGMENT. We are indebted to Bob Tarjan for many helpful discussions. REFERENCES l, ACKERMANN,W Solvable Cases of the Dectston Problem North-Holland, Amsterdam, 1954 2 AHO, A V, HOPCROFT, J E, AND ULLMANN, J D The Destgn and Analysts of Computer Algortthms Addison-Wesley, Reading, Mass 1974

364

G. NELSON AND D. C. OPPEN

3. DOWNEY,P. J, SETHI, R , ANDTARTAN,R E. Var,ations on the common subexpresslon problem To appear m £ ACM.

4. KOZEN, D. Complexity of finitely represented algebras. Proc. 9th Annual ACM Symp. on Theory of Comptg., Boulder, Colo., May 1977, pp. 164-177. 5. NE~ON, C G., AND OPPEN, D. C Fast decision procedures based on UNION and'FIND. Proc Eighteenth Annual Syrup on Foundations of Comptr. Scl, Providence, R 1., 1977 (This is an earher version of the present paper.) 6 NELSON,C G., AND OPPEN, D. C Stmphfication by cooperating decision procedures To be pubhshed 70PPEN, D C. Reasoning about recurstvely defined data structures Proc 5th ACM Symp on Prmctples of Programming Languages, Tucson, ADz, January 1978, pp 151-157 8. SHOSTAK,R An algorithm for reasoning about equality Comm ACM 21, 7 (July 1978), 583-585 9 TARIAN,R. E Efficiency of a good but not linear set umon algorithm J ACM 22, 2 (April 1975), 215-225 RECEIVED JUNE

1978,

REVISED APRIL

1979,

ACCEPTED APRIL 1979

Journal of the Assoclat*on for Computing Machinery Vol 27, No 2, Aprd 1980

*When life gives you a hundred reasons to cry, show life that you have a thousand reasons to smile*

© Copyright 2015 - 2021 PDFFOX.COM - All rights reserved.