Parallel Processing of Resolution

PARALLEL PROCESSING OF RESOLUTION

Takahira YAMAGUCHI *, Yoshikazu TEZUKA* * a nd Os amu KAKUSHO*

• The I nstitute o f Scientific and Industria l Re search , Osaka University , 8-l Mihogaoka , Ibaragi , Osaka 567 , Japan
• ** Faculty o f Eng inee ring , Os aka University , 2-1 Yamadaoka, Suita , Os aka 565 , Japan

A B S T R A C T

I n this paper , PArallel Resolution Algorithm (PARA ) is described to improve the execution effici ency i n resolution process . PARA consists of two parts: parallel unification and generat ion of a r esolvent . The first part is character i stic of PARA , which partitions whole set of expressions W into independent clusters as pr e- pr ocessing and unifies each cluster in parall el . The efficient implementation for the processing peculiar t o PARA is presented and checked by means of the experiment in comparison of execution efficiency of resolut ion . Experimental results show PARA is very ef fective i n occurrence of many clusters .

1.INTRODUCTION

Unificati on in first-order logic is to match corresponding ar guments in two predicates . This pr ocessing is important in resolution [1] and the efficient implementation for it has been the subj ect of much investigation [2] - [5] . Butthis r esear ch in unification was out of parallel­ pr ocessing .

With r egard to unification (resolution) par allel ism, two representative ways , the post­ processing way and the pre- processing way , would be considered . In case of the former , after unification , t he consistency of substitution must be checked and each substitution component must be composed . This processing would be computed with unifi cation and so the post- processing way i s considered to cost much . On the contrar y , in case of t he latter , the pre- processing way to par tition a set of expressions f irstly could cost lit tle , because this processing could be computed wi thout unification .

From thi s cons ideration , in this paper , PARA is presented as one of the pre- processing ways . The characteristic of PARA lies in par titioning whole set of expressions W (the pair s of corresponding arguments in resolved literals) into clusters (sets of pairs of arguments such that each set has no variables in common ) a s pre- processing and unifying each cl uster i ndependently in parallel.

2.PARALLEL RESOLUTION ALGORITHM

Resolution consists of unification and generation of a resolvent . It costs more time to execute uni f i cation and so unification must be executed efficiently. The unification problern can be expressedas simultaneaus equations [5] and the solution of them can be cons i dered as most gener al unifier (mgu ) . The ordinary serial unificati on is process whi ch sol ves simul taneaus equations sequentially. They could , however , be divided into subsets of equations which are paral lel- processed independently . Parallel resolution consists of two parts : parallel­ processing of unification and generation of a resolvent . Fig. 1 shows PARA. Firstly PARA partitions whole sets of expr essi ons W into clusters of W1 - Wm which include no variables in common as pre- processing . Secondly, after this pre- processing, PARA tries to unify each cluster independently in parall el. If all clusters are unifiabl e , PARA obtains t he mgu of W by uniting the mgus of all cluster s . Otherwise PARA concludes that W is not unifiabl e . Finally , after having obtained t he mgu of W, PARA gener ates the resolvent and Clustering Information (which wil l be described later) .

3.EFFICIENT PROCESSING FOR PECULIAR PHASE IN PARA

The phases with * sign in Fig.1 are peeuliar to PARA. Among these phases, eluatering of W and generation of Clustering Information must be proeessed effieiently.

3.1 CLUSTERING INFORMATION

Sinee W is partitioned based on variables, Clustering Information will have to inelude the following information in order to exeeute eluatering of W effieiently ·

1. Variable Information (of argument)
2. Cluster Information (of literal)

Variable Information shows what variables eaeh argument of literal has. Variable Information is stored in a form easy to treat. Cluster Information shows how one literal ean be divided, Clustering Information eonsists of the above two pieees of information and the number of them. This is stored eorresponding to eaeh literal, as shown in Fig.2.

3.2 CLUSTER OPERATION ALGORITHM

Clustering of W is exeeuted by means of applying · eluster operation to Cluster Information of resolved literals. Cluster operation is the process which makes clusters for parallel unification. It matches n-th component of one Cluster Information with all components of the other and combines matched components. P(a,g(x1),x2,f(g(x2))) and P(x4,x3,f(x4),f(x3)) turn out nottobe divided by means of applying cluster operation to Cluster Information of them.

3.3 CLUSTERING INFORMATION GENERATION ALGORITHM Generating Clustering Information is executed

