Heuristic Search vs. Exhaustive Search

HEURISTIC SEARCH \'S. EXHAUSTI \'E SEARCH Laurent Sikl&ssy and Vesko Marinovl Department of Computer Sciences University of Texas at Au~tin Austin, Texas U.S.A.

ABSTRACT

A theorem proving system embodying a systema­ tic search procedure is described. Although the search spaces are usually infinite, ~nd not even locally finite, the asymmetric way in which they are generated results in a speed that is estima­ ted to be one to two orders of magnitude faster than the theorem provers of Quinlan and Hunt, aro Chang and the problem-solver of Fikes, to which this system has been compared extensively.

Descriptiv-e ~: search, heuristic search, ex­ haustive search, search space, locally infinite search space, rewriting rule, expansion rule, theorem proving, problem-solving .

I. INTRODUCTION

Heuristic programming techniques ha ve been developed to make it possible to solve problems whose solutions each constitute just one point~ a small set of points in a very large, and po$i­ bly infinite, space, the search space . Many pro­ blems in artificial intelligence are difficult, and require "intelligence" from the problem sol­ ver, precisely because of the size of the search space. Although heuristic search does not gua~ tee a solution, the size of the search space pre­ cludes an alternative technique such as exhaus~ search. Any method that would attempt to search unselectively the whole search space for a solu­ tion would quickly exhaust available resources of time and memory and would be bound to failure, except in some rare, "lucky" cases .

The statements in the above paragraph seem so "obvious" that few would disagree with them. The present study shows that, in fact, they are false in regards to several artificial intelligence systems that have been built. First, the search space is very small in many problems, often less than even a few dozen nodes. Second, although ttE search spaces may be infinite in principle, in reality only very small parts of this space need to be generated, in a systematic way, until the solution is found . Finally, a simple program, embodying a systematic, blind and "dumb" (?) pro­ cedure, was written. This program has solved over sixty problems that are typically considered as requiring heuristic search. The vast majority of these problems have a potentially infinite search space. An estimate of the relative speeds of different computers and programming languages indicates that our program is from one to two orders of magnitude faster, on the average, than the most powerful problem solvers with which it has been compared.

The reader should not conclude, either now or after reading the additional evidence that we present, that heuristic programming has no value . The success of our program, however, has impor­ tant methodological and practical consequences. Exhaustive search appears as a derided, yet powerful technique to solve many problems that ar~ very hard for humans and that ·remed t0 necessitate heuristics fnr thrir ·olution. In a powerful problem-solver, an exhaustivE' Sl·<nch component might have an important function in solving efficiently large classrs of problems, although alone it certainly cannot solve all problems .

II . PROBLEM DOMAIN

Points in the problem space arc expressions defined recursively as variables (atoms) or z~ one- and two-place function s~~bols (operators) having expressions as arguments . Constants are zero-place functions. Nvw points in the problem space can be obtained by applying a rewrite rule to an expression that is already in the problem space . A rewrite rule is of the form: (left-hand-side) : · <right-hand-side) where b0th sides are expressions . A rewrite rule can be applied to an expression if the expression, or one of its subexpressions, is a substitution instance of the left-hand-side of the rewrite rule . We say that the rewrite rule operates on the (sub)expression . The (sub)expression that is operated on is transformed by applying the same substitution to the right-han~-side of the re­ write rule. For example, if the binary operator + is used with the variables A, B and C; and if the expression (A+B)+C is in the problem space, a single application of the rewrite rule A+B : · B+A can produce two new expressions: C+(A+B) and (B+A)+C, depending on whether the rule is appl~ at the top level or not . The rules are seen as having one input and producing one output . This is not general, and in resolution, for example,

rewrite rules have two inputs for one output.

A theorem is in the form of a rewrite rule, for example (A+B)+C:·A+(B+C). A proof of the theorem consists in showing that, by a success~ of applications of rewrite rules, the left-hand side can be transformed into the right-hand sid~ After having been proved, theorems can be consid­ ered as rewrite rules.

This problem domain is identical to that con­ sidered extensively by Quinlan* (7) and Quinlan and Hunt "".' (8). Q&H show results of their learn­ ing programs, FDSl and FDS2, on 59 theorems grouped in 5 different areas (see Tables I through V). Q includes much additional informa­ tion on the programs' performance. FDS is con­ sidered the most powerful theorem-prover of its type. Ernst and Newell (3) consider the results of Q&H "quite impressive." (p. 27.) The same version of our program has proved all 59 theo~ in the tables in Q&H.

Chang (2) has also proved some of the theo~ in Q&H using a resolution-based system, and a comparison of his results with ours is given. Resolution is best viewed as a system utilizing a single two-input, one-output rewrite rule. Finally, Fikes (4) has documented proofs of four heuristic search problems . Although stated in a programming language, these four problems in Fikes can be easily rewritten as problems in a

*To Le abbreviated Q.

**To be abbreviated Q&H.

rewrite rule formulation. Two of them were solved by the same program that proved the theorems in Q&H. The addition of some numerical capabilities to our program would allow it to solve the other two problems. (See Siklossy and Harinov (10) for a hand-simulation and additional information on our system.) Some of the problems that can be easily expressed for Chang's system are awkward to express in our system of rewrite rules. Our system lacks the constraint manipulation tech­ niques and numerical capabilities of Fikes' REF­ ARF . On the other hand, it is doubtful that either Chang's or Fikes' system could prove all the theorems in Table Ill. In this article, their systems are compared on problems on an intersection of their respective domains of expertise with the domain of application of our system.

Ill. SYSTEMATIC SEARCH

A. Non-Expansion Rules

A theorem is of the form L:~R, where Land R are the left and right expressions of the theorem. A systematic search for the proof of the theorem starts with the search space consisting of the expression L. From L, we build the next ~ of the search tree. To thi_s effect, we apply to L all rewrite rules, one after the other . An expression resulting from the application of a rewrite rule to a node of the search tree is in­ serted in the tree if and only if it does not already figure in the search tree. Figure 1 shows the search tree for the proof of theorem I in Table I, using only the first two rewrite rules . The third node of the search tree, (B+A)+C, is called a dead node since no new expressions can be obtained by-;pplying rewrite rules Rl or R2 to this node. The search terminates when the expression A+(B+C) is found at the fifth level of the tree, as the 12th node .

B. Expansion Rules

The reader will notice that rule R4, A:· (A+B)-B, in Table 1 could also be applied to try to prove theorem 1. Any expression or subexpres­ sion is a substitution instance of the left­ hand-side of R4 . Thus, any (sub)expression can be rewritten, using R4, by first adding to it any expression, then subtracting the same expres­ sion that had been added. There are clearly an infinity of expressions that can be substituted forB, so that the search space is locally in­ finite and, consequently, some recent results in heuristic search by Pohl (6) on locally finite search spaces are not applicable to the problem domain considered here.

We call expansion ~ those rules (such as R4 in Table I, or R6 in Table IV) whose repeated application could generate an infinite search space for the problem domain considered. Some ordered generation of the space is needed, especially for those rules (such as R4 in Tablel) which allow the introduction of arbitrary expres.sions.

Since expansion rules play an important role in our system they deserve a more detailed dis­ cussion. The rules are a sample of the different types of expansion rules in the domains that we

have considered:

1. A:·(A+B)-B

R4 in Tables I and II.

2 . A/C:·(A/B)/C

R16 in Table III .

3. O:·A-A

T4 in Table Il . ''

4 . A:zA+O

Tl in Table II .

5. P:· P

R6 in Table IV.

6. A>B:·(A-B)>O

Rl in Table V.

The fir~t three rules generate a locally infin­ ite search space, while the other three gener­ ate an infinite space, which is locally finite . For example, applying Tl, Table II to the node X results in the node X+O. Another appli'cation of the same rewrite rule produces the three nodes (X+O)+O, (X+O)+O and X+(O+O) .

We further distinguish between two types of expansion rules . ~expansion rules have a single variable as thP. left-hand-side. Rules 1, 4 and 5 are atomic. The other expansion rules are called non-atomic. The search strategy is slightly di!f;r~r the two types of expan­ sion rules (see below) .

It is undecidable in general whether a re­ write rule system has an infinite search space. However, in the problem domains that we consid­ ered, a rule R is an expansion rule if it can be applied to its own right-hand-side (i.e . if the right-hand-side is a substitution instance of the left-hand-side) and if the expression ob­ tained by applying R to its own right-handside has more nodes (when considered as a tree) than the right-hand-side of R. It is seen that testing whether a rule is an expansion rule is a simple matter in our problem domains .