by means of making use of Variable Information of parent clauses.

Step 1 : Delete Variable Information of resolved literals of parent clauses. The rest is Variable Information of CLrsv' which is an incomplete resolvent which mgu is not applied.

Step 2 Generate the pairs of the variable number (natural number eorresponding to eaeh variable) ineluded in 11 term11 of mgu and the variable number eorresponding to the substituted variable of mgu.

Step 3 Apply Variable to Variable Information generate Variable Information a eomplete resolvent. Information of mgu of CLrsv 1 and of CLrsv which is

Step 4 : Generate Cluster Information of first literal by means of eluatering Variable Information.

Step 5 : Conneet Variable Information of and Cluster Information of and let them Clustering Information of CLrsv.

4oCOMPARISON OF PARA AND SRA

To eompare PARA with SRA (Serial Resolution Algorithm), 4 logie programs (6) have been run on two algorithms using theorem proving system 11 SENRI 11 (6). The run time for each process has been measured with exeeuting SNL resolution and the total time for resolution process has been finally eompared, Table 1 shows the experimental results,

PARA has about 2.1-fold improvement in unifi­ eation proeess and about 1,8-fold improvement in resolution process over SRA on the average.

Comparing the run time for generating resolvents in two algorithms, the run time of PARA is about twice one of SRA. This implies that the run time for generating Clustering Information is as small as one of generating resolvents and so does not affect the total time so badly.

Sinee the redundancy for generating Clustering Information adds to resolution process, the improvement rate of resolution process becomes worse. The improvement rate of resolution process is, however, areund 0.7times of the number of clusters. Moreovar the improvement rate of both unification proeess and resolution process rises in proportion to the number of clusters.

5, COMMENTS

In this experiment, some pairs of resolved literals, in which PARA becomes effective or ineffective, emerged definitely. Table 2 reports these literal pairs in detail.

(1) Litersl Pair 1 (in which resolution succeeds and PARA becomes effective) -> MICOM(FMB,FUJITSU,6809,218000)

MICOM( X1, X2 , X3 ,218000) Literal Pair 1 is divided into 4 clusters at the pre-processing. Since the mgu of each cluster has only Substitution component, the run time for substitution is short. So parallel resolution becomes very effective.

1. -> Literal Pair 2 (in which resolution fails and PARA becomes effective) MICOM(MZBOB,SHARP,ZBOA,278000) MICOM( Xl , X2 , XJ ,218000) 4

Literal Pair 2 is divided into clusters at the pre-processing and computation terminates at the time when cluster proves not to be unifiable. parallel resolution becomes very effective. the 4-th So

1. Literal Pair 3 (in which resolution fails and PARA becomes ineffective)
2. -> MAKER(OKI ,TOKYO, E) MAKER(SHARP, Xl ,X2)

Literal Pair 3 proves not to be unifiable at the first argument in SRA. So PARA becomes ineffective due to the extra time for clustering. Besides Literal Pair 3, literal pairs which are not divided at the pre-processing are similar.

1. This divided Table 2). Literal succeeds literal at the Pair(in which resolution and PARA becomes ineffective) pair is one which is not pre-processing(not shown in

unit time usec

machine ACOS system 1000 (NEC)

5 R A

Serial Resolution Algorithm

P A R A

PArallel Resolution Algorithm

I R

Improvement Rate

4 logic programs have literal pairs inconvenient for PARA as well as convenient for PARA and so the experiment is fair. Since the decrease in cost caused by convenient literal pairs is over the increase in cost caused by inconvenient literal pairs, PARA is effective to ordinary problems which include inconvenient literal pairs as well as convenient literal pairs.

6.CONCLUSION

PARA has been introduced for the improvement of execution efficiency for resolution process. It is characteristic of PARA to partition whole set of expressions W into independent clusters as pre-processing and unify each cluster in parallel.

The experimental results in comparison of execution efficiency for resolution show the following.

1. The processing peculiar to PARA has been impl~mented efficiently.
2. The improvement rates of both unification process and resolution process by parallel-processing rise in proportion to the number of clusters.
3. Since the decrease in cost caused by convenient literal pairs is over the increase in cost caused by inconvenient literal pairs, PARA is effective to ordinary problems.

Finally, unification in this paper is limited to be basic unification in [2]. Parallel-processing of refined unification in [4] or [5] would, however, be possible and further improvement could be expected.