Our systematic search procedure proceeds as follows : first non-expansion rules are applied to the left-hand side of the theorem to be proved. If the right-hand side of the theorem is found, the system terminates . Other~ise, all nodes of the search tree are eventually dead, since non-expansion rules, by definition, can­ not generate an infinite search space . At that point, nodes of the search tree are generated in level order (9). For each node so generat ed, we apply all expansion rules (as will be described below), adding any new nodes to the search tree . We then shift to using only non­ expansion rules again . It is seen that expansion rules are called in only when all else has failed; and when they are called in, they are applied as sparsely as possible. The reason for this is simply that expansion rules ten.d t ·· increase drastically the size of the search space. It is interesting t·· notice the similar­ ity of our asymnetric use of rewrite rules tn the asymmetry in the use of the tW·' classes of axioms in the geometry theorem machine (5) . Tn this latter system, axioms of class (i i) are used only when axioms of class (i) havt· faile<l to prove a theorem .

An example of the use of a locally finite expansion rule (R6 in Table I\') is given in Figure 2. After the application of Rl to the left-hand side of theorem I, Table 1\', both nodes of the search tree are dead . The (unique) expansion rule R6 is applied to thv first node of the tree, namely (S.,.rR). R, producing nodes 3,4 and 5. We switch back to non-expansion rules only, and the answer is quickly found at node 9. Notice that nodes 2,6 and 7 are dead.

*0 is a constant .

The situation is fOre complex for a locally infinite expansion rule, which introduces arbi­ trary expressions, as, for example, R4 in Tables I and II . We have chosen to allow for such expressions only those that can be constructed legally from the atoms encountered in the themrem to be proved, which is no real restriction. It should be noted that here is the only case where the right-hand side of the theorem is used for purposes other than just checking for termina­ tion. Otherwise, the search is indeed blind~

Our strategy is to grow the search space as slowly as possible . We attain our goal by limit­ ing both the expressions to which atomic expan­ sion rules are applied, and the expressions that can be substituted for the arbitrary variables in locally infinite expansion rules. The growth of the search space takes place in several pa~~ and in each successive pass there are fewer limitations on the use of expansion rules.

I n a first pass, atomic expansion rules (whkh could be applied to any (sub)expression of a node ) are applied only to variables, constants and unary functions. There is no restriction on the (sub)expressions that non-atomic expansion rules are allowed to match. During that same first pass, we l imit the expressions that will be substituted for the arbitrary variables in l ocally infinite rules . (If a certain expression i s substituted for the arbitrary variable, we say that we are expanding with that expression.) In the first pass, locall y infinite expansion rules expand only with variables, constants and unary functions .

If the theorem is not proved during the first pas s, the restrictions described above would be successively loosened . We did not need to pro­ gram passes beyond the first s i nce all theorems could be proved during the first pass . Moreover, we are now testing more ·sophisticated techniques fo r expansion that render much of the above sc heme ineff i cient .

One might argue that we are using heuristics . We be lieve though that we are only using a stra­ t egy , si nce the orde r in wh i ch the rules are applied is predetermined and not modified during pr oof s.

IV. COMPARISONS WITH OTHER SYSTEMS

A. Comparisons with Quinlan and Hunt

The theor em provers of Q&H {there are two ve r s i ons of FDS) were written for a FORTRAN comp i l e r on the IBM 7094. Our sys tem is written f or a LISP 1. 5 interpreter on the CDC 6600 . Com­ pari sons be tween the speeds of the two systems a r e awkward. A consensus of "experts" indicates tha t we should expect our system to be about ten times'' s l ow.:- r than Q&H. (It was estimated tha t t he FORTRAtl compiler is about 100 times f as te r than our LISP interpreter, while the CDC 6600 may be s ome e ight t o ten time s faster t han t he IB~ 7094. ) To fac i lita te comparisons, all our times (in seconds) were divided by 10 in the results in Tables I through VI . All rewrite rules, labelled Ri, were taken in exactly the same order as given in Q&H, and all theorems, labelled Ti, proved exactly in the same order. All the proofs mentioned in this article were obtained with the same version of our program. By contrast, the results mentioned by Q&H are for different, locally optimized programs . The only exception is in Table V: the rewrite rules in Q&H are insufficient to prove the theorems. Q&H indicate that they used addi­ tional rewrite rules, without specifying which. We added the four rewrite rules Rl2 through RlS . Because of these changes, the results of Table V are not as meaningful as those of the first four tables . (In the tables below, S&M label our results.)

REWRITING RULES

Rl A+B: ·B+A

R2 A+(B+C):·(A+B)+C

R3 (A+B)-B:·A

R4 A: ·(A+B)-B

RS (A-B)+C:·(A+C)-B

R6 (A+B)-C:·(A-C)+B

Tl A: ·A+O

REWRITING RULES Rl A+B: ·B+A R2 A+(B+C):a(A+B)+C R3 (A+B)-B:·A R4 A:c(A+B)-B R5 (A-B)+C: ·(A+C)-B R6 (A+B)-C:z(A-C)+B R7 (A+B)+C:· A+(B+C) R8 (A-B)+B: =A R9 A:·(A-B)+B R10 A+(B-C):·(A+B)-C Rll (A-B)+C:·A+(C-B) R12 (A-C)-(B-C):-A-B R13 (A+C)-(B+C):·A-B R14 A+(B-C):·(A-C)+B R15 (A+B)-C:·A+(B-C) Rl6 (A-B)-C:=(A-C)-B R17 A-(B+C):·(A-B)-C R18 A+(B-C):zA-(C-B) R19 A-(B-C):·A+(C-B) R20 (A-B)+C:·A-(B-C) R21 A-(B-C) :·(A-B)+C R22 A-(B-C) :· (A+C)-B R23 (A-B)-C:·A-(B+C) R24 (A+B)-C:cA-(C-B) R25 A+O:cA R26 A-0: =A R27 NEG(A):=O-A R28 0-A:c~~�(A)

THEOREMS

'IIMES(Sean:ls) NoEs 1D

Solutim

Q&H S&M/ 10 by S&M

5

T2 A: =A-0

8

T3 A-A:zO

21

!4 0: zA-A

6

T5 A+NEG (A): ·0

5

T6 0: ·A+~~� (A)

58

T7 A+NEG(B):·A-B

5

T8 A-NEG (B): cA+B

6

T9 NE�(A)+~~�(B):·~~�(A+B) 125

TlO NEG(A)-NEG(B):·NEG(A-B) 47

Tll ~~�(NE�(A)):=A

105

Average

35.545

TABLE II

0.112

0.112

2.046

0.256

0.124

1. 095

0.201

0 . 124

2.136

1. 712

0.489

0. 764

11

11

58

13

8

44

10

6

50

51

13

Rl

R2

R3

R4

R5

R6

R7

R8

R9

. RIO

R11

R12

R13

Rl4

Rl5

Rl6

Rl7

R18

R19

R20

R21

R22

R23

R24

R25

R26

REWRITING RULES

(A+B)+C:·A+(B+C)

A+(B+C) :· (A+B)+C

I+A: ·A

A: ·I+A

A+I:·A

A:·A+I

Z+A: ·Z

A+Z : ·Z

Z:·A+Z

Z:·Z+A

I /I: ·I

I: ·I /I

(A+C)/(B+C) :· (A IB)+C

(A /B)+C:·(A+C) /(B+C)

(A/B) /C: =A/C

A/C: ·(A/B) /C

A/ (B /C): ·A/C

A/C: ·A/ (B / C)

SIG(A) :·(A+SIG(A)) / I

(A+SIG(A))/I :·SIG(A)

SIG(A IB) :·SIG(A)

SIG(A):·SIG(A/B)

SIG(A)+B/C:·SIG(A)+C

SIG(A)+C:·SIG(A)+B /C

SIG (I): .,z /I

Z/I: ·SIG(I)

R1

R2

R3

R4

REWRITING RULES

P·Q: =Q·P

P· (Q·R):=(P·Q)·R

p. (P-t Q}: =Q

rQ·(P-tQ};= P

RS rrp; =P

R6 P: :,-,-p

REWRITING RULES

• A>B:=(A-B}>O Rl
• (A-B)>O: =A:->B R2
• R3 A' O: =0>:-.'EG (A)
• R4 O>~'E�(A):=A>O

I

• RS A IS REAL:=(A>O) (A=O) I (:-lEG (A)>O)
• R6 (A IS REAL)· (B IS REAL):=(A-B) IS REAL
• R7 (A IS REAL)· (B IS REAL):=(A+B) IS REAL
• R8 (A-B)=O: =A=B
• R9 A=B:=(A-B)=O
• R10 (A> B) (B'>O): = (A+B)>O
• Rl1 (A>O) (B>O) : =(A"'B)>O
• R12 l\'EG (A): =0-A
• R13 0-A: =NEG (A)
• Rl4 A-B:=:IEG(B-A)

RlS

~'E� (B-A): =B-A

Actually, the comparison between Q&H and our system is misleading . Not only are their results obtained with two different versions of FDS, but their results for each Table are obtained after optimization of th~erage time to prove the theorems of a particular table. In other words, the particular version of FDS that proves most efficiently the theorems of Table III performs miserably when proving the theorems of Table I. In Table VI, we list, when available, the best and worst average times to prove theorems in the various tables (as collected from (7)) as well as the results in Q&H and our own.

A proof terminates when the (right-hand side of a) theorem is found. The level at which the theorem is encountered is fixed, but the number of nodes searched at that level can vary if we change the order in which the rewrite rules are applied. It would be straightforward to imple­ ment a system that would change the order of application of rewrite rules to minimize the average time per proof in a given table. We can­ not estimate the gains in speed that would result. As we mentioned previously, we have kept the order of the rules and theorems that we found in Q&H.

TABLE IV . Average times (in s) per t heorem.

B. Comparison with Fikes

Fikes (4) describes four heuristic search problems: monkey and bananas; waterj~g; a pro­ gramming problem; and the missionaries and canni­ bals. The statements of these problems are not reproduced here. These problems in Fikes are written in a programming language, but each of them can be translated easily into a rewrite rule system. Such a translation for the firs~ problem is given in Figure 3. In each triple, the first element indicates the monkey's positioq the second element the monke y's height and the last element the position of the box . Each of the rewrite rules corresponds to an allowable activity of the monkey, in exactly the same order as found in Fikes. The translation of the pro­ gramming problem is shown in Figure 4. The sex­ tuple represents the two registers put side by side. The rewrite rules correspond to the allowed shift operations.

Fikes' system was programmed on an IBM 360/ 67 for an IPL-V interpreter . His computer may be slightly slower than the CDC 6600, while we expect IPL to have a speed comparable to our LISP. The real times to solution, also listed in Figures 3 and 4, are therefore comparable as given.

The waterjug problem and the missionaries arn cannibals problem necessitate some arithmetiL capabilities that our sys tem lacks . Both problems can be eas i l y translated into a system for re­ write rules (see (10)). For example, in the waterjug problem the rewrite rule corresponding to pouring from the large jug into the small jug would be:

where the first and second element of the orderm pair represent the amounts of water in the small and large jugs, respectively.

The missionaries and cannibals problem has a total search space of 16 nodes (1) while our hand simulation (10) shows that our system would solve the waterjug problem in a total of seven nodes. We would estimate our system to use less than 2 seconds for each of these problems. These (hypothesized) times should be compared to 491 seconds and 83 seconds for Fikes' REF-ARF. More­ over, the particular way in which the missionarEs and cannibals problem is stated in REF has a strong influence on the time needed to solve it Fikes mentions that a particular statement of the problem would require more than 1800 seconds of 360/67 t i me .

C. Comparisons with Chang.

Chang (2) reports on a very efficient theorem prover based on the resolution principle. He has proved some of the theorems from Q&H . Table VII compares his times with ours. Chang's program is written in LISP 1.6 for the PDP-10. We do not know whether a compiled or interpreted version of LISP 1.6 was used .

REWRITE RULES 6 Rules as in Table I.

The results described in this section could be improved substantially, especially those of the long proofs. A newly generated node is added to the search space only if it is not already in the space. At present, the space is searched linearly for the existence of the node. A hash­ coding scheme would cut down dramatically on the time needed for such a search.

In spite of such improvements, our system would perform poorly in potentially large search spaces which could be reduced significantly by the manipulation of constraints.* We have repor­ ted results on problems for which few or no con­ straints can be used.

*Fikes' system has solved several constraint satisfaction problems .

V. CONCLUSIONS

The research reported here is part of a larger, continuing investigation into the cost of overhead in a theorem prover. It appears intuitive (but it may not be true) that, as a theorem prover applies more sophisticated tech­ niques to reduce its search space, it will expend more time for computation per node con­ sidered . The total number of nodes considered is an inadequate measure of the efficiency of a theorem prover, since this number does not take into account the cost per node . Total time to solution still appears as the only reasonable criterion for ~ring different systems with similar domains .

It may come as a surprise to many that our systematic, blind, search procedure performs at least one to two orders of magnitude faster than the most powerful existent theorem provers to which it has been compared. The result is even more surprising when it is stressed that the problem domains considered have infinite search spaces that are often not even locally finite The results can be explained by noticing that the proofs of the theorems are very short. The deepest proofs in Q&H (tied by the theorem in Figure 1) have a depth of only 5 . Many of the proofs in Q&H, and all four problems in Fikes, are found after generating at most a few dozen nodes.* Consequently, the problems considered should not tax the capabilities of a sophist i ­ cated heuristic program (although they certainl y seem to have done so!) . These problems do not represent adequate tests for such a program.

An informal investigation into the problems solved by artificial intelligence systems using heuristic search indicates that many of the tasks have, in fact, very small search spaces. If these problems are representative of many of the future problems to be solved by these systanS, then it is apparent that a very powerful problem solver can be built by combining heuristic and systematic search procedures that would time­ share available resources . The systematic search procedure could solve very rapidly a large number of the easy problems. The cooperation, inside a large system, of subsystems of various degrees of sophistication will be a fascinating area of research .

VI. REFERENCES

1. Amarel, S. On Representations of Problems of Reasoning about Actions, in: Michie , D. (Ed.), Machine Intelligence 1. American Elsev i er, N. Y. , 1968, 131-171.
2. Chang, C.L . The Unit Proof and the Input Proof in Theorem Proving, J . ACM, 17, 4, 1970, 698-707. -- -
3. Ernst, G.W. and Newell, A. GPS : a Case Study ~�enerality ~ Pr~em-S~ng , Academic Press, N.Y., 1969.
4. Fikes, R.E. REF-ARF : A System for Solving Problems Stated as Procedures, Artificial Intelligence, 1, 1970, 27-120.

*A more thorough discussion of the size of se<rch spaces will be reported subsequently .

1. �i lmer~, P.C. An Examinat i on of the Geometry Theorem Machine, Artificial Intelligence, 1, 3, 1970, 171-187 .
2. P;hl, I . Heuristic Search Viewed as Path Finding in a Graph, Artificial Intelligence, 1, 3, 1970, 193-204.
3. Q~inlan, J.R. FORTRAN Deductive System: Experim~nts with two Implementations, Technical Report n68-5-03, Computer Science Group, Univ~rsity of Washington , Seattle, 1968 .
4. Quinlan, J.R. and Hunt, E.B. A Formal Deduc­ tive Problem-Solving System, ~. 11. 4, 1968, 625-646 .
5. Salton, G. Manipulation of trees in informa­ tion retrie val, C.A,C.M,, i· 2, 103-114, 1962.
6. Siklossy, L. and Marinov, V. Experiments in search, Technical Report TSN-20, Com­ putation Center, University of Texas at Au s tin, 1971.

Rl (A, onfloor, B) :·(C, onfloor, B)

R2 (A, onfloor, A):·(C, onfloor, C)

R3 (A, onfloor, A):·(A, onbox, A)

R4 (A, onbox, A):·(A, onfloor, A}

R5 (underbananas, onbox, underbananas) : · (withbananas, onbox, underbananas)

Variables: A,B,C. Range : Xl,X2, underbananas.

Tl (XI, onfloor, X2) : ·

(withbananas, onbox, underbananas)

Times for proof : Fikes: 36s ; S&M 2. 027s .

FIGURE 3. Monkey and Bananas Problem.

Rl

(a,b,c,d,e,f): · (O,a,b,d,e,f)

R2

(a,b,c,d,e,f):·(b,c,O,d,e,f)

R3

(a,b,c,d,e,f):·(O,a,b,c,d,e)

R4

(a , b , c , d , e , f) : · (b , c , d , e , f , 0)

R5

(a,b,c,d,e,f): =(a,b,c ,a,b,c)

Tl

(2,3,4,0,0,0}:·(2,3,0,0,0,0)

Times for proof : Fikes 143s ; S&M 0 . 93ls.

FIGURE 4 . Programming Problem

1. One of the investigators (VM) was supported by the National Institute of Health Grant GM15769-04.